diff --git a/paragon.cabal b/paragon.cabal
--- a/paragon.cabal
+++ b/paragon.cabal
@@ -1,5 +1,5 @@
 Name:                   paragon
-Version:                0.1.21
+Version:                0.1.22
 License:                BSD3
 License-File:           LICENSE
 Author:                 Niklas Broberg
diff --git a/src/Language/Java/Paragon.hs b/src/Language/Java/Paragon.hs
--- a/src/Language/Java/Paragon.hs
+++ b/src/Language/Java/Paragon.hs
@@ -78,7 +78,8 @@
       -- Workaround for old and buggy 'filepath' versions
       _directory = if null directoryRaw then "./" else directoryRaw
   pp <- getPIPATH
-  let pDirs = concat [ splitSearchPath dir | PiPath dir <- flags ] ++ pp
+  let pDirsSpec = concat [ splitSearchPath dir | PiPath dir <- flags ] ++ pp
+      pDirs = if null pDirsSpec then ["./"] else pDirsSpec
   fc <- readFile filePath
   runBaseErr $ do
     ast <- liftShowEither $ parser compilationUnit fc
diff --git a/src/Language/Java/Paragon/Interaction.hs b/src/Language/Java/Paragon/Interaction.hs
--- a/src/Language/Java/Paragon/Interaction.hs
+++ b/src/Language/Java/Paragon/Interaction.hs
@@ -49,7 +49,7 @@
 issueTracker = "http://code.google.com/p/paragon-java/issues/entry"
 
 versionString :: String
-versionString = "0.1.19"
+versionString = "0.1.22"
 
 libraryBase, typeCheckerBase :: String
 libraryBase = "Language.Java.Paragon"
diff --git a/src/Language/Java/Paragon/Monad/Base.hs b/src/Language/Java/Paragon/Monad/Base.hs
--- a/src/Language/Java/Paragon/Monad/Base.hs
+++ b/src/Language/Java/Paragon/Monad/Base.hs
@@ -3,7 +3,7 @@
      ErrCtxt, Uniq, BaseM, runBaseM, runBaseErr,
 
      MonadIO(..), MonadBase(..), 
-     liftEither, liftShowEither,
+     liftEither, liftShowEither, tryCatch,
 
      getUniqRef, getErrCtxt, withErrCtxt,
 
@@ -73,14 +73,25 @@
 class MonadIO m => MonadBase m where
   liftBase :: BaseM a -> m a
   withErrCtxt' :: (ErrCtxt -> ErrCtxt) -> m a -> m a
+  tryM :: m a -> m (Either String a)
 
 instance MonadBase BaseM where
   liftBase = id
   withErrCtxt' strff (BaseM f) = BaseM $ \ec u -> f (strff ec) u
+  tryM (BaseM f) = BaseM $ \ec u -> do
+                           esa <- f ec u
+                           return $ Right esa
 
 
 withErrCtxt :: MonadBase m => String -> m a -> m a
 withErrCtxt str = withErrCtxt' (. (str ++))
+
+tryCatch :: MonadBase m => m a -> (String -> m a) -> m a
+tryCatch tr ctch = do esa <- tryM tr
+                      case esa of
+                        Right a -> return a
+                        Left err -> ctch err
+
 
 --------------------------------------------
 --                                        --
diff --git a/src/Language/Java/Paragon/Monad/PiReader.hs b/src/Language/Java/Paragon/Monad/PiReader.hs
--- a/src/Language/Java/Paragon/Monad/PiReader.hs
+++ b/src/Language/Java/Paragon/Monad/PiReader.hs
@@ -53,6 +53,7 @@
 instance MonadBase PiReader where
   liftBase ba = PiReader $ \_ -> ba
   withErrCtxt' ecf (PiReader f) = PiReader $ withErrCtxt' ecf . f
+  tryM (PiReader f) = PiReader $ tryM . f
 
 instance MonadIO PiReader where
   liftIO = liftBase . liftIO
diff --git a/src/Language/Java/Paragon/NameResolution.hs b/src/Language/Java/Paragon/NameResolution.hs
--- a/src/Language/Java/Paragon/NameResolution.hs
+++ b/src/Language/Java/Paragon/NameResolution.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TupleSections, QuasiQuotes #-}
 module Language.Java.Paragon.NameResolution (resolveNames) where
 
 import Language.Java.Paragon.Syntax
 import Language.Java.Paragon.Pretty
--- import Language.Java.Paragon.Parser
+import Language.Java.Paragon.QuasiQuoter
 import Language.Java.Paragon.Interaction
 
 import Language.Java.Paragon.NameResolution.Monad
@@ -28,10 +28,11 @@
 resolveNames :: PiPath                -- PIPATH
              -> CompilationUnit ()      -- Compilation unit to transform
              -> BaseM (CompilationUnit ())
-resolveNames piPath (CompilationUnit _ _pkg imps [td]) = runPiReader ("./":piPath) $ do
+resolveNames piPath (CompilationUnit _ _pkg imps [td]) = runPiReader piPath $ do
+  (_, javaLangExpnMap) <- buildMapFromImportName [impDeclQQ| import java.lang.*; |]
   (imps', impExpnMap) <- buildMapFromImports imps
   piExpnMap           <- buildMapFromPiPath
-  let jipExpnMap = unionExpnMaps [javaExpnMap, impExpnMap, piExpnMap]
+  let jipExpnMap = unionExpnMaps [javaExpnMap, javaLangExpnMap, impExpnMap, piExpnMap]
   (tnExpnMap,supExpnMap) <- buildMapFromTd td jipExpnMap
   -- We need to take the current name take precedence
   let expnMap = Map.union tnExpnMap (unionExpnMaps [jipExpnMap,supExpnMap])
@@ -658,7 +659,9 @@
                  
 -- The package name 'java' is always in scope.
 javaExpnMap :: Expansion
-javaExpnMap = Map.fromList $ mkPExpansion (Ident () "java")
+javaExpnMap = Map.fromList $ 
+                mkPExpansion (Ident () "java")
+
 
 {-
 buildMapFromCurrentPkg :: FilePath -> PiReader Expansion
diff --git a/src/Language/Java/Paragon/NameResolution/Monad.hs b/src/Language/Java/Paragon/NameResolution/Monad.hs
--- a/src/Language/Java/Paragon/NameResolution/Monad.hs
+++ b/src/Language/Java/Paragon/NameResolution/Monad.hs
@@ -37,6 +37,7 @@
 instance MonadBase NameRes where
   liftBase = liftPR . liftBase
   withErrCtxt' prf (NameRes f) = NameRes $ withErrCtxt' prf . f
+  tryM (NameRes f) = NameRes $ tryM . f
 
 instance MonadIO NameRes where
   liftIO = liftPR . liftIO
diff --git a/src/Language/Java/Paragon/PiGeneration.hs b/src/Language/Java/Paragon/PiGeneration.hs
--- a/src/Language/Java/Paragon/PiGeneration.hs
+++ b/src/Language/Java/Paragon/PiGeneration.hs
@@ -23,10 +23,10 @@
 transformCompilationUnit :: CompilationUnit () -> CompilationUnit ()
 transformCompilationUnit (CompilationUnit _ mpDecl _  [tdecl])
   = let cu = CompilationUnit () mpDecl []  [transformTypeDecl tdecl]
-    in expandLocals preName locals cu
-        where prePre = fmap (\(PackageDecl _ n) -> n) mpDecl
+    in {- expandLocals preName locals -} cu
+{-        where prePre = fmap (\(PackageDecl _ n) -> n) mpDecl
               preName = Name () TName prePre i
-              (i, locals) = gatherLocalAlps tdecl
+              (i, locals) = gatherLocalAlps tdecl -}
 transformCompilationUnit _ = panic (piGenModule ++ ".transformCompilationUnit") $
                              "More than one type decl"
 
diff --git a/src/Language/Java/Paragon/QuasiQuoter.hs b/src/Language/Java/Paragon/QuasiQuoter.hs
--- a/src/Language/Java/Paragon/QuasiQuoter.hs
+++ b/src/Language/Java/Paragon/QuasiQuoter.hs
@@ -47,7 +47,8 @@
 stmtQQ = parserQQ stmt
 lhsQQ  = parserQQ lhs
 
-varDeclQQ, methodBodyQQ, memberDeclQQ, fieldDeclQQ, methodDeclQQ, 
+impDeclQQ,
+  varDeclQQ, methodBodyQQ, memberDeclQQ, fieldDeclQQ, methodDeclQQ, 
   modifiersQQ, formalParamQQ, blockStmtQQ, classDeclQQ, lockPropQQ :: QuasiQuoter
 varDeclQQ    = parserQQ varDecl
 methodBodyQQ = parserQQ methodBody 
@@ -59,3 +60,4 @@
 blockStmtQQ  = parserQQ blockStmt
 classDeclQQ  = parserQQ classDecl
 lockPropQQ   = parserQQ lockProperties
+impDeclQQ    = parserQQ importDecl
diff --git a/src/Language/Java/Paragon/QuasiQuoter/Lift.hs b/src/Language/Java/Paragon/QuasiQuoter/Lift.hs
--- a/src/Language/Java/Paragon/QuasiQuoter/Lift.hs
+++ b/src/Language/Java/Paragon/QuasiQuoter/Lift.hs
@@ -110,6 +110,7 @@
        ''VarDeclId,
        ''ExplConstrInv,
        ''Stmt,
+       ''ImportDecl,
        ''EnumConstant, ''ForInit, ''SwitchBlock, ''Catch,
        ''SwitchLabel, ''EnumBody])
 
diff --git a/src/Language/Java/Paragon/TypeCheck.hs b/src/Language/Java/Paragon/TypeCheck.hs
--- a/src/Language/Java/Paragon/TypeCheck.hs
+++ b/src/Language/Java/Paragon/TypeCheck.hs
@@ -46,16 +46,16 @@
 -------------------------------------------------------------------------------------
 -- Here goes TcTypeDecl.hs
 
-typeCheckTd :: TypeCheck (TcDeclM r) TypeDecl
+typeCheckTd :: TypeCheck TcDeclM TypeDecl
 typeCheckTd (ClassTypeDecl     _ cdecl) = ClassTypeDecl Nothing <$> typeCheckCd cdecl
 typeCheckTd (InterfaceTypeDecl _ idecl) = InterfaceTypeDecl Nothing <$> typeCheckId idecl
 
-typeCheckId :: TypeCheck (TcDeclM r) InterfaceDecl
+typeCheckId :: TypeCheck TcDeclM InterfaceDecl
 typeCheckId (InterfaceDecl _ _ms i tps supers (InterfaceBody _ memberDecls)) = do
   --debug "typeCheckId"
   withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do
   let staticWPol = top
-  withThisType i tps supers $ do
+  registerThisType i tps supers
   withFoldMap withTypeParam tps $
    typeCheckActorFields memberDecls $ do
     --debug "typeCheckLockDecls start"
@@ -66,13 +66,14 @@
     typeCheckPolicyFields memberDecls $ do
      --debug "typeCheckSignatures start"
      typeCheckSignatures memberDecls $ \constrWPol -> do
+      registerThisTypeSigs i tps supers
       --debug "typeCheckMemberDecls start"
       InterfaceDecl Nothing (map notAppl _ms) (notAppl i) 
         (map notAppl tps) (map notAppl supers) .
           InterfaceBody Nothing <$>  
             typeCheckMemberDecls staticWPol constrWPol memberDecls
 
-typeCheckCd :: TypeCheck (TcDeclM r) ClassDecl
+typeCheckCd :: TypeCheck TcDeclM ClassDecl
 typeCheckCd (ClassDecl _ ms i tps mSuper _impls (ClassBody _ decls)) = do
   --debug "typeCheckCd"
   withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do
@@ -82,9 +83,9 @@
       inits       = [ idecl | idecl@(InitDecl {}) <- decls ]
       supers      = maybe [] (:[]) mSuper
   withFoldMap withTypeParam tps $ do
-  withThisType i tps supers $ do
+  registerThisType i tps supers
 --  withFoldMap withSuperType (maybe [] (:[]) mSuper) $ do
-   typeCheckActorFields memberDecls $ do
+  typeCheckActorFields memberDecls $ do
     debugPrint "typeCheckLockDecls start"
     typeCheckLockDecls memberDecls $ do
     debugPrint "typeCheckTypeMethods start"
@@ -93,7 +94,7 @@
     typeCheckPolicyFields memberDecls $ do
      debugPrint "typeCheckSignatures start"
      typeCheckSignatures memberDecls $ \constrWPol -> do
-      withThisTypeSigs i tps supers $ do
+        registerThisTypeSigs i tps supers
         ClassDecl Nothing (map notAppl ms) (notAppl i) 
           (map notAppl tps) (fmap notAppl mSuper) (map notAppl _impls) .
             ClassBody Nothing <$> do
@@ -106,8 +107,8 @@
 typeCheckCd _ = panic (typeCheckerBase ++ ".typeCheckCd")
                 "Enum decls not yet supported"
 
-withThisType :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM r a -> TcDeclM r a
-withThisType i tps supers tcda = do
+registerThisType :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM ()
+registerThisType i tps supers = do
     cTys   <- mapM evalSrcClsType supers
     baseTm <- getTypeMap
     let superTMs = flip map cTys $ \cTy -> 
@@ -117,17 +118,17 @@
                               $ "Super type evaluated but now doesn't exist: " ++ show mErr
                        Right superSig -> (tMembers superSig) { constrs = Map.empty }
 
-    withTypeMap (\tm ->
+    extendGlobalTypeMap (\tm ->
         -- We insert an empty typemap at first,
         -- since we are only using this when checking signatures
         let thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) 
                         True False cTys [] emptyTM
             newTm = tm { types = Map.insert i (tps,thisSig) (types tm) } 
-        in foldl merge newTm superTMs) $ tcda
+        in foldl merge newTm superTMs)
           
 
-withThisTypeSigs :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM r a -> TcDeclM r a
-withThisTypeSigs i tps supers tcba = do
+registerThisTypeSigs :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM ()
+registerThisTypeSigs i tps supers = do
   cTys   <- mapM evalSrcClsType supers
   baseTm <- getTypeMap
   let superTMs = flip map cTys $ \cTy -> 
@@ -141,30 +142,8 @@
       resTm  = foldl merge thisTm superTMs
       thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) 
                   True False cTys [] resTm -- TODO: Include proper values
-  withTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig) $
-    tcba
+  extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig)
 
-withTypeParam :: TypeParam () -> TcDeclM r a -> TcDeclM r a
-withTypeParam tp tcba = 
-    case tp of
-      ActorParam _ i -> do
-          let vti = VSig actorT top False False True
-          withTypeMap (\tm -> 
-              tm { actors = Map.insert i (ActorTPVar i) (actors tm),
-                   fields = Map.insert i vti (fields tm) }) $ tcba
-      PolicyParam _ i -> do
-           let vti = VSig policyT top False False True
-           withTypeMap (\tm ->
-              tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),
-                   fields = Map.insert i vti (fields tm) }) $ tcba
-      LockStateParam _ i -> do
-          let vti = VSig (lockT []) top False False True
-          withTypeMap (\tm ->
-              tm { fields = Map.insert i vti (fields tm) }) $ tcba
-      TypeParam _ _i _ -> do
-          --withTypeMap (\tm ->
-          --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $ 
-            tcba
 
 ---------------------------------------------------------------
 -- Actors
@@ -172,7 +151,7 @@
 -- TODO: We may have a problem with boot-strapping here.
 -- We can stay clear of the problem for now, using careful
 -- Paragon coding, but we need to think about it and fix it eventually.
-typeCheckActorFields :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
+typeCheckActorFields :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a
 typeCheckActorFields mDecls tcba = do
     --debug "fetchActors"
     let acts = [ (ms, vd) 
@@ -191,14 +170,14 @@
         tcba
         
             where spawnActorVd, evalActorVd -- , aliasActorVd 
-                      :: ([Modifier ()],VarDecl ()) -> TcDeclM r a -> TcDeclM r a
+                      :: ([Modifier ()],VarDecl ()) -> TcDeclM a -> TcDeclM a
                   -- Only Nothing for initializer
                   spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
                     a <- freshActorId (prettyPrint i)
                     p <- getReadPolicy ms
                     let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
-                    withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
-                                             fields = Map.insert i vti (fields tm) }) $
+                    withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
+                                                    fields = Map.insert i vti (fields tm) }) $
                       tcra
                   spawnActorVd (_, VarDecl _ arvid _) _ =
                       fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
@@ -226,8 +205,8 @@
                                Just a -> return a
                                Nothing -> aliasActorId --fail "Internal error: no such actor"
                            _ -> aliasActorId
-                    withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
-                                             fields = Map.insert i vti (fields tm) }) $
+                    withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
+                                                    fields = Map.insert i vti (fields tm) }) $
                       tcra
                   evalActorVd (_, VarDecl _ _ Nothing) _ = panic (typeCheckerBase ++ ".evalActorVd") $ "No initializer"
                   evalActorVd (_, VarDecl _ arvid _)   _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
@@ -237,18 +216,18 @@
 ---------------------------------------------------------------
 -- Locks
 
-typeCheckLockDecls :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
+typeCheckLockDecls :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a
 typeCheckLockDecls mds tcba = do
   let ls = [ ld | ld@ LockDecl {} <- mds ]
   withFoldMap typeCheckLockDecl ls $ tcba
 
-typeCheckLockDecl :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
+typeCheckLockDecl :: MemberDecl () -> TcDeclM a -> TcDeclM a
 typeCheckLockDecl (LockDecl _ ms i mps mProps) tcba = do
   lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
     pol <- getLockPolicy ms
     prs <- evalSrcLockProps i mProps
     return $ LSig pol (length mps) prs
-  withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
+  withCurrentTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
     tcba
 
 --typeCheckLockDecl (LockDecl _ _ _ _ _) _ = fail $ "Lock properties not yet supported"
@@ -258,7 +237,7 @@
 ---------------------------------------------------------------
 -- Typemethods
 
-typeCheckTypeMethods :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
+typeCheckTypeMethods :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a
 typeCheckTypeMethods mds tcba = do
   let tms = [ tmd | tmd@(MethodDecl _ ms _ _ _ _ _ _) <- mds,
                     Typemethod () `elem` ms
@@ -270,7 +249,7 @@
       tcba
 
 -- Precondition: only applied on actual typemethods
-typeCheckTMSig :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
+typeCheckTMSig :: MemberDecl () -> TcDeclM a -> TcDeclM a
 typeCheckTMSig (MethodDecl _ ms tps retT i ps exns _) tcba = do
   newMethMap <- withErrCtxt ("When checking signature of typemethod " 
                                ++ prettyPrint i ++ ":\n") $ do
@@ -302,16 +281,16 @@
         newMethMap = Map.singleton (tps, tyPs, isVarArity) mti
     return newMethMap
 
-  withTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $
+  withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $
        tcba
 
 typeCheckTMSig md _ = panic (typeCheckerBase ++ ".typeCheckTMSig") $
                       "Applied to non-method decl " ++ show md
 
-addTMBody :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
+addTMBody :: MemberDecl () -> TcDeclM a -> TcDeclM a
 addTMBody (MethodDecl _ _ _ _ i ps _ (MethodBody _ (Just bl))) =
     let pis = [ iP | FormalParam _ _ _ _ (VarId _ iP) <- ps ]
-    in withTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) }
+    in withCurrentTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) }
 addTMBody md = panic (typeCheckerBase ++ ".addTMBody") $
                "Applied to non-method decl " ++ show md
 
@@ -319,14 +298,14 @@
 -------------------------------------------------------------------------------------
 -- Policies
 
-typeCheckPolicyFields :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
+typeCheckPolicyFields :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a
 typeCheckPolicyFields mds =
     let pfs = [ pf | pf@(FieldDecl _ _ (PrimType _ (PolicyT _)) _) <- mds ] in
     -- The 'map' here means fields can only refer to things above them
     withFoldMap typeCheckPolicyField pfs
 
 -- Precondition: only apply on policies
-typeCheckPolicyField :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
+typeCheckPolicyField :: MemberDecl () -> TcDeclM a -> TcDeclM a
 typeCheckPolicyField fd@(FieldDecl _ ms t vds) tcba = do
   --debug "typeCheckPolicyField"
   -- 0. Flatten
@@ -357,14 +336,14 @@
       tcba  
 
           where 
-            addField :: VarFieldSig -> Ident () -> TcDeclM r a -> TcDeclM r a
+            addField :: VarFieldSig -> Ident () -> TcDeclM a -> TcDeclM a
             addField vti i = 
-                    withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) })
+                    withCurrentTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) })
 
 typeCheckPolicyField fd _ = panic (typeCheckerBase ++ ".typeCheckPolicyField") $
                            "Applied to non-policy decl " ++ show fd
 
-evalAddPolicyInit :: CodeState -> (Ident (), VarInit ()) -> TcDeclM r a -> TcDeclM r a
+evalAddPolicyInit :: CodeState -> (Ident (), VarInit ()) -> TcDeclM a -> TcDeclM a
 evalAddPolicyInit st (i, InitExp _ eInit) tcba = do
   --debug $ "evalAddInit: " ++ show i
   tcPol <- withErrCtxt ("When evaluating the initializer of field " 
@@ -373,7 +352,7 @@
   check (isPolicyType tyInit) $
         "Cannot initialize policy field " ++ prettyPrint i ++
         " with non-policy expression " ++ prettyPrint eInit ++ " of type " ++ prettyPrint tyInit
-  withTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $
+  withCurrentTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $
     tcba
 evalAddPolicyInit _ (i, arrInit) _ = 
     fail $ "Cannot initialize policy field " ++ prettyPrint i ++
@@ -382,19 +361,19 @@
 ------------------------------------------------------------------------------
 -- Signatures
 
-typeCheckSignatures :: [MemberDecl ()] -> (ActorPolicy -> TcDeclM r a) -> TcDeclM r a
+typeCheckSignatures :: [MemberDecl ()] -> (ActorPolicy -> TcDeclM a) -> TcDeclM a
 typeCheckSignatures mds tcbaf = do
   st <- setupStartState
   withFoldMap (typeCheckSignature st) mds $
     getConstrPol >>= tcbaf
 
-getConstrPol :: TcDeclM r ActorPolicy
+getConstrPol :: TcDeclM ActorPolicy
 getConstrPol = do
   mConstrs <- constrs <$> getTypeMap
   let wPols = map cWrites $ Map.elems mConstrs
   return $ foldl join bottom wPols
 
-typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM r a -> TcDeclM r a
+typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM a -> TcDeclM a
 -- Fields
 typeCheckSignature st (FieldDecl _ ms t vds) tcba 
     | t /= PrimType () (PolicyT ()) && t /= PrimType () (ActorT ()) = do
@@ -413,7 +392,7 @@
     mapM_ (typeCheckPolicyMod st) rPolExps
     rPol <- getReadPolicy ms
     check (Final () `elem` ms || (not $ includesThis rPol)) $
-          "Non-final field may not reference " ++ prettyPrint thisP
+          "Non-final field may not reference " ++ prettyPrint (thisP :: PrgPolicy TcActor)
 
     -- 3. Add signature to typemap
     return $ VSig {
@@ -426,9 +405,9 @@
   withFoldMap (addField vti) vds $
     tcba
 
-        where addField :: VarFieldSig -> VarDecl () -> TcDeclM r a -> TcDeclM r a
+        where addField :: VarFieldSig -> VarDecl () -> TcDeclM a -> TcDeclM a
               addField vti (VarDecl _ (VarId _ i) _) =
-                  withTypeMap $ \tm -> 
+                  withCurrentTypeMap $ \tm -> 
                       tm { fields = Map.insert i vti (fields tm) }
               addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd
 
@@ -470,7 +449,7 @@
                        (FormalParam _ _ _ b _ : _) -> b
     return $ Map.singleton (tps, pTs, isVarArity) mti
 
-  withTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $
+  withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $
     tcba
 
 -- Constructors
@@ -504,7 +483,7 @@
                        (FormalParam _ _ _ b _ : _) -> b
     return (pTs, isVarArity, cti)
 
-  withTypeMap (\tm -> tm { constrs = Map.insert (tps, pTs, isVA) cti (constrs tm) }) $
+  withCurrentTypeMap (\tm -> tm { constrs = Map.insert (tps, pTs, isVA) cti (constrs tm) }) $
     tcba
 
 -- Locks -- already handled
@@ -520,10 +499,10 @@
 
 typeCheckSignature _ _ tcba = tcba
 
-withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM r a -> TcDeclM r a
+withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM a -> TcDeclM a
 withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do
     let vsig = VSig ty p True (Static () `elem` ms) (Final () `elem` ms)
-    withTypeMap $ \tm -> 
+    withCurrentTypeMap $ \tm -> 
         tm { fields = Map.insert i vsig (fields tm) }
 
 
@@ -531,7 +510,7 @@
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
 
-typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM r (TcType, ExnSig)
+typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM (TcType, ExnSig)
 typeCheckExnSig st (ExceptionSpec _ ms xT) = do
   withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do
     ty <- TcRefT <$> evalSrcRefType xT
@@ -552,7 +531,7 @@
              }
     return (ty, xSig)
 
-checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM r ()
+checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM ()
 checkPolicyMods st ms failStr = do
   --debug $ "checkPolicyMods: " ++ show ms
   let rPolExps = [ e | Reads  _ e <- ms ] 
@@ -560,7 +539,7 @@
   check (length rPolExps <= 1 && length wPolExps <= 1) failStr
   mapM_ (typeCheckPolicyMod st) $ rPolExps ++ wPolExps
 
-checkLMMods :: [Modifier ()] -> TcDeclM r LockMods
+checkLMMods :: [Modifier ()] -> TcDeclM LockMods
 checkLMMods ms = do
   let cs = concat [ l | Closes _ l <- ms ]
       os = concat [ l | Opens  _ l <- ms ]
@@ -568,12 +547,12 @@
   tcOs <- mapM evalLock os
   return (tcCs, tcOs)
 
-checkExpectsMods :: [Modifier ()] -> TcDeclM r [TcLock]
+checkExpectsMods :: [Modifier ()] -> TcDeclM [TcLock]
 checkExpectsMods ms = do
   let es = concat [ l | Expects _ l <- ms ]
   mapM evalLock es
 
-typeCheckParam :: CodeState -> FormalParam () -> TcDeclM r (TcType, ActorPolicy)
+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, ActorPolicy)
 typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do
   withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do
     -- 1. Check parameter type
@@ -586,7 +565,7 @@
 typeCheckParam _ (FormalParam _ _ _ _ arvid) =
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
-typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM r (Policy T)
+typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM (Policy T)
 typeCheckPolicyMod st polExp = do
   -- tm <- getTypeMap
   -- debug $ show tm
@@ -605,21 +584,21 @@
 -- Initializers
 
 -- Precondition: Only init decls
-typeCheckInitDecls :: ActorPolicy -> ActorPolicy -> [Decl ()] -> TcDeclM r [Decl T]
+typeCheckInitDecls :: ActorPolicy -> ActorPolicy -> [Decl ()] -> TcDeclM [Decl T]
 typeCheckInitDecls sLim cLim is = do
   stSt <- setupStartState
   (sIs, st) <- go (typeCheckInitDecl sLim) stSt [] [ bl | InitDecl _ True  bl <- is ]
   (iIs, _ ) <- go (typeCheckInitDecl cLim) st   [] [ bl | InitDecl _ False bl <- is ]
   return (map (InitDecl Nothing True) sIs ++ map (InitDecl Nothing False) iIs)
 
-      where go :: (CodeState -> Block () -> TcDeclM r (CodeState, Block T))
-               -> CodeState -> [Block T] -> [Block ()] -> TcDeclM r ([Block T], CodeState)
+      where go :: (CodeState -> Block () -> TcDeclM (CodeState, Block T))
+               -> CodeState -> [Block T] -> [Block ()] -> TcDeclM ([Block T], CodeState)
             go _ st acc [] = return (reverse acc, st)
             go f st acc (bl:bls) = do (st', blT) <- f st bl
                                       go f st' (blT:acc) bls
   
 
-typeCheckInitDecl :: ActorPolicy -> CodeState -> Block () -> TcDeclM r (CodeState, Block T)
+typeCheckInitDecl :: ActorPolicy -> CodeState -> Block () -> TcDeclM (CodeState, Block T)
 typeCheckInitDecl lim st bl = do
     tm <- getTypeMap
     (newSB,cs) <- runTcCodeM (simpleEnv lim $ "initializer block") st $
@@ -633,12 +612,12 @@
 ------------------------------------------------------------------------------
 -- Bodies
 
-typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM r [MemberDecl T]
+typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM [MemberDecl T]
 typeCheckMemberDecls sLim cLim ms = do
   st <- setupStartState
   mapM (typeCheckMemberDecl sLim cLim st) ms
 
-typeCheckMemberDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) MemberDecl
+typeCheckMemberDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl
 typeCheckMemberDecl sLim cLim st fd@(FieldDecl {}) =
     typeCheckFieldDecl sLim cLim st fd
 typeCheckMemberDecl _ _ st md@(MethodDecl {}) =
@@ -647,7 +626,7 @@
     typeCheckConstrDecl st cd
 typeCheckMemberDecl _ _ _ md = return $ notAppl md
 
-typeCheckFieldDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) MemberDecl
+typeCheckFieldDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl
 typeCheckFieldDecl staticLim constrLim st (FieldDecl _ ms _t vds) = do
   --debug $ "typeCheckFieldDecl:" ++ show fd
   let lim = if Static () `elem` ms then staticLim else constrLim
@@ -657,7 +636,7 @@
 typeCheckFieldDecl _ _ _ md = panic (typeCheckerBase ++ ".typeCheckFieldDecl") $
                               "Applied to non-field decl " ++ show md
 
-typeCheckVarDecl :: ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) VarDecl
+typeCheckVarDecl :: ActorPolicy -> CodeState -> TypeCheck TcDeclM VarDecl
 typeCheckVarDecl lim st vd@(VarDecl _ (VarId _ i) mInit) = do
   --debug $ "typeCheckVarDecl:" ++ show i
   withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do
@@ -691,7 +670,7 @@
 typeCheckVarDecl _ _ vd = fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd
 
 
-typeCheckMethodDecl :: CodeState -> TypeCheck (TcDeclM r) MemberDecl
+typeCheckMethodDecl :: CodeState -> TypeCheck TcDeclM MemberDecl
 typeCheckMethodDecl st (MethodDecl _ _ms tps _rt i ps _exs mb) = do
   -- Lookup the correct function signature
   debugPrint $ "Type-checking method " ++ prettyPrint i
@@ -746,7 +725,7 @@
                             "Applied to non-method decl " ++ show md
 
 
-typeCheckConstrDecl :: CodeState -> TypeCheck (TcDeclM r) MemberDecl
+typeCheckConstrDecl :: CodeState -> TypeCheck TcDeclM MemberDecl
 typeCheckConstrDecl st (ConstructorDecl _ _ms tps ci ps _exs cb) = do
   withErrCtxt ("When checking body of constructor " ++ prettyPrint ci ++ ":\n") $ do
   --debug $ "Type-checking constructor:\n " ++ prettyPrint cd
@@ -805,13 +784,13 @@
 typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $
                             "Applied to non-constructor decl " ++ show md
 
-aliasIfActor :: (Ident (), TcType) -> TcDeclM r [(Ident (), ActorId)]
+aliasIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)]
 aliasIfActor (i, ty)
     | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]
     | otherwise = return []
                 
 
-checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM r ()
+checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM ()
 checkExnMods st (xTy, lms) = do
   let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st)
   maybeM mExnSt $ \sX -> do
@@ -820,11 +799,11 @@
               ++ show lms
 
 
-tcMethodBody :: TypeCheck (TcCodeM r) MethodBody
+tcMethodBody :: TypeCheck (TcCodeM) MethodBody
 tcMethodBody (MethodBody _ mBlock) = 
     MethodBody Nothing <$> maybe (return Nothing) ((Just <$>) . tcBlock) mBlock
 
-tcConstrBody :: TypeCheck (TcCodeM r) ConstructorBody
+tcConstrBody :: TypeCheck (TcCodeM) ConstructorBody
 tcConstrBody (ConstructorBody _ mEci stmts) = do
   mEci' <- maybe (return Nothing) ((Just <$>) . tcEci) mEci
   stmts' <- tcBlockStmts stmts
diff --git a/src/Language/Java/Paragon/TypeCheck/Constraints.hs b/src/Language/Java/Paragon/TypeCheck/Constraints.hs
--- a/src/Language/Java/Paragon/TypeCheck/Constraints.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Constraints.hs
@@ -16,8 +16,8 @@
 constraintsModule :: String
 constraintsModule = typeCheckerBase ++ ".Constraints"
 
-data Constraint = LRT (PrgPolicy TcAtom) [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)
-  deriving Show
+data Constraint = LRT [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)
+  deriving (Show, Eq)
 
 type ConstraintWMsg = (Constraint, String)
 
diff --git a/src/Language/Java/Paragon/TypeCheck/Containment.hs b/src/Language/Java/Paragon/TypeCheck/Containment.hs
--- a/src/Language/Java/Paragon/TypeCheck/Containment.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Containment.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternGuards #-}
 module Language.Java.Paragon.TypeCheck.Containment (lrt) where
 
 import Language.Java.Paragon.Syntax
@@ -9,40 +10,64 @@
 import Language.Java.Paragon.TypeCheck.Locks
 
 import Language.Java.Paragon.Pretty
+import Language.Java.Paragon.Interaction
 
 import Debug.Trace
 
 import Data.List
 import Data.Maybe
 
-lrt :: PrgPolicy TcAtom -> 
+containmentModule :: String
+containmentModule = typeCheckerBase ++ ".Containment"
+
+lrt :: [TcClause TcAtom] -> 
        [TcLock] -> 
        TcPolicy TcActor -> 
        TcPolicy TcActor -> 
        Either Bool Constraint
-lrt TcThis _ _ _ = error "Error: TcThis instead of concrete global policy in lrt check."
-lrt (TcRigidVar _) _ _ _ = error "Error: Rigid var instead of concrete global policy in lrt check."
-lrt (TcJoin _ _) _ _ _ = error "Error: TcJoin instead of concrete global policy in lrt check."
-lrt (TcMeet _ _) _ _ _ = error "Error: TcJoin instead of concrete global policy in lrt check."
-lrt (TcPolicy g) ls (RealPolicy (TcPolicy p)) (RealPolicy (TcPolicy q)) = 
-    Left (lrtC g ls p q)
-lrt g ls (RealPolicy (TcRigidVar _)) q = lrt g ls top q
-lrt g ls p (RealPolicy (TcRigidVar _)) = lrt g ls p bottom
-lrt _ _ (RealPolicy _) (RealPolicy _) = 
-    error "Error: Non-computed policy provided to lrt"
-lrt g ls p@(RealPolicy _) q@(VarPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(VarPolicy _) q@(RealPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(VarPolicy _) q@(VarPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(Join p1 p2) q = let
-    ap1 = lrt g ls p1 q
-    ap2 = lrt g ls p2 q
-    in either (\x -> if x then ap2 else Left False)
-              (\c -> either (\x -> if x then Right c else Left False)
-                            (\_ -> Right (LRT g ls p q) )
-                            ap2
-              )
-              ap1
-lrt _ _ _ (Join _ _) = error "Error: Join occurring on right-hand side of lrt check!"
+lrt g ls p q =
+    case (p, q) of
+      (_, Join _ _) -> panic (containmentModule ++ ".lrt")
+                       $ "Join occuring on the right-hand side of an lrt check: " ++ show q
+      (RealPolicy rp, RealPolicy rq) -> Left $ lrtReal g ls rp rq
+      (Join p1 p2, _) -> let
+                    ap1 = lrt g ls p1 q
+                    ap2 = lrt g ls p2 q
+                    in case (ap1, ap2) of
+                         _ | Left False `elem` [ap1, ap2] -> Left False
+                         (Left True, _) -> ap2
+                         (_, Left True) -> ap1 
+                         _ -> Right (LRT g ls p q)
+
+      (VarPolicy _, _) -> Right (LRT g ls p q)
+      (_, VarPolicy _) -> Right (LRT g ls p q)
+
+
+lrtReal :: [TcClause TcAtom] 
+        -> [TcLock]
+        -> PrgPolicy TcActor 
+        -> PrgPolicy TcActor 
+        -> Bool
+--lrtReal _ _ p q | any includesThis [p,q] =
+--                    panic (containmentModule ++ ".lrtReal")
+--                              $ "THIS in containment check: " ++ show (p,q)
+lrtReal g ls (TcPolicy p) (TcPolicy q) =  lrtC g ls p q
+lrtReal g ls (TcJoin p1 p2) q = lrtReal g ls p1 q && lrtReal g ls p2 q
+lrtReal g ls p (TcMeet q1 q2) = lrtReal g ls p q1 && lrtReal g ls p q2
+lrtReal g ls p q
+        | Just i <- firstRigid (TcJoin p q) = 
+                    let subi pol x = substPolicy [(i, x)] pol
+                        [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, top]) [p,q]
+                    in lrtReal g ls pb qb && lrtReal g ls pt qt
+        | any includesThis [p,q] =
+                    let [[pb,pt],[qb,qt]] = map (\y -> map (flip substThis y) [bottom, top]) [p,q]
+                    in lrtReal g ls pb qb && lrtReal g ls pt qt
+lrtReal _ _ p q = 
+    panic (containmentModule ++ ".lrtReal") 
+    $ "Error: Non-computed policy provided to lrt: " ++ show (p, q)
+
+
+
 
 -- If either p or q at least contain a policy variable, 
 -- we know we'll send back a constraint
diff --git a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
--- a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
@@ -55,7 +55,7 @@
   let def = foldl join bottom ppols
   return $ mpol `orUse` def
 -}
-evaluate :: Policy () -> TcDeclM r (TcPolicy TcActor)
+evaluate :: Policy () -> TcDeclM (TcPolicy TcActor)
 evaluate = evalPolicy
 {-evaluate (PolicyExp _ pe) = evalPolicyExp pe
 evaluate (ExpName _ n) = -- getPolicy n
@@ -74,7 +74,7 @@
 evaluate (MethodInv _ mi) = evalTypeMethod mi
 evaluate e = fail $ "Unsupported type-level expression: " ++ prettyPrint e
 -}
-evalTypeMethod :: MethodInvocation () -> TcDeclM r (TcPolicy TcActor)
+evalTypeMethod :: MethodInvocation () -> TcDeclM (TcPolicy TcActor)
 evalTypeMethod = panic (evaluateModule ++ ".evalTypeMethod") ("undefined!")
 
 orUse :: Maybe a -> a -> a
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad.hs b/src/Language/Java/Paragon/TypeCheck/Monad.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad.hs
@@ -98,10 +98,10 @@
 import Data.IORef
 import Data.List (union, intersperse)
 
---debug :: String -> TcDeclM r ()
+--debug :: String -> TcDeclM ()
 --debug str = liftIO $ finePrint $ "DEBUG: " ++ str
 
---debugTc :: String -> TcCodeM r ()
+--debugTc :: String -> TcCodeM ()
 --debugTc = liftTcDeclM . debug
 
 monadModule :: String
@@ -113,12 +113,12 @@
 
 -- this
 
---getThisType :: TcCodeM r TcType
+--getThisType :: TcCodeM TcType
 --getThisType = liftCont getThisT
 
 -- returns
 
-getReturn :: TcCodeM r (TcType, ActorPolicy)
+getReturn :: TcCodeM (TcType, ActorPolicy)
 getReturn = do
   mRet <- returnI <$> getEnv
   case mRet of
@@ -135,21 +135,21 @@
 --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) }
 
 
-extendVarEnvList :: [(Ident (), VarFieldSig)] -> TcCodeM r a -> TcCodeM r a
+extendVarEnvList :: [(Ident (), VarFieldSig)] -> TcCodeM a -> TcCodeM a
 extendVarEnvList vs = withEnv $ \env ->
   let oldVmap = vars env
       newVmap = foldl (\m (i,vti) -> Map.insert i vti m) oldVmap vs
   in env { vars = newVmap }
 
-extendVarEnv :: Ident () -> VarFieldSig -> TcCodeM r a -> TcCodeM r a
+extendVarEnv :: Ident () -> VarFieldSig -> TcCodeM a -> TcCodeM a
 --extendVarEnv i = extendVarEnvN i
---extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM r a -> TcCodeM r a
+--extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM a -> TcCodeM a
 extendVarEnv i vti = withEnv $ \env ->
   let oldVmap = vars env
       newVmap = Map.insert i vti oldVmap
   in env { vars = newVmap }
 
-lookupActorName :: ActorName () -> TcCodeM r (TcType, ActorPolicy)
+lookupActorName :: ActorName () -> TcCodeM (TcType, ActorPolicy)
 lookupActorName (ActorName _ nam@(Name _ nt mPre i))
     | nt == EName = 
         do (ty, pol, _) <- lookupVar mPre i
@@ -166,7 +166,7 @@
 -- | Lookup the prefix part of a name, which has to be dereferenceable.
 --   Returns the relevant type (Nothing if package), its typemap 
 --   and the accumulated policy of the name access path.
-lookupPrefixName :: Name () -> TcCodeM r (Maybe TcType, TypeMap, ActorPolicy)
+lookupPrefixName :: Name () -> TcCodeM (Maybe TcType, TypeMap, ActorPolicy)
 lookupPrefixName n@(Name _ EName Nothing i) = do
     -- Special case: This *could* be a var, since those can only
     -- appear first in the name, i.e. prefix == Nothing
@@ -228,7 +228,7 @@
 
 -- | Lookup the type and policy of a field or variable access path.
 --   Precondition: Name is the decomposition of an EName
-lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM r (TcType, ActorPolicy, Bool)
+lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM (TcType, ActorPolicy, Bool)
 lookupVar Nothing i = do
   -- Could be a single variable
   varMap <- vars <$> getEnv
@@ -239,7 +239,7 @@
     Nothing -> do
       tm <- getTypeMap
       case Map.lookup i $ fields tm of
-        Just (VSig ty p _ _ _) -> return (ty, p, False)
+        Just (VSig ty p param _ _) -> return (ty, p, param)
         Nothing -> panic (monadModule ++ ".lookupVar") 
                    $ "Not a var or field: " ++ show i
 
@@ -261,20 +261,20 @@
     :: [TypeArgument ()]
     -> [TcType]
     -> [Sig]  -- Works for both methods and constrs
-    -> TcCodeM r [Sig]
+    -> TcCodeM [Sig]
 findBestMethod tArgs argTys candidates =
   findBestFit =<< filterM isApplicable candidates
 
-  where isApplicable :: Sig -> TcCodeM r Bool
+  where isApplicable :: Sig -> TcCodeM Bool
         isApplicable (tps, pTys, isVA) = 
             (&&) <$> checkArgs tps tArgs <*> checkTys isVA pTys argTys
 
-        checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM r Bool
+        checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM Bool
         checkArgs [] [] = return True
         checkArgs (tp:tps) (ta:tas) = (&&) <$> checkArg tp ta <*> checkArgs tps tas
         checkArgs _ _ = return False
 
-        checkArg :: TypeParam () -> TypeArgument () -> TcCodeM r Bool
+        checkArg :: TypeParam () -> TypeArgument () -> TcCodeM Bool
         checkArg _ _ = return True -- TODO: Type arguments not yet handled correctly
 
         checkTys _ [] [] = return True
@@ -287,11 +287,11 @@
         checkTys b (p:ps) (a:as) = (&&) <$> (p =<: a) <*> checkTys b ps as
         checkTys _ _ _ = return False
 
-        findBestFit :: [Sig] -> TcCodeM r [Sig]
+        findBestFit :: [Sig] -> TcCodeM [Sig]
         findBestFit [] = return []
         findBestFit (x:xs) = go [x] xs
 
-        go :: [Sig] -> [Sig] -> TcCodeM r [Sig]
+        go :: [Sig] -> [Sig] -> TcCodeM [Sig]
         go xs [] = return xs
         go xs (y:ys) = do
           bs0 <- mapM (\x -> y `moreSpecificThan` x) xs
@@ -299,7 +299,7 @@
            else do bs1 <- mapM (\x -> x `moreSpecificThan` y) xs
                    if and bs1 then go xs ys else go (y:xs) ys
 
-        moreSpecificThan :: Sig -> Sig -> TcCodeM r Bool
+        moreSpecificThan :: Sig -> Sig -> TcCodeM Bool
         moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (=<:) ps2 ps1
         moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do
           let n = length ps1
@@ -312,7 +312,7 @@
              -> Ident ()           -- Method name
              -> [TypeArgument ()]  -- Type arguments
              -> [TcType]           -- Argument types
-             -> TcCodeM r (ActorPolicy, [TypeParam ()], MethodSig)
+             -> TcCodeM (ActorPolicy, [TypeParam ()], MethodSig)
 lookupMethod mPre i tArgs argTys = do
   baseTm <- getTypeMap
   (mPreTy, preTm, prePol) <- case mPre of
@@ -363,7 +363,7 @@
 --   so the policy of the access path is irrelevant.
 lookupLock :: Maybe (Name ()) -- Access path
            -> Ident ()        -- Name of lock
-           -> TcCodeM r LockSig
+           -> TcCodeM LockSig
 lookupLock mPre i = do
   baseTm <- getTypeMap
   preTm <- case mPre of
@@ -373,11 +373,9 @@
                        return preTm
   case Map.lookup i $ locks preTm of
     Just lsig -> return lsig
-    Nothing -> panic (monadModule ++ ".lookupLock")
-               $ "Not a lock: " ++ show (Name () LName mPre i)
-
+    Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope"
 
-getPolicy :: Name () -> TcCodeM r ActorPolicy
+getPolicy :: Name () -> TcCodeM ActorPolicy
 getPolicy n = do
   tm <- getTypeMap
   case lookupNamed policies n tm of
@@ -385,7 +383,7 @@
     Just p -> return p
 
 
-lookupFieldT :: TcType -> Ident () -> TcCodeM r VarFieldSig
+lookupFieldT :: TcType -> Ident () -> TcCodeM VarFieldSig
 lookupFieldT typ i = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
   aSig <- lookupTypeOfType typ
@@ -398,7 +396,7 @@
               -> Ident () 
               -> [TypeArgument ()] 
               -> [TcType] 
-              -> TcCodeM r ([TypeParam ()], MethodSig)
+              -> TcCodeM ([TypeParam ()], MethodSig)
 lookupMethodT typ i tArgs argTys = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
   aSig <- lookupTypeOfType typ
@@ -431,7 +429,7 @@
 lookupConstr :: TcClassType 
              -> [TypeArgument ()]
              -> [TcType] 
-             -> TcCodeM r ([TypeParam ()], ConstrSig)
+             -> TcCodeM ([TypeParam ()], ConstrSig)
 lookupConstr ctyp tArgs argTys = do
   debugPrint $ "\n\n######## Looking up constructor! ######## \n"
   let typ = clsTypeToType ctyp
@@ -460,7 +458,7 @@
               Just csig -> return (tps, csig)
                  
 
---lookupLock :: Name () -> TcCodeM r LockSig
+--lookupLock :: Name () -> TcCodeM LockSig
 --lookupLock n = do
 --  tm <- getTypeMap
 --  -- debugTcCodeM $ show tm
@@ -468,17 +466,17 @@
 --    Nothing -> fail $ "Unknown lock: " ++ prettyPrint n
 --    Just lsig -> return lsig
 
-lookupExn :: TcType -> TcCodeM r (ActorPolicy, ActorPolicy)
+lookupExn :: TcType -> TcCodeM (ActorPolicy, ActorPolicy)
 lookupExn tyX = do
   exnMap <- exnsE <$> getEnv
   case Map.lookup tyX exnMap of
     Just ps -> return ps
     Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX
 
-registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM r a -> TcCodeM r a
+registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM a -> TcCodeM a
 registerExn tyX rX wX = registerExns [(tyX, (rX,wX))]
 
-registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM r a -> TcCodeM r a
+registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM a -> TcCodeM a
 registerExns tysPols =
     withEnv $ \env -> 
         let oldMap = exnsE env
@@ -486,44 +484,44 @@
         in env { exnsE = newMap }
 
 
-extendLockEnv :: [TcLock] -> TcCodeM r a -> TcCodeM r a
+extendLockEnv :: [TcLock] -> TcCodeM a -> TcCodeM a
 extendLockEnv locs = withEnv $ \env -> 
                         env { lockstate = lockstate env `union` locs }
 
-getBranchPC :: Entity -> TcCodeM r [(ActorPolicy, String)]
+getBranchPC :: Entity -> TcCodeM [(ActorPolicy, String)]
 getBranchPC e = do env <- getEnv
                    -- debugTcCodeM $ "Env: " ++ show env
                    return $ branchPC (Just e) env
 
-getBranchPC_ :: TcCodeM r [(ActorPolicy, String)]
+getBranchPC_ :: TcCodeM [(ActorPolicy, String)]
 getBranchPC_ = do env <- getEnv
                   return $ branchPC Nothing env
 
-extendBranchPC :: ActorPolicy -> String -> TcCodeM r a -> TcCodeM r a
+extendBranchPC :: ActorPolicy -> String -> TcCodeM a -> TcCodeM a
 extendBranchPC p str = withEnv $ joinBranchPC p str
 
-addBranchPCList :: [Ident ()] -> TcCodeM r a -> TcCodeM r a
+addBranchPCList :: [Ident ()] -> TcCodeM a -> TcCodeM a
 addBranchPCList is =
     withEnv $ \env ->
         let (bm, def) = branchPCE env
             newBm = foldl (\m i -> Map.insert (VarEntity (mkSimpleName EName i)) [] m) bm is
         in env { branchPCE = (newBm, def) }
 
-addBranchPC :: Entity -> TcCodeM r a -> TcCodeM r a
+addBranchPC :: Entity -> TcCodeM a -> TcCodeM a
 addBranchPC ent = 
     withEnv $ \env -> 
         let (bm, def) = branchPCE env
             newBm = Map.insert ent [] bm
         in env { branchPCE = (newBm, def) }
 
-getCurrentPC :: Entity -> TcCodeM r ActorPolicy
+getCurrentPC :: Entity -> TcCodeM ActorPolicy
 getCurrentPC ent = do
   bpcs <- fst . unzip <$> getBranchPC ent
   epcs <- fst . unzip <$> getExnPC
   return $ foldl join bottom (bpcs ++ epcs)
 
 {-- Tying the knot for member policies
-setFieldPol :: Ident -> TcPolicy -> TcCodeM r ()
+setFieldPol :: Ident -> TcPolicy -> TcCodeM ()
 setFieldPol i pF = do
   fMap <- (fields . typemap) <$> getEnv
   case Map.lookup (Name [i]) fMap of
@@ -537,7 +535,7 @@
             Just _  -> fail "panic: field policy already written when tying the knot"
         _ -> fail "panic: field policy already set when tying the knot"
       
-setMethodPols :: Ident -> TcPolicy -> TcPolicy -> TcCodeM r ()
+setMethodPols :: Ident -> TcPolicy -> TcPolicy -> TcCodeM ()
 setMethodPols i retM 
 -}
 
@@ -546,40 +544,40 @@
 --------------------------------------------
 {-
 -- Leave actor mappings from fields
-startState :: TcCodeM r ()
+startState :: TcCodeM ()
 startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty }
 -}
 
 -- Actor Analysis
 
-getActorId :: Name () -> TcCodeM r ActorId
+getActorId :: Name () -> TcCodeM ActorId
 getActorId n = do
   actorMap <- actorSt <$> getState
   case Map.lookup n actorMap of
     Nothing -> liftTcDeclM $ aliasActorId
     Just ai -> return $ aID ai
 
-setActorId :: Name () -> ActorId -> TcCodeM r ()
+setActorId :: Name () -> ActorId -> TcCodeM ()
 setActorId n aid = updateState setAct
   where setAct :: CodeState -> CodeState
         setAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap }
         replId (AI _ st) = AI aid st
 
 
-newActorIdWith :: Ident () -> ActorId -> TcCodeM r ()
+newActorIdWith :: Ident () -> ActorId -> TcCodeM ()
 newActorIdWith i aid = do
   updateState insertAct
       where insertAct :: CodeState -> CodeState
             insertAct s@(CodeState { actorSt = actMap }) = 
                 s { actorSt = Map.insert (mkSimpleName EName i) (AI aid Stable) actMap }
 
-newActorId :: Ident () -> TcCodeM r ActorId
+newActorId :: Ident () -> TcCodeM ActorId
 newActorId i = do 
   aid <- liftTcDeclM $ freshActorId (prettyPrint i)
   newActorIdWith i aid
   return aid
 
-newAliasId :: Ident () -> TcCodeM r ActorId
+newAliasId :: Ident () -> TcCodeM ActorId
 newAliasId i = do
   aid <- liftTcDeclM aliasActorId
   newActorIdWith i aid
@@ -587,7 +585,7 @@
 
 
 
-scrambleActors :: Maybe TcType -> TcCodeM r ()
+scrambleActors :: Maybe TcType -> TcCodeM ()
 scrambleActors mtc = do
   let stb = maybe FullV (FieldV . Just . typeName_) mtc
   state <- getState
@@ -597,10 +595,10 @@
 
 -- Exception tracking
 
-getExnPC :: TcCodeM r [(ActorPolicy, String)]
+getExnPC :: TcCodeM [(ActorPolicy, String)]
 getExnPC = exnPC <$> getState
 
-throwExn :: ExnType -> ActorPolicy -> TcCodeM r ()
+throwExn :: ExnType -> ActorPolicy -> TcCodeM ()
 throwExn et pX = do
   uref <- getUniqRef
   state <- getState
@@ -609,7 +607,7 @@
   mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap
   setState $ state { exnS = mergedXmap }
   
-deactivateExn :: ExnType -> TcCodeM r ()
+deactivateExn :: ExnType -> TcCodeM ()
 deactivateExn et = 
     updateState $ \s -> 
         let oldEmap = exnS s
@@ -617,7 +615,7 @@
         in s { exnS = newEmap }
   
 
-activateExns :: [(ExnType, ExnSig)] -> TcCodeM r ()
+activateExns :: [(ExnType, ExnSig)] -> TcCodeM ()
 activateExns exns = do
   uref <- getUniqRef
   state <- getState
@@ -631,44 +629,44 @@
   mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap
   setState $ state { exnS = mergedXmap }
 
-getExnState :: ExnType -> TcCodeM r (Maybe CodeState)
+getExnState :: ExnType -> TcCodeM (Maybe CodeState)
 getExnState et = do
   eMap <- exnS <$> getState
   return $ epState <$> Map.lookup et eMap
 
-mergeActiveExnStates :: TcCodeM r ()
+mergeActiveExnStates :: TcCodeM ()
 mergeActiveExnStates = do
   exnMap <- exnS <$> getState
   mapM_ (mergeWithState . epState) $ Map.elems exnMap
 
-useExnState :: CodeState -> TcCodeM r ()
+useExnState :: CodeState -> TcCodeM ()
 useExnState es = updateState (\s -> s { exnS = exnS es })
 
 -- Lockstate tracking
 
-getCurrentLockState :: TcCodeM r [TcLock]
+getCurrentLockState :: TcCodeM [TcLock]
 getCurrentLockState = do
   base <- lockstate <$> getEnv
   mods <- lockMods <$> getState
   return $ snd $ ([], base) ||>> mods
 
-applyLockMods :: LockMods -> TcCodeM r ()
+applyLockMods :: LockMods -> TcCodeM ()
 applyLockMods lms = do
   updateState $ \s -> s { lockMods = lockMods s ||>> lms }
 
-openLock, closeLock :: TcLock -> TcCodeM r ()
+openLock, closeLock :: TcLock -> TcCodeM ()
 openLock  l = applyLockMods ([],[l])
 closeLock l = applyLockMods ([l],[])
 
 -- Policy inference
 
-newMetaPolVar :: TcCodeM r ActorPolicy
+newMetaPolVar :: TcCodeM ActorPolicy
 newMetaPolVar = do
   uniq <- liftIO . getUniq =<< getUniqRef
   ref  <- liftIO (newIORef Nothing)
   return $ VarPolicy (TcMetaVar uniq ref)
 
---newRigidPolVar :: TcCodeM r TcPolicy
+--newRigidPolVar :: TcCodeM TcPolicy
 --newRigidPolVar = do
 --  uniq <- lift . getUniq =<< getUniqRef
 --  return $ TcRigidVar uniq
@@ -677,26 +675,22 @@
 --       Working with constraints         --
 --------------------------------------------
 
-constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM r ()
+constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM ()
 constraint ls p q str = do -- addConstraint $ LRT ls p1 p2
   g <- getGlobalLockProps
   case lrt g ls p q of
     Left b -> do
 --      debugTc $ "constraint: p1: " ++ show p1
 --      debugTc $ "constraint: p2: " ++ show p2
-      check b str {-
-                $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)
-                 "\n* p = " ++ prettyPrint p1 ++
-                 "\n* q = " ++ prettyPrint p2 ++
-                 "\nin the presence of lock state {" ++
-                   concat (intersperse ", " (map prettyPrint ls)) ++ "}" -}
+      -- st <- getState
+      check b (str {-++ "\n\nState: " ++ show st -})
     Right c -> addConstraint c str
 
-getGlobalLockProps :: TcCodeM r (PrgPolicy TcAtom)
+getGlobalLockProps :: TcCodeM [TcClause TcAtom]
 getGlobalLockProps = do
   cs <- go <$> getTypeMap
   debugPrint $ "Fetching global lock props: " ++ show cs
-  return $ TcPolicy cs
+  return cs
       where go :: TypeMap -> [TcClause TcAtom]
             go tm = let lps = map lProps $ Map.elems $ locks tm
                         tlps = map (go . tMembers . snd) $ Map.elems $ types tm
@@ -706,21 +700,21 @@
 locksToRec :: [TcLock] -> (PrgPolicy TcAtom)
 locksToRec ls = TcPolicy (map (\x -> TcClause x []) (map lockToAtom ls))
 
-constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM r ()
+constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM ()
 constraintLS p1 p2 str = do
   l <- getCurrentLockState
   withErrCtxt ("In the context of lock state: " ++ prettyPrint l ++ "\n") $
     constraint l p1 p2 str
 
-constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM r ()
+constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM ()
 constraintPC bpcs pW msgf = mapM_ (uncurry constraintPC_) bpcs
-    where constraintPC_ :: ActorPolicy -> String -> TcCodeM r ()
+    where constraintPC_ :: ActorPolicy -> String -> TcCodeM ()
           -- Don't take lock state into account
           constraintPC_ pPC src = constraint [] pPC pW (msgf pPC src)
   
 
 
-exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM r ()
+exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM ()
 exnConsistent caller exnTy (ExnSig rX wX _) = do
     exnMap <- exnsE <$> getEnv
     --debugTc $ "Using exnMap: " ++ show exnMap
@@ -754,7 +748,7 @@
 -- We don't give crap about backwards compatibility here, and even if we
 -- did, we would have to rule it out because it would be unsound.
 
-isAssignableTo, (=<:) :: (Monad (m r), MonadTcDeclM m) => TcType -> TcType -> m r Bool
+isAssignableTo, (=<:) :: MonadTcDeclM m => TcType -> TcType -> m Bool
 isAssignableTo t1 t2 = liftTcDeclM $ 
     if t1 == t2 -- identity conversion
      then return True
@@ -762,10 +756,10 @@
 
 (=<:) = flip isAssignableTo
 
-isCastableTo, (<<:) :: (Monad (m r), MonadTcDeclM m) 
+isCastableTo, (<<:) :: MonadTcDeclM m
                     => TcType 
                         -> TcType 
-                        -> m r (Bool, Bool) -- (Can be cast, needs reference narrowing)
+                        -> m (Bool, Bool) -- (Can be cast, needs reference narrowing)
 isCastableTo t1 t2 = liftTcDeclM $ do
   -- 'isAssignableTo' handles the cases of identity, primitive widening,
   -- boxing + reference widening and unboxing + primitive widening.
@@ -801,7 +795,7 @@
 -- 2) rt/rt -> widening reference conversion
 -- 3) pt/rt -> boxing conversion + widening reference conversion
 -- 4) rt/pt -> unboxing conversion + widening primitive conversion
-widensTo :: TcType -> TcType -> TcDeclM r Bool
+widensTo :: TcType -> TcType -> TcDeclM Bool
 widensTo (TcPrimT pt1) (TcPrimT pt2) = return $ pt2 `elem` widenConvert pt1
 widensTo (TcRefT   rt1) (TcRefT   rt2) = rt1 `subTypeOf` rt2
 widensTo (TcPrimT pt1) t2@(TcRefT _) = 
@@ -818,10 +812,10 @@
                | isActorType  t1 && t2 == actorT   = return True
 widensTo _ _ = return False
 
-subTypeOf :: TcRefType -> TcRefType -> TcDeclM r Bool
+subTypeOf :: TcRefType -> TcRefType -> TcDeclM Bool
 subTypeOf TcNullT _ = return True
 subTypeOf rt1 rt2 = (rt2 `elem`) <$> ([TcClsRefT objectT] ++) <$> superTypes rt1
-  where superTypes :: TcRefType -> TcDeclM r [TcRefType]
+  where superTypes :: TcRefType -> TcDeclM [TcRefType]
         superTypes rt = do
           tm <- getTypeMap
           tsig <- case lookupTypeOfRefT rt tm of
@@ -874,7 +868,7 @@
 
 
 {-
-solve :: [ConstraintWMsg] -> TcDeclM r ()
+solve :: [ConstraintWMsg] -> TcDeclM ()
 solve cs =
     liftIO $ do
       wcs <- return [(p, q) | (LRT _ p q, _) <- cs]
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs
@@ -9,7 +9,6 @@
      getEnv, withEnv,                                  -- Reader
      getState, setState, updateState, mergeWithState,  -- State
      addConstraint,                                    -- Writer
-     tryCatch,                                         -- Error
 
 --     withTypeMapAlwaysC, 
 
@@ -41,7 +40,7 @@
 -------------------------------------------------
 -- All the cool methods of this monad
 
-setupStartState :: TcDeclM r CodeState
+setupStartState :: TcDeclM CodeState
 setupStartState = do
   tm <- getTypeMap
   let aMap = gatherActorInfo tm
@@ -86,19 +85,15 @@
 
 -- Running in parallel
 infix 1 |||
-(|||) :: TcCodeM r a -> TcCodeM r b -> TcCodeM r (a,b)
+(|||) :: TcCodeM a -> TcCodeM b -> TcCodeM (a,b)
 (TcCodeM f1) ||| (TcCodeM f2) = 
-    TcCodeM $ \ec te ts -> do
-      esa <- f1 ec te ts
-      esb <- f2 ec te ts
-      case (esa, esb) of
-        (Right (a, ts1, cs1), Right (b, ts2, cs2)) -> do
-                          ts' <- mergeStatesDecl ts1 ts2
-                          return $ Right ((a,b), ts', cs1 ++ cs2)
-        (Left err, _) -> return $ Left err
-        (_, Left err) -> return $ Left err
+    TcCodeM $ \te ts -> do
+      (a, ts1, cs1) <- f1 te ts
+      (b, ts2, cs2) <- f2 te ts
+      ts' <- mergeStatesDecl ts1 ts2
+      return ((a,b), ts', cs1 ++ cs2)
 
-mergeStatesDecl :: CodeState -> CodeState -> TcDeclM r CodeState
+mergeStatesDecl :: CodeState -> CodeState -> TcDeclM CodeState
 mergeStatesDecl s1 s2 = do
   u <- getUniqRef
   liftIO $ mergeStates u s1 s2
@@ -111,92 +106,77 @@
 --------------------------------------------------
 -- The monad used for typechecking code snippets
 
-newtype TcCodeM r a = 
-    TcCodeM (ErrCtxt -> CodeEnv -> CodeState -> TcDeclM r (Either String (a, CodeState, [ConstraintWMsg])))
+newtype TcCodeM a = 
+    TcCodeM (CodeEnv -> CodeState -> TcDeclM (a, CodeState, [ConstraintWMsg]))
 
-runTcCodeM :: CodeEnv -> CodeState -> TcCodeM r a -> TcDeclM r (a, [ConstraintWMsg])
+runTcCodeM :: CodeEnv -> CodeState -> TcCodeM a -> TcDeclM (a, [ConstraintWMsg])
 runTcCodeM env state (TcCodeM f) = do
-  esa <- f id env state
-  case esa of
-    Left err -> fail err
-    Right (a,_,cs) -> return (a, cs)
+  (a,_,cs) <- f env state
+  return (a, cs)
 
-instance Monad (TcCodeM r) where
-  return x = TcCodeM $ \_ _ s -> return (Right (x, s, []))
+instance Monad TcCodeM where
+  return x = TcCodeM $ \_ s -> return (x, s, [])
 
-  TcCodeM f >>= h = TcCodeM $ \ec e s0 -> do
-                      esa <- f ec e s0
-                      case esa of
-                        Left err -> return $ Left err
-                        Right (a, s1, cs1) -> do
-                            let TcCodeM g = h a
-                            esb <- g ec e s1
-                            case esb of
-                              Left err -> return $ Left err
-                              Right (b, s2, cs2) -> return $ Right (b, s2, cs1 ++ cs2)
+  TcCodeM f >>= h = TcCodeM $ \e s0 -> do
+                      (a, s1, cs1) <- f e s0
+                      let TcCodeM g = h a
+                      (b, s2, cs2) <- g e s1
+                      return (b, s2, cs1 ++ cs2)
 
-  fail err = TcCodeM $ \ec _ _ -> return (Left $ ec err) -- TcCodeM $ \_ _ -> fail err
+  fail err = TcCodeM $ \_ _ -> fail err
 
-instance Functor (TcCodeM r) where
+instance Functor TcCodeM where
   fmap = liftM
 
-instance Applicative (TcCodeM r) where
+instance Applicative TcCodeM where
   (<*>) = ap
   pure = return
 
-instance MonadIO (TcCodeM r) where
+instance MonadIO TcCodeM where
   liftIO = liftTcDeclM . liftIO
 
-instance MonadBase (TcCodeM r) where
+instance MonadBase TcCodeM where
   liftBase = liftTcDeclM . liftBase
-  withErrCtxt' ecf (TcCodeM f) = TcCodeM $ \ec e s -> (f (ecf ec) e s)
+  withErrCtxt' ecf (TcCodeM f) = TcCodeM $ \e s -> withErrCtxt' ecf (f e s)
+  tryM (TcCodeM f) = TcCodeM $ \e s -> do
+                             esa <- tryM $ f e s
+                             case esa of
+                               Right (a, s', cs) -> return (Right a, s', cs)
+                               Left err -> return (Left err, s, [])
 
-instance MonadPR (TcCodeM r) where
+instance MonadPR TcCodeM where
   liftPR = liftTcDeclM . liftPR
 
-instance MonadTcBaseM (TcCodeM r) where
-  liftTcBaseM = liftTcDeclM . liftTcBaseM
-  withTypeMap tmf (TcCodeM f) = TcCodeM $ \ec e s -> withTypeMap tmf (f ec e s)
+--instance MonadTcBaseM TcCodeM where
+--  liftTcBaseM = liftTcDeclM . liftTcBaseM
+--  withTypeMap tmf (TcCodeM f) = TcCodeM $ \ec e s -> withTypeMap tmf (f ec e s)
 
 instance MonadTcDeclM TcCodeM where
-  liftTcDeclM tdm = TcCodeM $ \_ _ s -> Right . (,s,[]) <$> tdm
-
-{-
-liftCallCC :: ((((a, CodeState, [ConstraintWMsg]) -> TcDeclM r (b, CodeState, [ConstraintWMsg]))
-                 -> TcDeclM r (a, CodeState, [ConstraintWMsg]))
-                  -> TcDeclM r (a, CodeState, [ConstraintWMsg]))
-              -> ((a -> TcCodeM r b) -> TcCodeM r a) -> TcCodeM r a
-liftCallCC ccc k = TcCodeM $ \e s -> ccc $ \c ->
-                       let (TcCodeM f) = k (\a -> TcCodeM $ \_ _ -> c (a, s, []))
-                       in f e s
-
-withTypeMapAlwaysC :: (TypeMap -> TypeMap) -> TcCodeM r a -> TcCodeM r a
-withTypeMapAlwaysC tmf tcm = liftCallCC callCC $ \cont -> do
-                               withTypeMap tmf $ tcm >>= cont
--}
+  liftTcDeclM tdm = TcCodeM $ \_ s -> (,s,[]) <$> tdm
+  withCurrentTypeMap tmf (TcCodeM f) = TcCodeM $ \e s -> withCurrentTypeMap tmf (f e s)
 
 
 -- The environment
 
-getEnv :: TcCodeM r CodeEnv
-getEnv = TcCodeM (\_ e s -> return $ Right (e,s,[]))
+getEnv :: TcCodeM CodeEnv
+getEnv = TcCodeM (\e s -> return (e,s,[]))
 
-withEnv :: (CodeEnv -> CodeEnv) -> TcCodeM r a -> TcCodeM r a
-withEnv k (TcCodeM f) = TcCodeM $ \ec -> (f ec . k)
+withEnv :: (CodeEnv -> CodeEnv) -> TcCodeM a -> TcCodeM a
+withEnv k (TcCodeM f) = TcCodeM $ f . k
 
 
 -- The state
 
-getState :: TcCodeM r CodeState
-getState = TcCodeM (\_ _ s -> return $ Right (s,s,[]))
+getState :: TcCodeM CodeState
+getState = TcCodeM (\_ s -> return (s,s,[]))
 
-setState :: CodeState -> TcCodeM r ()
-setState s = TcCodeM (\_ _ _ -> return $ Right ((),s,[]))
+setState :: CodeState -> TcCodeM ()
+setState s = TcCodeM (\_ _ -> return ((),s,[]))
 
-updateState :: (CodeState -> CodeState) -> TcCodeM r ()
+updateState :: (CodeState -> CodeState) -> TcCodeM ()
 updateState f = getState >>= return . f >>= setState
 
-mergeWithState :: CodeState -> TcCodeM r ()
+mergeWithState :: CodeState -> TcCodeM ()
 mergeWithState s = do
   sOld <- getState
   sNew <- liftTcDeclM $ mergeStatesDecl sOld s
@@ -204,12 +184,12 @@
 
 -- Constraints
 
-addConstraint :: Constraint -> String -> TcCodeM r ()
-addConstraint c str = TcCodeM (\_ _ s -> return $ Right ((), s, [(c,str)]))
+addConstraint :: Constraint -> String -> TcCodeM ()
+addConstraint c str = TcCodeM (\_ s -> return ((), s, [(c,str)]))
 
 -- Exceptions
-
-tryCatch :: TcCodeM r a -> (String -> TcCodeM r a) -> TcCodeM r a
+{-
+tryCatch :: TcCodeM a -> (String -> TcCodeM a) -> TcCodeM a
 tryCatch (TcCodeM f) ctch = TcCodeM $ \ec e s -> do
                               esa <- f ec e s
                               case esa of
@@ -217,4 +197,4 @@
                                 Left err -> do
                                          let TcCodeM g = ctch err
                                          g ec e s
-
+-}
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs
@@ -5,13 +5,14 @@
 
      TcDeclM, runTcDeclM, TypeCheck,
 
-     MonadTcDeclM(..), MonadTcBaseM(..),
+     MonadTcDeclM(..), -- MonadTcBaseM(..),
 
-     callCC, withTypeMapAlways,
      fetchPkg, fetchType,
 
      getTypeMap, getThisType, getSuperType, lookupTypeOfType,
 
+     withTypeParam, extendGlobalTypeMap,
+
      evalSrcType, evalSrcRefType, evalSrcClsType,
      evalSrcTypeArg, evalSrcNWTypeArg,
      evalReturnType,
@@ -52,8 +53,8 @@
 
 type TypeCheck m ast = ast () -> m (ast T)
 
-lookupTypeOfType :: MonadTcBaseM m => TcType -> m TypeSig
-lookupTypeOfType ty = liftTcBaseM $ do
+lookupTypeOfType :: MonadTcDeclM m => TcType -> m TypeSig
+lookupTypeOfType ty = liftTcDeclM $ do
   tm <- getTypeMap
   debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm
   case lookupTypeOfT ty tm of
@@ -62,20 +63,21 @@
     Left (Just err) -> fail err
 
 
-fetchPkg :: Name () -> TcDeclM r ()
+fetchPkg :: Name () -> TcDeclM ()
 fetchPkg n = do
   debugPrint $ "Fetching package " ++ prettyPrint n ++ " ..."
   isP <- doesPkgExist n
   if not isP
    then fail $ "No such package: " ++ prettyPrint n
    else do
-     withTypeMapAlways (extendTypeMapP n emptyTM) $ do
-               debugPrint $ "Done fetching package " ++ prettyPrint n
-               return ()
+     extendGlobalTypeMap (extendTypeMapP n emptyTM)
+     debugPrint $ "Done fetching package " ++ prettyPrint n
+     return ()
                        
 
-fetchType :: Name () -> TcDeclM r ([TypeParam ()], TypeSig)
+fetchType :: Name () -> TcDeclM ([TypeParam ()], TypeSig)
 fetchType n@(Name _ _ _ typName) = do
+  withFreshCurrentTypeMap $ do
   debugPrint $ "Fetching type " ++ prettyPrint n ++ " ..."
   isT <- doesTypeExist n
   if not isT
@@ -110,30 +112,30 @@
                             tImpls   = implsTys,
                             tMembers = superTm { constrs = Map.empty }
                           }
-               (rtps,rsig) <- withTypeMapAlways (extendTypeMapT n tps tsig) $ do
-                                withFoldMap withTypeParam tps $ do
-                                     let mDs = map unMemberDecl ds
-                                     -- These will be written directly into the right
-                                     -- places in" the TM, using the 'always' trick
-                                     fetchActors n mDs
-                                     fetchLocks  n mDs
-                                     fetchPols   n mDs
-                                     fetchTypeMethods n mDs
-                                     fetchSignatures  n mDs
+               extendGlobalTypeMap (extendTypeMapT n tps tsig)
 
-                                     tm <- getTypeMap
-                                     case lookupNamed types n tm of
-                                       Just res -> do
-                                         debugPrint $ "Done fetching type: " ++ prettyPrint n
-                                         debugPrint $ "Result: " ++ show res ++ "\n"
-                                         return res
-                                       Nothing  -> panic (tcDeclMModule ++ ".fetchType") $
-                                                   "Just fetched type " ++ show n ++ 
-                                                   " but now it doesn't exist!"
-               withTypeMapAlways (extendTypeMapT n rtps rsig) $ do
+--               (rtps,rsig) <- withTypeMapAlways (extendTypeMapT n tps tsig) $ do
+               withFoldMap withTypeParam tps $ do
+                 let mDs = map unMemberDecl ds
+                 fetchActors n mDs $ do
+                 fetchLocks  n mDs $ do
+                 fetchPols   n mDs $ do
+                 fetchTypeMethods n mDs $ do
+                 fetchSignatures  n mDs
+
                  tm <- getTypeMap
-                 debugPrint $ "TypeMap here: " ++ show tm ++ "\n"
-                 return (rtps,rsig)
+                 case lookupNamed types n tm of
+                   Just res -> do
+                     debugPrint $ "Done fetching type: " ++ prettyPrint n
+                     debugPrint $ "Result: " ++ show res ++ "\n"
+                     return res
+                   Nothing  -> panic (tcDeclMModule ++ ".fetchType") $
+                               "Just fetched type " ++ show n ++ 
+                              " but now it doesn't exist!"
+--               withTypeMapAlways (extendTypeMapT n rtps rsig) $ do
+--                 tm <- getTypeMap
+--                 debugPrint $ "TypeMap here: " ++ show tm ++ "\n"
+--                 return (rtps,rsig)
                
               where unMemberDecl :: Decl () -> MemberDecl ()
                     unMemberDecl (MemberDecl _ md) = md
@@ -159,14 +161,17 @@
                             tImpls   = [],
                             tMembers = superTm
                           }
-               withTypeMapAlways (extendTypeMapT n tps tsig) $ do
-                withFoldMap withTypeParam tps $ do
+
+               extendGlobalTypeMap (extendTypeMapT n tps tsig)
+
+--               withTypeMapAlways (extendTypeMapT n tps tsig) $ do
+               withFoldMap withTypeParam tps $ do
                  -- These will be written directly into the right
                  -- places in the TM, using the 'always' trick
-                 fetchActors n mDs
-                 fetchLocks  n mDs
-                 fetchPols   n mDs
-                 fetchTypeMethods n mDs
+                 fetchActors n mDs $ do
+                 fetchLocks  n mDs $ do
+                 fetchPols   n mDs $ do
+                 fetchTypeMethods n mDs $ do
                  fetchSignatures  n mDs
 
                  tm <- getTypeMap
@@ -175,14 +180,15 @@
                    Nothing  -> panic (tcDeclMModule ++ ".fetchType") $
                                "Just fetched type " ++ show n ++ 
                                " but now it doesn't exist!"
+
        _ -> fail $ "Enums not yet supported"
 
 fetchType n = panic (tcDeclMModule ++ ".fetchType") $ show n
 
 -- Actors
 
-fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM r ()
-fetchActors n mDecls = do
+fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a
+fetchActors n mDecls tdra = do
     --debug "fetchActors"
     let acts = [ (ms, vd) 
                      | FieldDecl _ ms (PrimType _ (ActorT _)) vds <- mDecls 
@@ -190,22 +196,30 @@
                      , Final () `elem` ms -- Static () `elem` ms 
                ]
     let -- (sfs,unstables)  = partition (\(ms, _) -> Final () `elem` ms) acts
-        (spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs
+        (spawns  , stables ) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs
+        (sspawns , fspawns ) = partition (\(ms,_) -> Static () `elem` ms) spawns
+        (sstables, fstables) = partition (\(ms,_) -> Static () `elem` ms) stables
                                
-    (sas, svs) <- unzip <$> mapM spawnActorVd spawns
+    (ssas, ssvs) <- unzip <$> mapM spawnActorVd sspawns
+    (fsas, fsvs) <- unzip <$> mapM spawnActorVd fspawns
+    (seas, sevs) <- unzip <$> mapM evalActorVd  sstables
+    (feas, fevs) <- unzip <$> mapM evalActorVd  fstables
 --    (aas, avs) <- unzip <$> mapM aliasActorVd unstables
-    (eas, evs) <- unzip <$> mapM evalActorVd stables
-    withTypeMapAlways (extendTypeMapN n . merge $
---                         (\tm -> tm
-                           emptyTM { actors = Map.fromList (sas {- ++ aas -} ++ eas),
-                                     fields = Map.fromList (svs {- ++ avs -} ++ evs) }) $ do
-                       debugPrint "Actors fetched"
-                       return ()
+--    (eas, evs) <- unzip <$> mapM evalActorVd stables
+    let globTM = emptyTM { actors = Map.fromList (ssas ++ seas),
+                           fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) }
+        loclTM = emptyTM { actors = Map.fromList (ssas ++ fsas ++ seas ++ feas),
+                           fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) }
+
+    extendGlobalTypeMap (extendTypeMapN n $ merge globTM)
+    withCurrentTypeMap (merge loclTM) $ do
+      debugPrint "Actors fetched"
+      tdra
     
         
          where spawnActorVd, evalActorVd --, aliasActorVd
                    :: ([Modifier ()], VarDecl ())
-                   -> TcDeclM r ((Ident (), ActorId), (Ident (),VarFieldSig))
+                   -> TcDeclM ((Ident (), ActorId), (Ident (),VarFieldSig))
                   -- Only Nothing for initializer
                spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do
                  a <- freshActorId (prettyPrint i)
@@ -247,8 +261,8 @@
 
 -- locks
 
-fetchLocks :: Name () -> [MemberDecl ()] -> TcDeclM r ()
-fetchLocks n mds = do
+fetchLocks :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a
+fetchLocks n mds tdra = do
   let lcs = [ (i, ms, mps, mProps) | 
                LockDecl _ ms i mps mProps <- mds ]
   lsigs <- flip mapM lcs $ \(i, ms, mps, mProps) -> do
@@ -256,11 +270,13 @@
                      modPrs <- getLockModProps i ms
                      prs <- evalSrcLockProps i mProps
                      return (i, LSig pol (length mps) (modPrs ++ prs))
-  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { locks = Map.fromList lsigs })) $ do
-                     debugPrint $ "Locks fetched"
-                     return ()
+  let newTM = emptyTM { locks = Map.fromList lsigs }
+  extendGlobalTypeMap (extendTypeMapN n $ merge newTM)
+  withCurrentTypeMap (merge newTM) $ do
+       debugPrint $ "Locks fetched"
+       tdra
 
-getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM r [TcClause TcAtom]
+getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM [TcClause TcAtom]
 getLockModProps lockI ms = do
     let trans = evalSrcLockProps lockI $ Just [lockPropQQ| { #lockI('x,'y) : #lockI('x,'z), #lockI('z,'y) } |]
         refl  = evalSrcLockProps lockI $ Just [lockPropQQ| { #lockI('x,'x) : } |]
@@ -275,39 +291,51 @@
 
 -- policies
 
-fetchPols :: Name () -> [MemberDecl ()] -> TcDeclM r ()
-fetchPols n mds = do
-  let pols = [ (i,initz) | 
+fetchPols :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a
+fetchPols n mds tdra = do
+  let pols = [ (i,initz, Static () `elem` ms) | 
                  FieldDecl _ ms (PrimType _ (PolicyT _)) vds <- mds,
                  VarDecl _ (VarId _ i) (Just (InitExp _ initz)) <- vds,
-                 Static () `elem` ms, Final () `elem` ms
+                 Final () `elem` ms
              ]
-  ips <- mapM fetchPol pols
-  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do
+      (spols, fpols) = partition (\(_,_,b) -> b) pols
+      
+  sips <- mapM fetchPol spols
+  fips <- mapM fetchPol fpols
+
+  -- TODO: Expand local locks!
+  let globTM = emptyTM { policies = Map.fromList sips }
+      loclTM = emptyTM { policies = Map.fromList $ sips ++ fips }
+  extendGlobalTypeMap $ extendTypeMapN n $ merge globTM
+  withCurrentTypeMap (merge loclTM) $ do
+--  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do
                     debugPrint $ "Policies fetched"
-                    return ()
+                    tdra
 
-      where fetchPol :: (Ident (), Exp ()) -> TcDeclM r (Ident (), ActorPolicy)
-            fetchPol (i,e) = (i,) <$> evalPolicy e
+      where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)
+            fetchPol (i,e,_) = (i,) <$> evalPolicy e
 -- end policies
 
 -- Working with typemethods
-fetchTypeMethods :: Name () -> [MemberDecl ()] -> TcDeclM r ()
-fetchTypeMethods n mds  = do
+fetchTypeMethods :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a
+fetchTypeMethods n mds tdra = do
   let ipbs = [ (i,(ps,body)) | 
                MethodDecl _ ms _ _ i ps _ (MethodBody _ (Just body)) <- mds,
                Typemethod () `elem` ms
              ]
   ipidbs <- mapM paramsToIdents ipbs
-  withTypeMapAlways (extendTypeMapN n 
-                     (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do
+  let newTM = emptyTM { typemethods = Map.fromList ipidbs }
+  extendGlobalTypeMap $ extendTypeMapN n $ merge newTM
+  withCurrentTypeMap (merge newTM) $ do
+--  withTypeMapAlways (extendTypeMapN n 
+--                     (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do
                     debugPrint "TypeMethods fetched"
-                    return ()
+                    tdra
 
     where paramsToIdents (i, (ps,b)) = do
                               pids <- mapM paramIdent ps
                               return (i, (pids,b))
-          paramIdent :: FormalParam () -> TcDeclM r (Ident ())
+          paramIdent :: FormalParam () -> TcDeclM (Ident ())
           paramIdent (FormalParam _ _ _ _ (VarId _ i)) = return i
           paramIdent (FormalParam _ _ _ _ arvid) = 
               fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
@@ -316,28 +344,29 @@
 
 -- signatures of fields, methods and constructors
 
-fetchSignatures :: Name () -> [MemberDecl ()] -> TcDeclM r ()
+fetchSignatures :: Name () -> [MemberDecl ()] -> TcDeclM ()
 fetchSignatures n memDs = do
     fieldMap <- fetchFields memDs
     methodMap <- fetchMethods memDs
     constrMap <- fetchConstrs memDs
-    withTypeMapAlways (extendTypeMapN n (merge $ emptyTM
-                                                   { fields = fieldMap,
-                                                     methods = methodMap,
-                                                     constrs = constrMap })) $ do
-      debugPrint "Signatures fetched"
-      return ()
-
+    let newTM = emptyTM
+                { fields = fieldMap,
+                  methods = methodMap,
+                  constrs = constrMap }
+    extendGlobalTypeMap $ extendTypeMapN n $ merge newTM
+    debugPrint "Signatures fetched"
+    return ()
+    
  where
-   unVarDecl :: VarDecl () -> TcDeclM r (Ident ())
+   unVarDecl :: VarDecl () -> TcDeclM (Ident ())
    unVarDecl (VarDecl _ (VarId _ i) _) = return i
    unVarDecl arvid = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
-   fetchFields :: [MemberDecl ()] -> TcDeclM r (Map (Ident ()) VarFieldSig)
+   fetchFields :: [MemberDecl ()] -> TcDeclM (Map (Ident ()) VarFieldSig)
    fetchFields = go Map.empty
        where go :: Map (Ident ()) VarFieldSig 
                 -> [MemberDecl ()] 
-                -> TcDeclM r (Map (Ident ()) VarFieldSig)
+                -> TcDeclM (Map (Ident ()) VarFieldSig)
              go acc [] = return acc
              go fm (md:mds) = 
                  case md of
@@ -352,11 +381,11 @@
                    _ -> go fm mds
 
    fetchMethods :: [MemberDecl ()] 
-                -> TcDeclM r (Map (Ident ()) MethodMap) 
+                -> TcDeclM (Map (Ident ()) MethodMap) 
    fetchMethods = go Map.empty
        where go :: Map (Ident ()) MethodMap
                 -> [MemberDecl ()]
-                -> TcDeclM r (Map (Ident ()) MethodMap)
+                -> TcDeclM (Map (Ident ()) MethodMap)
              go acc [] = return acc
              go mm (md:mds) = 
                  case md of
@@ -391,7 +420,7 @@
    fetchConstrs = go Map.empty
        where go :: ConstrMap
                 -> [MemberDecl ()]
-                -> TcDeclM r ConstrMap
+                -> TcDeclM ConstrMap
              go acc [] = return acc
              go cm (md:mds) = 
                  case md of
@@ -419,7 +448,7 @@
                    _ -> go cm mds        
              
  
-   eSpecToSig :: ExceptionSpec () -> TcDeclM r (TcType, ExnSig)
+   eSpecToSig :: ExceptionSpec () -> TcDeclM (TcType, ExnSig)
    eSpecToSig (ExceptionSpec _ ms eType) = do
           ty <- evalSrcType (RefType () eType) -- should use evalSrcRefType
           rPol <- getReadPolicy ms
@@ -433,7 +462,7 @@
                      }
           return (ty, esig)
 
-   paramInfo :: FormalParam () -> TcDeclM r (TcType, ActorPolicy)
+   paramInfo :: FormalParam () -> TcDeclM (TcType, ActorPolicy)
    paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do
           pPol <- getParamPolicy i ms
           pTy  <- evalSrcType ty
@@ -441,31 +470,31 @@
    paramInfo (FormalParam _ _ _ _ arvid) = 
             fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
-withTypeParam :: TypeParam () -> TcDeclM r a -> TcDeclM r a
+withTypeParam :: TypeParam () -> TcDeclM a -> TcDeclM a
 withTypeParam tp tcba = 
     case tp of
       ActorParam _ i -> do
           let vti = VSig actorT top False False True
-          withTypeMap (\tm -> 
+          withCurrentTypeMap (\tm -> 
               tm { actors = Map.insert i (ActorTPVar i) (actors tm),
                    fields = Map.insert i vti (fields tm) }) $ tcba
       PolicyParam _ i -> do
            let vti = VSig policyT top False False True
-           withTypeMap (\tm ->
+           withCurrentTypeMap (\tm ->
               tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),
                    fields = Map.insert i vti (fields tm) }) $ tcba
       LockStateParam _ i -> do
           let vti = VSig (lockT []) top False False True
-          withTypeMap (\tm ->
+          withCurrentTypeMap (\tm ->
               tm { fields = Map.insert i vti (fields tm) }) $ tcba
       TypeParam _ _i _ -> do
-          --withTypeMap (\tm ->
+          --withCurrentTypeMap (\tm ->
           --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $ 
             tcba
 
 
 {-
-fetchSignature :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
+fetchSignature :: MemberDecl () -> TcDeclM a -> TcDeclM a
 fetchSignature memDecl tcba = do
 
     --debug $ "fetchSignature: " ++ show memberDecl
@@ -531,7 +560,7 @@
       LockDecl {} -> fail "Lock properties not yet supported"
       _ -> fail "Inner classes not yet supported"
 
-  where eSpecToSig :: ExceptionSpec () -> TcDeclM r (TcType, ExnSig)
+  where eSpecToSig :: ExceptionSpec () -> TcDeclM (TcType, ExnSig)
         eSpecToSig (ExceptionSpec _ ms eType) = do
           ty <- evalSrcType (RefType () eType) -- should use evalSrcRefType
           rPol <- getReadPolicy ms
@@ -545,7 +574,7 @@
                      }
           return (ty, esig)
 
-        paramInfo :: FormalParam () -> TcDeclM r (TcType, TcPolicy)
+        paramInfo :: FormalParam () -> TcDeclM (TcType, TcPolicy)
         paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do
           pPol <- getParamPolicy i ms
           pTy  <- evalSrcType ty
@@ -559,7 +588,7 @@
 ------------------------------------------------------------
 
 -------------------------------------------------------------------------------------      
-getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM r ActorPolicy
+getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM ActorPolicy
 getReadPolicy mods = 
     case [pol |Reads _ pol <- mods ] of -- !!0 -- Read Policy? what if no read policy?
       [pol] -> evalPolicy pol
@@ -578,14 +607,14 @@
       [] -> return top
       _ -> fail "At most one read modifier allowed per lock"
 
-getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM r ActorPolicy
+getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM ActorPolicy
 getParamPolicy i mods =
     case [pol | Reads _ pol <- mods ] of
        [pol] -> evalPolicy pol
        [] -> return $ ofPol i
        _ -> fail "At most one read modifier allowed per parameter"
 
-getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM r ActorPolicy
+getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM ActorPolicy
 getReturnPolicy mods pPols = 
     case [pol | Reads _ pol <- mods ] of
       [pol] -> evalPolicy pol
@@ -598,16 +627,16 @@
 -------------------------------------------------------------------
 -- Evaluating types
 
-evalReturnType :: Maybe (Type ()) -> TcDeclM r TcType
+evalReturnType :: Maybe (Type ()) -> TcDeclM TcType
 evalReturnType = maybe (return voidT) evalSrcType
 
-evalSrcType :: Type () -> TcDeclM r TcType
+evalSrcType :: Type () -> TcDeclM TcType
 evalSrcType (PrimType _ pt) = return $ TcPrimT pt
 evalSrcType (RefType  _ rt) = TcRefT <$> evalSrcRefType rt
 evalSrcType _ = panic (tcDeclMModule ++ ".evalSrcType")
                 "AntiQType should not appear in AST being type-checked"
 
-evalSrcRefType :: RefType () -> TcDeclM r TcRefType
+evalSrcRefType :: RefType () -> TcDeclM TcRefType
 evalSrcRefType (TypeVariable _ i) = return $ TcTypeVar i
 evalSrcRefType (ArrayType _ t mps) = do
   ty <- evalSrcType t
@@ -616,7 +645,7 @@
   return arrTy
 evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct
 
-evalSrcClsType :: ClassType () -> TcDeclM r TcClassType
+evalSrcClsType :: ClassType () -> TcDeclM TcClassType
 evalSrcClsType ct@(ClassType _ n tas) = do
   debugPrint $ "Evaluating class type: " ++ show ct
   baseTm <- getTypeMap
@@ -634,7 +663,7 @@
       where aux :: TypeMap                            -- Typemap of outer type (or top-level)
                 -> [(Ident (), [TcTypeArg])]          -- Accumulated type (reversed)
                 -> [(Ident (), [TypeArgument ()])]    -- Type to traverse
-                -> TcDeclM r [(Ident (), [TcTypeArg])] -- Result (re-reversed)
+                -> TcDeclM [(Ident (), [TcTypeArg])] -- Result (re-reversed)
             aux _ accTy [] = return $ reverse accTy
             aux tm accTy ((i,tas):rest) = do
                  debug $ "Looking up type: " ++ show i
@@ -656,11 +685,11 @@
 
 --    TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs
 -}      
-evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcDeclM r TcTypeArg
+evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcDeclM TcTypeArg
 evalSrcTypeArg tp (ActualArg _ a) = evalSrcNWTypeArg tp a
 evalSrcTypeArg _ _ = fail "evalSrcTypeArg: Wildcards not yet supported"
 
-evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcDeclM r TcTypeArg
+evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcDeclM TcTypeArg
 -- Types may be names or types -- TODO: Check bounds
 evalSrcNWTypeArg (TypeParam {}) (ActualName _ n) = do
     TcActualType . TcClsRefT <$> evalSrcClsType (ClassType () n [])
@@ -684,7 +713,7 @@
 evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls
 -}
 
-evalPolicy :: Exp () -> TcDeclM r ActorPolicy
+evalPolicy :: Exp () -> TcDeclM ActorPolicy
 evalPolicy e = case e of
   ExpName _ n -> do
     -- debug $ "evalPolicy: " ++ show n
@@ -707,37 +736,37 @@
   Paren _ p -> evalPolicy p
   _ -> fail "evalPolicy: More here!"
 
-evalPolicyExp :: PolicyExp () -> TcDeclM r ActorPolicy
+evalPolicyExp :: PolicyExp () -> TcDeclM ActorPolicy
 evalPolicyExp (PolicyLit _ cs) = (RealPolicy . TcPolicy) <$> mapM evalClause cs
 evalPolicyExp (PolicyOf _ i)   = return $ RealPolicy $ TcRigidVar i
 evalPolicyExp (PolicyThis _)   = return $ RealPolicy $ TcThis
 evalPolicyExp (PolicyTypeVar _ i) = return $ RealPolicy $ TcRigidVar i
 
-evalClause :: Clause () -> TcDeclM r (TcClause TcActor)
+evalClause :: Clause () -> TcDeclM (TcClause TcActor)
 evalClause (Clause _ h b) = do
   h' <- evalActor h
   b' <- mapM evalAtom b
   return $ TcClause h' b'
 
-evalActorName :: ActorName () -> TcDeclM r ActorId
+evalActorName :: ActorName () -> TcDeclM ActorId
 evalActorName (ActorName _ n) = evalActorId n
 evalActorName (ActorTypeVar _ i) = return $ ActorTPVar i
 
-evalActor :: Actor () -> TcDeclM r TcActor
+evalActor :: Actor () -> TcDeclM TcActor
 evalActor (Actor _ n) = TcActor <$> evalActorName n
 evalActor (Var _ i) = return $ TcVar i
 
-evalActorId :: Name () -> TcDeclM r ActorId
+evalActorId :: Name () -> TcDeclM ActorId
 evalActorId n = do
   tm <- getTypeMap
   case lookupNamed actors n tm of
     Just aid -> return aid
     Nothing -> aliasActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n
 
-evalAtom :: Atom () -> TcDeclM r TcAtom
+evalAtom :: Atom () -> TcDeclM TcAtom
 evalAtom (Atom _ n as) = TcAtom n <$> mapM evalActor as
 
-evalLock :: Lock () -> TcDeclM r TcLock
+evalLock :: Lock () -> TcDeclM TcLock
 evalLock (Lock _ n@(Name _ _nt mPre i) ans) = do
   tm <- case mPre of
           Nothing -> getTypeMap
@@ -765,17 +794,17 @@
 evalLock l = panic (tcDeclMModule ++ ".evalLock")
              $ show l
   
-evalSrcLockProps :: Ident () -> Maybe (LockProperties ()) -> TcDeclM r [TcClause TcAtom]
+evalSrcLockProps :: Ident () -> Maybe (LockProperties ()) -> TcDeclM [TcClause TcAtom]
 evalSrcLockProps _ Nothing = return []
 evalSrcLockProps i (Just (LockProperties _ lcs)) = do
   cs <- mapM (evalLClause i) lcs
   debugPrint $ "Properties: " ++ show cs
   return cs
 
-evalLClause :: Ident () -> LClause () -> TcDeclM r (TcClause TcAtom)
+evalLClause :: Ident () -> LClause () -> TcDeclM (TcClause TcAtom)
 evalLClause i (LClause _ h b) = TcClause <$> evalSimpleAtom i h <*> mapM evalAtom b
 
-evalSimpleAtom :: Ident () -> Atom () -> TcDeclM r TcAtom
+evalSimpleAtom :: Ident () -> Atom () -> TcDeclM TcAtom
 evalSimpleAtom i a@(Atom _ n _) = do
   case n of
     (Name _ _ Nothing aI) | aI == i -> evalAtom a
@@ -783,7 +812,7 @@
                 "\nExpected name: " ++ prettyPrint i ++
                 "\nFound name: " ++ prettyPrint n
 
-getActor :: ActorName () -> TcDeclM r ActorId
+getActor :: ActorName () -> TcDeclM ActorId
 getActor (ActorName _ n) = do
   tm <- getTypeMap
   case lookupNamed actors n tm of
@@ -791,21 +820,18 @@
     Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n
 getActor (ActorTypeVar _ i) = return $ ActorTPVar i
 
-freshActorId :: String -> TcDeclM r ActorId
+freshActorId :: String -> TcDeclM ActorId
 freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef
 
-aliasActorId :: TcDeclM r ActorId
+aliasActorId :: TcDeclM ActorId
 aliasActorId = (liftIO . newAlias) =<< getUniqRef
   
 
------------------------------------------------------
+{-----------------------------------------------------
 -- The continuation monad
 
 newtype TcDeclM r a = TcDeclM ((a -> TcBaseM r) -> TcBaseM r)
 
-runTcDeclM :: TcClassType -> TcDeclM a a -> PiReader a
-runTcDeclM ty (TcDeclM f) = runTcBaseM (f return) emptyTM ty
-
 instance Monad (TcDeclM r) where
   return x = TcDeclM $ \k -> k x
 
@@ -872,51 +898,66 @@
                             
 withTypeMapAlways tmf (TcDeclM f) = TcDeclM $ \k -> do
                                       withTypeMap tmf $ f k
-
+-}
 -----------------------------------------------
 -- Underlying non-cont'ed monad
 
-newtype TcBaseM a = TcBaseM { runTcBaseM :: TypeMap -> TcClassType -> PiReader a }
+newtype TcDeclM a = TcDeclM (TypeMap -> TypeMap -> TcClassType -> PiReader (a, TypeMap) )
 
-instance Monad TcBaseM where
+runTcDeclM :: TcClassType -> TcDeclM a -> PiReader a
+runTcDeclM ty (TcDeclM f) = fst <$> f emptyTM emptyTM ty
+
+instance Monad TcDeclM where
   return = liftPR . return
 
-  TcBaseM f >>= k = TcBaseM $ \tm ty -> do
-                       a <- f tm ty
-                       let TcBaseM g = k a
-                       g tm ty
+  TcDeclM f >>= k = TcDeclM $ \ctm gtm ty -> do
+                       (a, gtm') <- f ctm gtm ty
+                       let TcDeclM g = k a
+                       g ctm gtm' ty
 
   fail = liftPR . fail
 
-instance Functor TcBaseM where
+instance Functor TcDeclM where
   fmap = liftM
 
-instance MonadIO TcBaseM where
+instance Applicative TcDeclM where
+  pure = return
+  (<*>) = ap
+
+instance MonadIO TcDeclM where
   liftIO = liftPR . liftIO
 
-instance MonadBase TcBaseM where
+instance MonadBase TcDeclM where
   liftBase = liftPR . liftBase
+  withErrCtxt' prf (TcDeclM f) = TcDeclM $ \ctm gtm ty -> withErrCtxt' prf $ f ctm gtm ty
+  tryM (TcDeclM f) = TcDeclM $ \ctm gtm ty -> do
+                             esatm <- tryM (f ctm gtm ty)
+                             case esatm of
+                               Right (a, tm) -> return (Right a, tm)
+                               Left err -> return (Left err, gtm)
 
-  withErrCtxt' prf (TcBaseM f) = TcBaseM $ \tm ty -> withErrCtxt' prf $ f tm ty
+instance MonadPR TcDeclM where
+  liftPR pra = TcDeclM $ \_ gtm _ -> pra >>= \a -> return (a, gtm)
 
-instance MonadPR TcBaseM where
-  liftPR pra = TcBaseM $ \_ _ -> pra
+class MonadPR m => MonadTcDeclM m where
+  liftTcDeclM :: TcDeclM a -> m a
+  withCurrentTypeMap :: (TypeMap -> TypeMap) -> m a -> m a
 
-class MonadPR m => MonadTcBaseM m where
-  liftTcBaseM :: TcBaseM a -> m a
-  withTypeMap :: (TypeMap -> TypeMap) -> m a -> m a
+instance MonadTcDeclM TcDeclM where
+  liftTcDeclM = id
+  withCurrentTypeMap = withCurrentTypeMapTB
 
-instance MonadTcBaseM TcBaseM where
-  liftTcBaseM = id
-  withTypeMap = withTypeMapTB
+extendGlobalTypeMap :: MonadTcDeclM m => (TypeMap -> TypeMap) -> m ()
+extendGlobalTypeMap = liftTcDeclM . extendGlobalTypeMapTB
+  
 
-getTypeMap :: MonadTcBaseM m => m TypeMap
-getTypeMap = liftTcBaseM getTypeMapTB
+getTypeMap :: MonadTcDeclM m => m TypeMap
+getTypeMap = liftTcDeclM getTypeMapTB
 
-getThisType :: MonadTcBaseM m => m TcClassType
-getThisType = liftTcBaseM getThisTypeTB
+getThisType :: MonadTcDeclM m => m TcClassType
+getThisType = liftTcDeclM getThisTypeTB
 
-getSuperType :: MonadTcBaseM m => m TcClassType
+getSuperType :: MonadTcDeclM m => m TcClassType
 getSuperType = do
   thisTy <- getThisType
   thisSig <- lookupTypeOfType (clsTypeToType thisTy)
@@ -927,11 +968,18 @@
           $ "Called on non-class with multiple super types"
 
 
-getTypeMapTB :: TcBaseM TypeMap
-getTypeMapTB = TcBaseM $ \tm _ -> return tm
+withFreshCurrentTypeMap :: TcDeclM a -> TcDeclM a
+withFreshCurrentTypeMap = withCurrentTypeMap (const emptyTM)
 
-getThisTypeTB :: TcBaseM TcClassType
-getThisTypeTB = TcBaseM $ \_ ty -> return ty
 
-withTypeMapTB :: (TypeMap -> TypeMap) -> TcBaseM a -> TcBaseM a
-withTypeMapTB tmf (TcBaseM f) = TcBaseM $ \tm ty -> f (tmf tm) ty
+getTypeMapTB :: TcDeclM TypeMap
+getTypeMapTB = TcDeclM $ \ctm gtm _ -> return $ (ctm `merge` gtm, gtm)
+
+getThisTypeTB :: TcDeclM TcClassType
+getThisTypeTB = TcDeclM $ \_ gtm ty -> return (ty, gtm)
+
+withCurrentTypeMapTB :: (TypeMap -> TypeMap) -> TcDeclM a -> TcDeclM a
+withCurrentTypeMapTB tmf (TcDeclM f) = TcDeclM $ \ctm gtm ty -> f (tmf ctm) gtm ty
+
+extendGlobalTypeMapTB :: (TypeMap -> TypeMap) -> TcDeclM ()
+extendGlobalTypeMapTB tmf = TcDeclM $ \_ gtm _ -> return ((), tmf gtm)
diff --git a/src/Language/Java/Paragon/TypeCheck/Policy.hs b/src/Language/Java/Paragon/TypeCheck/Policy.hs
--- a/src/Language/Java/Paragon/TypeCheck/Policy.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Policy.hs
@@ -1,11 +1,11 @@
-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP, DeriveDataTypeable, PatternGuards #-}
 module Language.Java.Paragon.TypeCheck.Policy 
     (
      bottom, top, thisP, join, joinWThis, meet, {-recmeet,-} isTop, isBottom, includesThis,
      TcPolicy(..), PrgPolicy(..),{-TcPolicyRec(..),-} TcClause(..), TcAtom(..), TcActor(..), TcMetaVar(..),
      {- toPolicyLit, -} {-toRecPolicy,-}
      lockToAtom, 
-     {-zonkPolicy,-} substPolicy,
+     {-zonkPolicy,-} substPolicy, firstRigid, substThis,
      flowAtomString,
 
      ActorPolicy, AtomPolicy
@@ -19,8 +19,8 @@
 import Language.Java.Paragon.TypeCheck.Locks
 
 import Data.IORef
-import Data.List ( (\\) {-, groupBy, nub-} )
-import Data.Maybe (fromJust)
+import Data.List ( (\\) {-, groupBy, nub-}  )
+import Data.Maybe 
 
 #ifdef BASE4
 import Data.Data
@@ -31,8 +31,8 @@
 flowAtomString :: String
 flowAtomString = "$FLOW$"
 
-moduleString :: String
-moduleString = typeCheckerBase ++ ".Locks"
+policyModule :: String
+policyModule = typeCheckerBase ++ ".Policy"
 
 ---------------------------------------------------------------
 -- Basic policies
@@ -68,15 +68,15 @@
 --  deriving (Data, Typeable)
 
 instance Data (TcMetaVar a) where
-    gunfold    = panic (moduleString ++ ": instance Data TcMetaVar (gunfold)")
+    gunfold    = panic (policyModule ++ ": instance Data TcMetaVar (gunfold)")
                  "Meta variables should never be reified"
-    toConstr   = panic (moduleString ++ ": instance Data TcMetaVar (toConstr)")
+    toConstr   = panic (policyModule ++ ": instance Data TcMetaVar (toConstr)")
                  "Meta variables should never be reified"
-    dataTypeOf = panic (moduleString ++ ": instance Data TcMetaVar (dataTypeOf)")
+    dataTypeOf = panic (policyModule ++ ": instance Data TcMetaVar (dataTypeOf)")
                  "Meta variables should never be reified"
 
 instance Typeable (TcMetaVar a) where
-    typeOf = panic (moduleString ++ ": instance Typeable TcMetaVar (typeOf)")
+    typeOf = panic (policyModule ++ ": instance Typeable TcMetaVar (typeOf)")
              "Meta variables should never be reified"
 
 instance Eq (TcMetaVar a) where
@@ -143,7 +143,7 @@
   where toRecClause (TcClause act ats) = TcClause (TcAtom (mkSimpleLName (Ident () flowAtomString)) [act]) ats
 toRecPolicy (TcJoin p1 p2) = TcJoinRec (toRecPolicy p1) (toRecPolicy p2)
 toRecPolicy (TcMeet p1 p2) = TcMeetRec (toRecPolicy p1) (toRecPolicy p2)
-toRecPolicy _ = panic (moduleString ++ "toRecPolicy")
+toRecPolicy _ = panic (policyModule ++ "toRecPolicy")
                 "Cannot convert non-literal policy to a recursive one"
 -}
 
@@ -174,24 +174,43 @@
 ----------------------------------}
 -- Basic policies
 
-bottom, top, thisP :: (TcPolicy TcActor)
-bottom = RealPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []]
-top = RealPolicy $ TcPolicy []
-thisP = RealPolicy TcThis
+class IsPolicy p where
+  toPolicy :: PrgPolicy a -> p a
+  fromPolicy :: p a -> Maybe (PrgPolicy a)
+  includesThis :: p a -> Bool
 
-isTop, isBottom, includesThis :: (TcPolicy TcActor) -> Bool
-isTop = (== top)
-isBottom (RealPolicy (TcPolicy cs)) = any isBottomC cs
+instance IsPolicy PrgPolicy where
+  toPolicy = id
+  fromPolicy = Just
+  
+  includesThis TcThis = True
+  includesThis (TcJoin p q) = any includesThis [p,q]
+  includesThis (TcMeet p q) = any includesThis [p,q]
+  includesThis _ = False
+
+instance IsPolicy TcPolicy where
+  toPolicy = RealPolicy
+  fromPolicy (RealPolicy p) = Just p
+  fromPolicy _ = Nothing
+
+  includesThis (Join p q) = any includesThis [p,q]
+  includesThis (RealPolicy p) = includesThis p
+  includesThis _ = False
+
+bottom, top, thisP :: IsPolicy pol => pol TcActor
+bottom = toPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []]
+top = toPolicy $ TcPolicy []
+thisP = toPolicy TcThis
+
+isTop, isBottom :: IsPolicy pol => pol TcActor -> Bool
+isTop pol | Just (TcPolicy []) <- fromPolicy pol = True
+isTop _ = False
+
+isBottom pol | Just (TcPolicy cs) <- fromPolicy pol = any isBottomC cs
   where isBottomC (TcClause (TcVar _) []) = True
         isBottomC _ = False
 isBottom _ = False
 
-includesThis (RealPolicy TcThis) = True
-includesThis (RealPolicy (TcJoin p q)) = any includesThis [RealPolicy p, RealPolicy q]
-includesThis (RealPolicy (TcMeet p q)) = any includesThis [RealPolicy p, RealPolicy q]
-includesThis (Join p q) = any includesThis [p, q]
-includesThis _ = False
-
 ----------------------------------
 -- meet and join
 
@@ -200,7 +219,7 @@
 joinWThis p q = Join p q
 
 lubWThis :: (PrgPolicy TcActor) -> (PrgPolicy TcActor) -> (PrgPolicy TcActor)
-lubWThis TcThis p = p
+lubWThis TcThis q = q
 lubWThis p TcThis = p
 lubWThis p q = lub p q
 
@@ -268,7 +287,8 @@
 
 meet :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor)
 meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q
-meet _ _ = error "meet used on non-programmable policies"
+meet _ _ = panic (policyModule ++ ".meet") 
+           "meet used on non-programmable policies"
 
 {-TO FIX
 recmeet :: TcPolicyRec -> TcPolicyRec -> TcPolicyRec
@@ -279,8 +299,9 @@
 ----------------------------------------------
 {-- Specialisation
 
-specialise :: [TcLock] -> TcPolicy -> TcPolicy
+specialise :: [TcLock] -> PrgPolicy TcActor -> PrgPolicy TcActor
 specialise ls (TcPolicy cs) = TcPolicy $ concatMap (specClause ls) cs
+specialise _ p = p
 
 specClause :: [TcLock] -> TcClause TcActor -> [TcClause TcActor]
 specClause ls (TcClause h atoms) = 
@@ -335,8 +356,8 @@
               checkConsistent s = case nub s of
                                     [x] -> Just x
                                     _   -> Nothing
--}
 
+-}
 lockToAtom :: TcLock -> TcAtom
 lockToAtom (TcLock n aids) = TcAtom n $ map TcActor aids
 lockToAtom (TcLockVar i) = TcAtom (mkSimpleLName i) []
@@ -370,8 +391,9 @@
 -- Policy substitution
 
 -- Invariant: policies are always closed by the env
-substPolicy :: [(Ident (), (PrgPolicy TcActor))] -> (PrgPolicy TcActor) -> (PrgPolicy TcActor)
-substPolicy env (TcRigidVar i) = fromJust $ lookup i env
+substPolicy :: [(Ident (), PrgPolicy TcActor)] -> PrgPolicy TcActor -> PrgPolicy TcActor
+substPolicy env (TcRigidVar i) 
+    | Just q <- lookup i env = q
 substPolicy env (TcJoin p1 p2) =
     let pol1 = substPolicy env p1
         pol2 = substPolicy env p2
@@ -381,6 +403,24 @@
         pol2 = substPolicy env p2
     in pol1 `glb` pol2
 substPolicy _ p = p
+
+firstRigid :: PrgPolicy a -> Maybe (Ident ())
+firstRigid (TcRigidVar i) = Just i
+firstRigid (TcJoin p q) = listToMaybe $ catMaybes $ map firstRigid [p,q]
+firstRigid (TcMeet p q) = listToMaybe $ catMaybes $ map firstRigid [p,q]
+firstRigid _ = Nothing
+
+substThis :: PrgPolicy TcActor -> PrgPolicy TcActor -> PrgPolicy TcActor
+substThis p TcThis = p
+substThis p (TcJoin p1 p2) =
+    let pol1 = substThis p p1
+        pol2 = substThis p p2
+    in pol1 `lub` pol2
+substThis p (TcMeet p1 p2) =
+    let pol1 = substThis p p1
+        pol2 = substThis p p2
+    in pol1 `glb` pol2
+substThis _ p = p
 
 {-
 mkPolicySubst :: [TcPolicy] -> [TcPolicy] -> [(Ident (), TcPolicy)]
diff --git a/src/Language/Java/Paragon/TypeCheck/TcExp.hs b/src/Language/Java/Paragon/TypeCheck/TcExp.hs
--- a/src/Language/Java/Paragon/TypeCheck/TcExp.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TcExp.hs
@@ -45,7 +45,7 @@
 --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str
 --debugTc _ = return ()
 
-tcExp :: Exp () -> TcCodeM r (TcType, ActorPolicy, Exp T)
+tcExp :: Exp () -> TcCodeM (TcType, ActorPolicy, Exp T)
 
 -- Rule PAREN
 tcExp (Paren _ e) = do (ty, p, e') <- tcExp e
@@ -337,7 +337,7 @@
                           -> [Exp T]                          -- Accumulated annotated expressions
                           -> [(Exp (), Maybe (Policy ()))]    -- Remaining dimexprs/pols
                           -> ActorPolicy                      -- Policy of previous dimension
-                          -> TcCodeM r ([ActorPolicy], [Exp T])
+                          -> TcCodeM ([ActorPolicy], [Exp T])
             checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE)
             checkDimExprs accP accE ((e,mp):emps) pPrev = do
               (tyE,pE,e') <- tcExp e
@@ -392,7 +392,7 @@
 --------------------------
 -- Array initializers
 
-tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck (TcCodeM r) ArrayInit
+tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck TcCodeM ArrayInit
 tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do
   (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits
   mapM_ (\(p,e) -> constraintLS p pol1 $
@@ -404,7 +404,7 @@
   return $ ArrayInit Nothing inits'
 tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions"
 
-tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM r (ActorPolicy, VarInit T)
+tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T)
 tcVarInit baseType pols (InitExp _ e) = do
 --  debugPrint $ "Pols: " ++ show pols
 --  debugPrint $ "Exp:  " ++ show e
@@ -419,13 +419,13 @@
   arr' <- tcArrayInit baseType pols arr
   return (bottom, InitArray Nothing arr')
 
-evalMaybePol :: Maybe (Policy ()) -> TcCodeM r ActorPolicy
+evalMaybePol :: Maybe (Policy ()) -> TcCodeM ActorPolicy
 evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy)
 
 --------------------------
 -- Field Access
 
-tcFieldAccess :: FieldAccess () -> TcCodeM r (TcType, ActorPolicy, FieldAccess T)
+tcFieldAccess :: FieldAccess () -> TcCodeM (TcType, ActorPolicy, FieldAccess T)
 tcFieldAccess (PrimaryFieldAccess _ e fi) = do
   (tyE,pE,e') <- tcExp e
   case tyE of
@@ -445,7 +445,7 @@
 -- Instance creation
 
 tcCreate :: TcClassType -> [TypeArgument ()] -> [Argument ()] 
-         -> TcCodeM r (TcType, ActorPolicy, [Argument T])
+         -> TcCodeM (TcType, ActorPolicy, [Argument T])
 tcCreate ctyT tas args = do
   (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
   (tps,genCti) <- lookupConstr ctyT tas tysArgs
@@ -507,7 +507,7 @@
 
 -- | Check a method invocation, which could possibly represent
 --   a lock query expression.
-tcMethodOrLockInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T)
+tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)
 tcMethodOrLockInv (MethodCallOrLockQuery _ (Name _ MOrLName mPre i) args) = do
   -- We couldn't resolve without type information whether
   -- this truly is a method or a lock.
@@ -530,18 +530,20 @@
             ++ " arguments but has been given " ++ show (length args)
 
   (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
+  debugPrint $ "args': " ++ show args'
   mapM_ (\ty -> check (isActorType ty) $
                 "Trying to query lock with argument of type " 
                 ++ prettyPrint ty ++ "\n" ++
                        "All arguments to lock query must be of type actor") tysArgs
   let tyR = lockT [TcLock nam $ map (fromJust . mActorId) tysArgs]
+  debugPrint $ "tyR: " ++ show tyR
   return (tyR, foldl1 join (pL:psArgs),
              MethodCallOrLockQuery (Just tyR) (notAppl nam) args')
       
 tcMethodOrLockInv mi = tcMethodInv mi
 
 -- | Check a true method invocation
-tcMethodInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T)
+tcMethodInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)
 tcMethodInv mi = do
   debugPrint $ "tcMethodInv: " ++ prettyPrint mi
   (n, msig, args, psArgs, pE, ef) <-
@@ -582,8 +584,8 @@
                   constraintLS argP parP $
                       "Method applied to argument with too restrictive policy:\n" ++ 
                       "Method invocation: " ++ prettyPrint mi ++ "\n" ++
-                      "Argument: " ++ prettyPrint arg ++
-                      "  with policy: " ++ prettyPrint argP ++
+                      "Argument: " ++ prettyPrint arg ++ "\n" ++
+                      "  with policy: " ++ prettyPrint argP ++ "\n" ++
                       "Declared policy bound: " ++ prettyPrint parP
              ) (zip3 args psArgs psPars)
   -- Check E[branchPC](*) <= pW
@@ -614,12 +616,17 @@
 -- Policy expressions
 -- Treat them as pure compile-time for now
 
-tcPolicyExp :: PolicyExp () -> TcCodeM r (PrgPolicy TcActor)
+tcPolicyExp :: PolicyExp () -> TcCodeM (PrgPolicy TcActor)
 tcPolicyExp (PolicyLit _ cs) = do
   tcCs <- mapM tcClause cs
   return (TcPolicy tcCs)
 tcPolicyExp pe@(PolicyOf _ i) = do
-  (_, _, param) <- lookupVar Nothing i
+  vi@(_, _, param) <- lookupVar Nothing i
+  debugPrint $ "tcPolicyExp: vi: " ++ show vi
+  tm <- getTypeMap
+  debugPrint $ "tcPolicyExp: TypeMap: " ++ show tm
+  vm <- vars <$> getEnv
+  debugPrint $ "tcPolicyExp: VarMap: " ++ show vm
   check param $
             "policyof may only be used on parameters: " ++ prettyPrint pe
   return $ TcRigidVar i
@@ -628,13 +635,13 @@
   return $ TcRigidVar i
 tcPolicyExp (PolicyThis _) = return TcThis
  
-tcClause :: Clause () -> TcCodeM r (TcClause TcActor)
+tcClause :: Clause () -> TcCodeM (TcClause TcActor)
 tcClause (Clause _ h ats) = do
   tcH <- tcActor h
   tcAs <- mapM tcAtom ats
   return (TcClause tcH tcAs)
 
-tcAtom :: Atom () -> TcCodeM r TcAtom
+tcAtom :: Atom () -> TcCodeM TcAtom
 tcAtom (Atom _ n@(Name _ LName mPre i) as) = do
   LSig _ ar _ <- lookupLock mPre i
   check (length as == ar) $ "Arity mismatch in policy"
@@ -643,11 +650,11 @@
 tcAtom (Atom _ n _) = panic (tcExpModule ++ ".tcAtom") $
                       "None-lock name: " ++ show n
 
-tcActor :: Actor () -> TcCodeM r TcActor
+tcActor :: Actor () -> TcCodeM TcActor
 tcActor (Var   _ i) = return $ TcVar i
 tcActor (Actor _ n) = TcActor <$> tcActorName n
 
-tcActorName :: ActorName () -> TcCodeM r ActorId
+tcActorName :: ActorName () -> TcCodeM ActorId
 tcActorName (ActorName    _ n) = getActorId n
 tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i
 
@@ -655,7 +662,7 @@
 --    Types of operators         --
 -----------------------------------
 
-opType :: Op () -> TcType -> TcType -> TcCodeM r TcType
+opType :: Op () -> TcType -> TcType -> TcCodeM TcType
 -- First the special cases: policy operators, and String conversion
 opType (Mult _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `join` p2))
 opType (Add  _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `meet` p2))
diff --git a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs
--- a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs
@@ -26,7 +26,7 @@
 --    Typechecking Statements    --
 -----------------------------------
 
-tcStmt :: TypeCheck (TcCodeM r) Stmt
+tcStmt :: TypeCheck TcCodeM Stmt
 
 -- Rule EMPTY
 tcStmt (Empty _) = return $ Empty Nothing
@@ -352,7 +352,7 @@
 tcStmt s = fail $ "Unsupported statement: " ++ prettyPrint s
 
 
-withInits :: Maybe (ForInit ()) -> TcCodeM r a -> TcCodeM r (Maybe (ForInit T), a)
+withInits :: Maybe (ForInit ()) -> TcCodeM a -> TcCodeM (Maybe (ForInit T), a)
 withInits Nothing tca = (Nothing,) <$> tca
 withInits (Just (ForInitExps _ es)) tca = do
     (_,_,es') <- unzip3 <$> mapM tcExp es
@@ -368,10 +368,10 @@
 -- Typechecking Blocks and BlockStmts --
 ----------------------------------------
 
-tcBlock :: TypeCheck (TcCodeM r) Block
+tcBlock :: TypeCheck TcCodeM Block
 tcBlock (Block _ bss) = Block Nothing <$> tcBlockStmts bss
 
-tcBlockStmts :: [BlockStmt ()] -> TcCodeM r [BlockStmt T]
+tcBlockStmts :: [BlockStmt ()] -> TcCodeM [BlockStmt T]
 -- Rule EMPTYBLOCK
 tcBlockStmts [] = return []
 
@@ -395,7 +395,7 @@
 
 
 tcLocalVars :: ActorPolicy -> TcType -> Bool -> [VarDecl ()] 
-            -> [VarDecl T] -> TcCodeM r a -> TcCodeM r ([VarDecl T], a)
+            -> [VarDecl T] -> TcCodeM a -> TcCodeM ([VarDecl T], a)
 tcLocalVars _ _ _ [] acc cont = cont >>= \a -> return (reverse acc, a)
 
 
@@ -445,7 +445,7 @@
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd
 
 
-localVarPol :: [Modifier ()] -> TcCodeM r ActorPolicy
+localVarPol :: [Modifier ()] -> TcCodeM ActorPolicy
 localVarPol ms = 
     case [ p | Reads _ p <- ms ] of
       [] -> newMetaPolVar --return bottom
@@ -456,7 +456,7 @@
 -- Typechecking Explicit Constructor Invocations --
 ---------------------------------------------------
 
-tcEci :: TypeCheck (TcCodeM r) ExplConstrInv
+tcEci :: TypeCheck TcCodeM ExplConstrInv
 tcEci eci = do
   (tyT, nwtas, as, con) <- 
       case eci of