diff --git a/paragon.cabal b/paragon.cabal
--- a/paragon.cabal
+++ b/paragon.cabal
@@ -1,5 +1,5 @@
 Name:                   paragon
-Version:                0.1.22
+Version:                0.1.23
 License:                BSD3
 License-File:           LICENSE
 Author:                 Niklas Broberg
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.22"
+versionString = "0.1.23"
 
 libraryBase, typeCheckerBase :: String
 libraryBase = "Language.Java.Paragon"
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
@@ -36,7 +36,7 @@
   (tnExpnMap,supExpnMap) <- buildMapFromTd td jipExpnMap
   -- We need to take the current name take precedence
   let expnMap = Map.union tnExpnMap (unionExpnMaps [jipExpnMap,supExpnMap])
-  debugPrint $ "Expansions: " ++ show expnMap
+--  debugPrint $ "Expansions: " ++ show expnMap
   td' <- runNameRes (rnTypeDecl td) expnMap
   return $ CompilationUnit () _pkg imps' [td']
 
@@ -139,13 +139,13 @@
 
 rnMemberDecl :: Resolve MemberDecl
 rnMemberDecl md = do
-    debugPrint $ "Resolving member decl: " ++ prettyPrint md
-    debugPrint $ show md ++ "\n"
+--    debugPrint $ "Resolving member decl: " ++ prettyPrint md
+--    debugPrint $ show md ++ "\n"
     case md of
       FieldDecl _ ms t vds -> 
           FieldDecl () <$> mapM rnModifier ms <*> rnType t <*> mapM rnVarDecl vds
 
-      MethodDecl _ ms tps mRet mI fps exns mbody -> do
+      MethodDecl _ ms tps ret mI fps exns mbody -> do
           let ps = [ pI | FormalParam _ _ _ _ (VarId _ pI) <- fps ]
               paramsE = Map.fromList $ 
                               concatMap mkEExpansion ps
@@ -153,7 +153,7 @@
             MethodDecl () 
               <$> mapM rnModifier ms
               <*> mapM rnTypeParam tps
-              <*> mapM rnType mRet
+              <*> rnReturnType ret
               <*> pure mI
               <*> mapM rnFormalParam fps
               <*> mapM rnExceptionSpec exns
@@ -179,7 +179,7 @@
             <*> pure arity
             <*> mapM rnLockProperties mProps
       _ -> do
-        debugPrint $ show md
+--        debugPrint $ show md
         fail $ "Inner types not supported"
               
 rnConstructorBody :: Resolve ConstructorBody
@@ -475,6 +475,10 @@
 
 -- Types
 
+rnReturnType :: Resolve ReturnType
+rnReturnType (Type _ t) = Type () <$> rnType t
+rnReturnType rt = return rt
+
 rnType :: Resolve Type
 rnType (RefType _ rt) = RefType () <$> rnRefType rt
 rnType t = return t
@@ -741,7 +745,7 @@
                        -> PiReader (ImportDecl (), Expansion)
 buildMapFromImportName imp = do
     finePrint $ "Resolving import: " ++ prettyPrint imp
-    debugPrint $ show imp
+--    debugPrint $ show imp
     case imp of
       SingleTypeImport _ tn@(Name _ TName mPre i) -> do
               mPre' <- resolvePre mPre
@@ -771,7 +775,7 @@
               isP  <- doesPkgExist resName
               if isP
                then do -- resolve as package
-                 debugPrint $ "Package exists: " ++ show resName
+                 --debugPrint $ "Package exists: " ++ show resName
                  piTypeIdents <- getPkgContents resName
                  let resExpn = Map.fromList $ 
                                  concatMap (\x -> [((x, TName   ), return (Just resName, TName)),
diff --git a/src/Language/Java/Paragon/Parser.hs b/src/Language/Java/Paragon/Parser.hs
--- a/src/Language/Java/Paragon/Parser.hs
+++ b/src/Language/Java/Paragon/Parser.hs
@@ -20,7 +20,7 @@
     
     stmtExp, exp, primary, literal, lhs,
     
-    ttype, primType, refType, classType, resultType,
+    ttype, primType, refType, classType, returnType,
 
     typeParams, typeParam,
     
@@ -280,7 +280,7 @@
 methodDeclM :: P (Mod (MemberDecl ()))
 methodDeclM = do
     tps <- lopt typeParams
-    rt  <- resultType
+    rt  <- returnType
     i   <- ident
     fps <- formalParams
     thr <- lopt throws
@@ -389,7 +389,7 @@
 absMethodDeclM :: P (Mod (MemberDecl ()))
 absMethodDeclM = do
     tps <- lopt typeParams
-    rt  <- resultType
+    rt  <- returnType
     i   <- ident
     fps <- formalParams
     thr <- lopt throws
@@ -837,9 +837,10 @@
     LockExp () <$> (tok Op_Query >> lock) <|>
     -- TODO: These two following should probably be merged more
     (try $ do 
-        rt <- resultType 
+        rt <- returnType 
+        mt <- checkClassLit rt
         period >> tok KW_Class
-        return $ ClassLit () rt) <|>
+        return $ ClassLit () mt) <|>
     (try $ do 
         n <- nameRaw tName
         period >> tok KW_This
@@ -854,6 +855,12 @@
             AntiQExpTok s -> Just s
             _ -> Nothing)
 
+checkClassLit :: ReturnType () -> P (Maybe (Type ()))
+checkClassLit (LockType ()) = fail "Lock is not a class type!"
+checkClassLit (VoidType ()) = return Nothing
+checkClassLit (Type _ t)    = return $ Just t
+                                           
+
 primarySuffix :: P (Exp () -> Exp ())
 primarySuffix = try instanceCreationSuffix <|>
     try ((ArrayAccess () .) <$> arrayAccessSuffix) <|>
@@ -1207,8 +1214,10 @@
     return (i, tas)
 -}
 
-resultType :: P (Maybe (Type ()))
-resultType = tok KW_Void >> return Nothing <|> Just <$> ttype <?> "resultType"
+returnType :: P (ReturnType ())
+returnType = tok KW_Void   >> return (VoidType ()) <|> 
+             tok KW_P_Lock >> return (LockType ()) <|>
+             Type () <$> ttype <?> "returnType"
 
 classTypeList :: P [ClassType ()]
 classTypeList = seplist1 classType comma
diff --git a/src/Language/Java/Paragon/Pretty.hs b/src/Language/Java/Paragon/Pretty.hs
--- a/src/Language/Java/Paragon/Pretty.hs
+++ b/src/Language/Java/Paragon/Pretty.hs
@@ -116,10 +116,10 @@
   pretty (FieldDecl _ mods t vds) =
     hsep (map pretty mods ++ pretty t:map pretty vds) <> semi
 
-  pretty (MethodDecl _ mods tParams mt ident fParams throws body) =
+  pretty (MethodDecl _ mods tParams ret ident fParams throws body) =
     hsep [hsep (map pretty mods)
           , ppTypeParams tParams
-          , ppResultType mt
+          , pretty ret
           , pretty ident <> ppArgs fParams
           , ppThrows throws
          ] $$ pretty body
@@ -364,7 +364,7 @@
   pretty (Lit _ l) = pretty l
   
   pretty (ClassLit _ mT) = 
-    ppResultType mT <> text ".class"
+    maybe (text "void") pretty mT <> text ".class"
 
   pretty (This _) = text "this"
   
@@ -624,9 +624,14 @@
   pretty (ExceptionSpec _ mods t) =
       hsep (map pretty mods) <+> pretty t
 
-ppResultType :: Maybe (Type x) -> Doc
-ppResultType Nothing = text "void"
-ppResultType (Just a) = pretty a
+instance Pretty (ReturnType a) where
+  pretty (VoidType _) = text "void"
+  pretty (LockType _) = text "lock"
+  pretty (Type _ ty ) = pretty ty
+
+--ppResultType :: Maybe (Type x) -> Doc
+--ppResultType Nothing = text "void"
+--ppResultType (Just a) = pretty a
 
 -----------------------------------------------------------------------
 -- Paragon Policies
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
@@ -89,6 +89,7 @@
        ''WildcardBound,''Decl,''VarInit,
        ''Clause, ''LClause,
        ''PrimType,
+       ''ReturnType,
        ''Atom,
        ''Actor,
        ''ActorName,
diff --git a/src/Language/Java/Paragon/Syntax.hs b/src/Language/Java/Paragon/Syntax.hs
--- a/src/Language/Java/Paragon/Syntax.hs
+++ b/src/Language/Java/Paragon/Syntax.hs
@@ -104,7 +104,7 @@
     -- | The variables of a class type are introduced by field declarations.
     = FieldDecl a [Modifier a] (Type a) [VarDecl a]
     -- | A method declares executable code that can be invoked, passing a fixed number of values as arguments.
-    | MethodDecl a      [Modifier a] [TypeParam a] (Maybe (Type a)) (Ident a) [FormalParam a] [ExceptionSpec a] (MethodBody a)
+    | MethodDecl a      [Modifier a] [TypeParam a] (ReturnType a) (Ident a) [FormalParam a] [ExceptionSpec a] (MethodBody a)
     -- | A constructor is used in the creation of an object that is an instance of a class.
     | ConstructorDecl a [Modifier a] [TypeParam a]                  (Ident a) [FormalParam a] [ExceptionSpec a] (ConstructorBody a)
     -- | A member class is a class whose declaration is directly enclosed in another class or interface declaration.
@@ -467,6 +467,11 @@
 -----------------------------------------------------------------------
 -- Types
 
+data ReturnType a
+    = VoidType a
+    | LockType a
+    | Type a (Type a)
+  deriving (Eq,Ord,Show,Typeable,Data,Functor)
 
 -- | There are two kinds of types in the Java programming language: primitive types and reference types.
 data Type a
@@ -696,7 +701,7 @@
    ''Catch, ''SwitchBlock, ''SwitchLabel, ''ForInit, ''ExceptionSpec,
    ''Exp, ''Literal, ''Op, ''AssignOp, ''Lhs, 
    ''ArrayIndex, ''FieldAccess, ''MethodInvocation,
-   ''Type, ''PrimType, ''RefType, ''ClassType, 
+   ''Type, ''PrimType, ''RefType, ''ClassType, ''ReturnType,
    ''TypeArgument, ''NonWildTypeArgument, ''WildcardBound, ''TypeParam,
    ''PolicyExp, ''LockProperties, ''Clause, ''LClause,
    ''Actor, ''ActorName, ''Atom, ''Lock, ''Ident, ''Name])
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
@@ -116,14 +116,14 @@
                        Left mErr
                            -> panic (typeCheckerBase ++ ".withSuperType")
                               $ "Super type evaluated but now doesn't exist: " ++ show mErr
-                       Right superSig -> (tMembers superSig) { constrs = Map.empty }
+                       Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty }
 
     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) } 
+            newTm = tm { types = Map.insert i (tps,[],thisSig) (types tm) } 
         in foldl merge newTm superTMs)
           
 
@@ -136,13 +136,13 @@
                        Left mErr
                            -> panic (typeCheckerBase ++ ".withSuperType")
                               $ "Super type evaluated but now doesn't exist: " ++ show mErr
-                       Right superSig -> (tMembers superSig) { constrs = Map.empty }
+                       Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty }
 
   let thisTm = baseTm { types = Map.empty, packages = Map.empty }
       resTm  = foldl merge thisTm superTMs
       thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) 
                   True False cTys [] resTm -- TODO: Include proper values
-  extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig)
+  extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps [] thisSig)
 
 
 ---------------------------------------------------------------
@@ -164,12 +164,12 @@
         (spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs
                                
     withFoldMap spawnActorVd spawns $
---      withFoldMap aliasActorVd unstables $
+--      withFoldMap unknownActorVd unstables $
       withFoldMap evalActorVd stables $ do
         --debug "fetchActors complete"
         tcba
         
-            where spawnActorVd, evalActorVd -- , aliasActorVd 
+            where spawnActorVd, evalActorVd -- , unknownActorVd 
                       :: ([Modifier ()],VarDecl ()) -> TcDeclM a -> TcDeclM a
                   -- Only Nothing for initializer
                   spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
@@ -183,15 +183,15 @@
                       fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
 {-                  -- All non-final OR non-static
-                  aliasActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
+                  unknownActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
                     p <- getReadPolicy ms
                     let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
-                    a <- aliasActorId
+                    a <- unknownActorId
                     withTypeMap (\tm -> 
                                      tm { actors = Map.insert i a (actors tm),
                                           fields = Map.insert i vti (fields tm) }) $
                       tcra
-                  aliasActorVd (_, VarDecl _ arvid _) _ =
+                  unknownActorVd (_, VarDecl _ arvid _) _ =
                       fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 -} 
                   -- Final, with explicit initializer
@@ -203,8 +203,8 @@
                              tm <- getTypeMap
                              case lookupNamed actors n tm of
                                Just a -> return a
-                               Nothing -> aliasActorId --fail "Internal error: no such actor"
-                           _ -> aliasActorId
+                               Nothing -> unknownActorId --fail "Internal error: no such actor"
+                           _ -> unknownActorId
                     withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
                                                     fields = Map.insert i vti (fields tm) }) $
                       tcra
@@ -259,8 +259,8 @@
     check (all (\m -> not (isPolicyMod m || isLockStateMod m)) ms) $
           "Methods annotated with typemethod cannot have policy or lock state modifiers"
     -- 3. Same check for parameters
-    let plms = [ m | FormalParam _ pms _ _ _ <- ps, m <- pms, 
-                     isPolicyMod m, isLockStateMod m ]
+    let (pis, pmss) = unzip [ (pI, pms) | FormalParam _ pms _ _ (VarId _ pI) <- ps ]
+        plms = [ m | m <- concat pmss, isPolicyMod m, isLockStateMod m ]
     check (null plms) $ "Parameters to typemethods must not have policy modifiers"
     -- 4. No exceptions may be thrown
     check (null exns) $ "Methods annotated with typemethod may not throw exceptions"
@@ -270,7 +270,8 @@
               mRetType = rTy,
               mRetPol  = bottom,
               mWrites  = top,
-              mPars    = [ bottom | _ <- ps ],
+              mPars    = pis,
+              mParPols = [ bottom | _ <- ps ],
               mExpects = [],
               mLMods   = noMods,
               mExns    = []
@@ -422,7 +423,7 @@
     -- 1. Check return type
     ty <- evalReturnType retT
     -- 2. Check parameter types and policy modifiers
-    (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps
+    (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps
     let pInfos = zip3 ps pTs pPols
     -- 3. Typecheck and evaluate policy modifiers
     withFoldMap withParam pInfos $ checkPolicyMods st ms 
@@ -439,7 +440,8 @@
                 mRetType = ty,
                 mRetPol  = rPol,
                 mWrites  = wPol,
-                mPars    = pPols,
+                mPars    = pIs,
+                mParPols = pPols,
                 mExpects = es,
                 mLMods   = lms,
                 mExns    = xSigs
@@ -459,7 +461,7 @@
     -- 0. Setup type parameters
     withFoldMap withTypeParam tps $ do
     -- 1. Check parameter types and policy modifiers
-    (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps
+    (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps
     let pInfos = zip3 ps pTs pPols
     -- 2. Typecheck and evaluate policy modifiers
     withFoldMap withParam pInfos $ checkPolicyMods st ms 
@@ -473,7 +475,8 @@
     wPol <- getWritePolicy ms
     let cti = CSig {
               cWrites  = wPol,
-              cPars    = pPols,
+              cPars    = pIs,
+              cParPols = pPols,
               cExpects = es,
               cLMods   = lms,
               cExns    = xSigs
@@ -552,7 +555,7 @@
   let es = concat [ l | Expects _ l <- ms ]
   mapM evalLock es
 
-typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, ActorPolicy)
+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)
 typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do
   withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do
     -- 1. Check parameter type
@@ -561,7 +564,7 @@
     checkPolicyMods st ms 
        "typeCheckSignature: At most one read modifier allowed per parameter"
     rPol <- getParamPolicy i ms
-    return (if ell then arrayType ty bottom else ty, rPol)
+    return (if ell then arrayType ty bottom else ty, i, rPol)
 typeCheckParam _ (FormalParam _ _ _ _ arvid) =
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
@@ -680,7 +683,7 @@
   let isVarArity = case reverse ps of
                      [] -> False
                      (FormalParam _ _ _ b _ : _) -> b
-  Just (MSig tyRet pRet pPars pWri expLs lMods xSigs) <- do
+  Just (MSig tyRet pRet _pIs pPars pWri expLs lMods xSigs) <- do
       mMap <- fromJust . Map.lookup i . methods <$> getTypeMap
       return $ Map.lookup (tps, tysPs, isVarArity) mMap
 
@@ -704,7 +707,7 @@
 
   -- debug $ "Using env: " ++ show env
   -- Setup the state in which to check the body
-  parAids <- concat <$> mapM aliasIfActor (zip pars tysPs)
+  parAids <- concat <$> mapM unknownIfActor (zip pars tysPs)
   let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids
       parSt = st { actorSt = parAMap `Map.union` actorSt st }
 
@@ -719,7 +722,7 @@
               "Declared lock modifiers not general enough: " ++ show lMods
   mapM_ (checkExnMods endSt) exnLMods
   return $ MethodDecl Nothing (map notAppl _ms) (map notAppl tps) 
-             (fmap notAppl _rt) (notAppl i) (map notAppl ps) (map notAppl _exs) mb'
+             (notAppl _rt) (notAppl i) (map notAppl ps) (map notAppl _exs) mb'
 
 typeCheckMethodDecl _ md = panic (typeCheckerBase ++ ".typeCheckMethodDecl") $
                             "Applied to non-method decl " ++ show md
@@ -735,7 +738,7 @@
   let isVarArity = case reverse ps of
                      [] -> False
                      (FormalParam _ _ _ b _ : _) -> b
-  Just (CSig pPars pWri expLs lMods xSigs) <- 
+  Just (CSig _pIs pPars pWri expLs lMods xSigs) <- 
       Map.lookup (tps, tysPs, isVarArity) . constrs <$> getTypeMap
 
   -- Setup the environment in which to check the body
@@ -763,7 +766,7 @@
 
   --debug $ "Using branch map: " ++ show (branchPCE env)
   -- Setup the state in which to check the body
-  parAids <- concat <$> mapM aliasIfActor (zip pars tysPs)
+  parAids <- concat <$> mapM unknownIfActor (zip pars tysPs)
   let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids
       parSt = st { actorSt = parAMap `Map.union` actorSt st }
 
@@ -784,9 +787,9 @@
 typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $
                             "Applied to non-constructor decl " ++ show md
 
-aliasIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)]
-aliasIfActor (i, ty)
-    | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]
+unknownIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)]
+unknownIfActor (i, ty)
+    | ty == actorT = unknownActorId >>= \aid -> return [(i, aid)]
     | otherwise = return []
                 
 
diff --git a/src/Language/Java/Paragon/TypeCheck/Actors.hs b/src/Language/Java/Paragon/TypeCheck/Actors.hs
--- a/src/Language/Java/Paragon/TypeCheck/Actors.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Actors.hs
@@ -21,12 +21,16 @@
 -- which actor(s) it can represent, we list that.
 -- Otherwise an empty list means it could be an alias
 -- of any other actor.
-data ActorId = Fresh Int String | Alias Int | ActorTPVar (Ident ())
+data ActorId = Fresh Int String 
+             | Instance (Name ()) Int 
+             | Unknown Int
+             | ActorTPVar (Ident ())
  deriving (Show, Eq, Ord, Data, Typeable)
 
 instance Pretty ActorId where
   pretty (Fresh k s) = text s <> text ('#':show k)
-  pretty (Alias k) = text ('@':show k)
+  pretty (Instance n k) = pretty n <> text ('#':'#':show k) 
+  pretty (Unknown k) = text ('@':show k)
   pretty (ActorTPVar i) = pretty i
 
 
@@ -36,12 +40,16 @@
 unifies :: ActorId -> ActorId -> Bool
 -- If we have the exact (fresh) ids, we can tell exactly
 unifies (Fresh x _) (Fresh y _) = x == y
-unifies _ _ =  True
+-- If we have two fresh instance ids, they could be aliases of the same instance
+unifies (Instance n1 _) (Instance n2 _) = n1 == n2
+unifies (Unknown _) _ =  True
+unifies _ (Unknown _) = True
+unifies _ _ = False
 -- If either side is an alias, check if it could represent the fresh side.
---unifies (Alias x xs) (Fresh y) = null xs || y `elem` xs
---unifies (Fresh x) (Alias y ys) = null ys || x `elem` ys
+--unifies (Unknown x xs) (Fresh y) = null xs || y `elem` xs
+--unifies (Fresh x) (Unknown y ys) = null ys || x `elem` ys
 -- If both are aliases, check if they could represent the same fresh actor.
---unifies (Alias x xs) (Alias y ys) = null xs || null ys || (not . null) (xs `intersect` ys)
+--unifies (Unknown x xs) (Unknown y ys) = null xs || null ys || (not . null) (xs `intersect` ys)
 
 unify :: [ActorId] -> [ActorId] -> Bool
 unify xs ys = all (uncurry unifies) $ zip xs ys 
@@ -49,30 +57,33 @@
 {-
 equals :: ActorId -> ActorId -> Bool
 equals (Fresh x)   (Fresh y)   = x == y
-equals (Alias x _) (Alias y _) = x == y
+equals (Unknown x _) (Unknown y _) = x == y
 equals _ _ = False
 
 reprs :: ActorId -> [Int]
 reprs (Fresh x) = [x]
-reprs (Alias x xs) = x:xs
+reprs (Unknown x xs) = x:xs
 -}
 getId :: ActorId -> Int
 getId (Fresh x _) = x
-getId (Alias x  ) = x
+getId (Unknown x  ) = x
 getId _ = panic "getId" 
           "Trying to get ActorId of ActorTPVar, which should have been instantiated"
 
 {-
 reprName :: ActorId -> Name
 reprName (Fresh _ n)   = n
-reprName (Alias _ _ n) = n
+reprName (Unknown _ _ n) = n
 -}
 
-newAlias :: Uniq -> IO ActorId
-newAlias u = do uniq <- getUniq u
-                return $ Alias uniq
+newUnknown :: Uniq -> IO ActorId
+newUnknown u = do uniq <- getUniq u
+                  return $ Unknown uniq
 
 newFresh :: Uniq -> String -> IO ActorId
 newFresh u str = do uniq <- getUniq u
                     return $ Fresh uniq str
 
+newInstance :: Uniq -> Name () -> IO ActorId
+newInstance u n = do uniq <- getUniq u
+                     return $ Instance n uniq
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
@@ -26,6 +26,7 @@
 splitCstrs (LRT g ls p q) = map (\x -> LRT g ls x q) (disjoin p)
     where disjoin :: (TcPolicy TcActor) -> [TcPolicy TcActor]
           disjoin (Join p1 p2) = (disjoin p1)++(disjoin p2)
+          disjoin (Meet p1 _p2) = disjoin p1 -- TODO: Ugly strategy!!
           disjoin p' = [p']
 
 
@@ -39,9 +40,9 @@
   case mpol of
     Nothing -> return True 
     Just _  -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""
-isCstrVar (LRT _ _ _ (Join _ _)) 
+isCstrVar (LRT _ _ _ _) 
     = panic (constraintsModule ++ ".isCstrVar") 
-      "Right-side of a constrain shouldn't be a join !"
+      "Right-side of a constraint shouldn't be a join or meet!"
 
 --Check if a given constraint p<=q verifies that q is an unknown policy of a variable
 noVarLeft :: Constraint -> IO Bool
@@ -51,7 +52,8 @@
   case mpol of
     Nothing -> return False
     Just _  -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""
-noVarLeft (LRT g ls (Join p q) r) = (noVarLeft (LRT g ls p r)) `orM` (noVarLeft (LRT g ls q r))
+noVarLeft (LRT g ls (Join p q) r) = noVarLeft (LRT g ls p r) `orM` noVarLeft (LRT g ls q r)
+noVarLeft (LRT g ls (Meet p q) r) = noVarLeft (LRT g ls p r) `orM` noVarLeft (LRT g ls q r)
 
 partitionM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint], [Constraint])
 partitionM f xs = do
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
@@ -27,8 +27,8 @@
        Either Bool Constraint
 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
+      (_, Join _ _) -> Right (LRT g ls p q)
+      (Meet _ _, _) -> Right (LRT g ls p q)
       (RealPolicy rp, RealPolicy rq) -> Left $ lrtReal g ls rp rq
       (Join p1 p2, _) -> let
                     ap1 = lrt g ls p1 q
@@ -38,7 +38,14 @@
                          (Left True, _) -> ap2
                          (_, Left True) -> ap1 
                          _ -> Right (LRT g ls p q)
-
+      (_, Meet q1 q2) -> let
+                    ap1 = lrt g ls p q1
+                    ap2 = lrt g ls p q2
+                    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)
 
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
@@ -23,8 +23,8 @@
      addBranchPC, addBranchPCList,
 
      getActorId, setActorId, 
-     newActorId, newActorIdWith, newAliasId,
-     freshActorId, aliasActorId,
+     newActorId, newActorIdWith, newUnknownId,
+     freshActorId, unknownActorId,
      scrambleActors,
 
      getPolicy,
@@ -91,7 +91,8 @@
 import Language.Java.Paragon.TypeCheck.Containment
 import Language.Java.Paragon.TypeCheck.Constraints
 
-import Control.Monad (filterM, zipWithM)
+import Control.Monad hiding (join) -- (filterM, zipWithM, when)
+--import qualified Control.Monad (join) as Monad
 import Control.Applicative ( (<$>), (<*>) )
 --import Control.Arrow ( first, second )
 import qualified Data.Map as Map
@@ -149,7 +150,7 @@
       newVmap = Map.insert i vti oldVmap
   in env { vars = newVmap }
 
-lookupActorName :: ActorName () -> TcCodeM (TcType, ActorPolicy)
+lookupActorName :: ActorName () -> TcCodeM (TcStateType, ActorPolicy)
 lookupActorName (ActorName _ nam@(Name _ nt mPre i))
     | nt == EName = 
         do (ty, pol, _) <- lookupVar mPre i
@@ -166,35 +167,35 @@
 -- | 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 (Maybe TcType, TypeMap, ActorPolicy)
+lookupPrefixName :: Name () -> TcCodeM (Maybe TcStateType, 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
     -- We can piggyback on lookupVar since its preconditions are met
-    (ty, p, _) <- lookupVar Nothing i
+    (sty, p, _) <- lookupVar Nothing i
+    debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ show sty
     tm <- getTypeMap
-    case lookupTypeOfT ty tm of
-      Right newSig -> return (Just ty, tMembers newSig, p)
+    case lookupTypeOfStateT sty tm of
+      Right newSig -> return (Just sty, tMembers newSig, p)
       Left (Just err) -> fail err
       _ -> panic (monadModule ++ ".lookupPrefixName")
            $ "Unknown variable or field: " ++ show n
 
 lookupPrefixName n@(Name _ nt mPre i) = do
   baseTm <- getTypeMap
-  (preTm, prePol) <- case mPre of
-                       Nothing -> do return (baseTm, bottom)
-                       Just pre -> do
-                                 (_, preTm, prePol) <- lookupPrefixName pre
-                                 return (preTm, prePol)
+  (mPreSty, preTm, prePol) <- case mPre of
+                                Nothing -> do return (Nothing, baseTm, bottom)
+                                Just pre -> lookupPrefixName pre
   baseTm2 <- getTypeMap
   case nt of
     EName -> case Map.lookup i $ fields preTm of
                Just (VSig ty p _ _ _) -> do
                    debugPrint $ "lookupPrefixName: EName: " ++ prettyPrint n ++ 
                                   " :: " ++ prettyPrint ty
-                   debugPrint $ show (packages baseTm2) ++ "\n"
-                   case lookupTypeOfT ty baseTm2 of
-                     Right tsig -> return (Just ty, tMembers tsig, prePol `joinWThis` p)
+                   -- debugPrint $ show (packages baseTm2) ++ "\n"
+                   sty <- getStateType (Just n) mPreSty ty 
+                   case lookupTypeOfStateT sty baseTm2 of
+                     Right tsig -> return (Just sty, tMembers tsig, prePol `joinWThis` p)
                      Left (Just err) -> fail err
                      _ -> panic (monadModule ++ ".lookupPrefixName")
                           $ "Unknown type: " ++ show ty
@@ -202,15 +203,17 @@
                           $ "Not a field: " ++ show n
 
     TName -> do
-            (tps, tsig) <- case Map.lookup i $ types preTm of
-                             Nothing -> liftTcDeclM $ fetchType n
-                   -- panic (monadModule ++ ".lookupPrefixName")
-                   -- $ "Not a type: " ++ show n
-                             Just tinfo -> return tinfo
-            check (null tps) $
-                      "Type " ++ prettyPrint n ++ " expects " ++ 
-                      show (length tps) ++ " but has been given none."
-            return (Just $ TcRefT $ tType tsig, tMembers tsig, prePol)
+            (_tps, _iaps, tsig) <- case Map.lookup i $ types preTm of
+                                     Nothing -> liftTcDeclM $ fetchType n
+                                     -- panic (monadModule ++ ".lookupPrefixName")
+                                     -- $ "Not a type: " ++ show n
+                                     Just tinfo -> return tinfo
+-- This lookup arises from refering to static fields, and then type arguments aren't given.
+-- TODO: Check that field *is* static.
+--            check (null tps) $
+--                      "Type " ++ prettyPrint n ++ " expects " ++ 
+--                      show (length tps) ++ " but has been given none."
+            return (Just . stateType . TcRefT $ tType tsig, tMembers tsig, prePol)
 
     PName -> case Map.lookup i $ packages preTm of
                Nothing -> do liftTcDeclM $ fetchPkg n
@@ -228,25 +231,34 @@
 
 -- | 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 (TcType, ActorPolicy, Bool)
+lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM (TcStateType, ActorPolicy, Bool)
 lookupVar Nothing i = do
   -- Could be a single variable
+  let nam = Name () EName Nothing i -- Reconstructing for lookups
   varMap <- vars <$> getEnv
   case Map.lookup i varMap of
     -- Is a variable
-    Just (VSig ty p param _ _) -> return (ty, p, param)
+    Just (VSig ty p param _ _) -> do
+                             sty <- getStateType (Just nam) Nothing ty
+                             return (sty, p, param)
     -- Not a variable, must be a field
     Nothing -> do
       tm <- getTypeMap
       case Map.lookup i $ fields tm of
-        Just (VSig ty p param _ _) -> return (ty, p, param)
+        Just (VSig ty p param _ _) -> do
+                  sty <- getStateType (Just nam) Nothing ty
+                  return (sty, p, param)
         Nothing -> panic (monadModule ++ ".lookupVar") 
                    $ "Not a var or field: " ++ show i
 
 lookupVar (Just pre) i = do
   (mPreTy, preTm, prePol) <- lookupPrefixName pre
   case Map.lookup i $ fields preTm of
-    Just (VSig ty p _ _ _) -> return (ty, prePol `joinWThis` p, False)
+    Just (VSig ty p _ _ _) -> do
+        sty <- getStateType (Just (Name () EName (Just pre) i)) mPreTy ty
+        debugPrint $ "lookupVar: " ++ prettyPrint pre ++ "." ++ prettyPrint i
+                     ++ " :: " ++ show sty
+        return (sty, prePol `joinWThis` p, False)
     Nothing -> 
         case mPreTy of
           Just preTy -> fail $ "Type " ++ prettyPrint preTy ++
@@ -282,9 +294,9 @@
             | not b && length ps /= length as = return False
             | b && length ps > length as + 1  = return False
         checkTys True [p] [a] = 
-             (p =<: a) `orM` (arrayType p bottom =<: a)
-        checkTys True [p] as = and <$> mapM (p =<:) as
-        checkTys b (p:ps) (a:as) = (&&) <$> (p =<: a) <*> checkTys b ps as
+             (a `isAssignableTo` p) `orM` (a `isAssignableTo` arrayType p bottom)
+        checkTys True [p] as = and <$> mapM (`isAssignableTo` p) as
+        checkTys b (p:ps) (a:as) = (&&) <$> (a `isAssignableTo` p) <*> checkTys b ps as
         checkTys _ _ _ = return False
 
         findBestFit :: [Sig] -> TcCodeM [Sig]
@@ -300,7 +312,7 @@
                    if and bs1 then go xs ys else go (y:xs) ys
 
         moreSpecificThan :: Sig -> Sig -> TcCodeM Bool
-        moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (=<:) ps2 ps1
+        moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (isAssignableTo) ps1 ps2
         moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do
           let n = length ps1
               k = length ps2
@@ -314,6 +326,7 @@
              -> [TcType]           -- Argument types
              -> TcCodeM (ActorPolicy, [TypeParam ()], MethodSig)
 lookupMethod mPre i tArgs argTys = do
+  debugPrint $ "lookupMethod: " ++ show (mPre, i, argTys)
   baseTm <- getTypeMap
   (mPreTy, preTm, prePol) <- case mPre of
                               Nothing -> return (Nothing, baseTm, bottom)
@@ -383,23 +396,23 @@
     Just p -> return p
 
 
-lookupFieldT :: TcType -> Ident () -> TcCodeM VarFieldSig
+lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig
 lookupFieldT typ i = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
-  aSig <- lookupTypeOfType typ
+  aSig <- lookupTypeOfStateType typ
   case Map.lookup i (fields $ tMembers aSig) of
     Just vti -> return vti
     Nothing -> fail $ "Class " ++ prettyPrint typ
                       ++ " does not have a field named " ++ prettyPrint i
   
-lookupMethodT :: TcType 
+lookupMethodT :: TcStateType 
               -> Ident () 
               -> [TypeArgument ()] 
               -> [TcType] 
               -> TcCodeM ([TypeParam ()], MethodSig)
 lookupMethodT typ i tArgs argTys = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
-  aSig <- lookupTypeOfType typ
+  aSig <- lookupTypeOfStateType typ
   case Map.lookup i (methods $ tMembers aSig) of
     Nothing -> fail $ "Class " ++ prettyPrint typ
                       ++ " does not have a method named " ++ prettyPrint i
@@ -429,15 +442,15 @@
 lookupConstr :: TcClassType 
              -> [TypeArgument ()]
              -> [TcType] 
-             -> TcCodeM ([TypeParam ()], ConstrSig)
+             -> TcCodeM ([TypeParam ()], [Ident ()], ConstrSig)
 lookupConstr ctyp tArgs argTys = do
-  debugPrint $ "\n\n######## Looking up constructor! ######## \n"
+--  debugPrint $ "\n\n######## Looking up constructor! ######## \n"
   let typ = clsTypeToType ctyp
-  debugPrint $ "typ: " ++ show typ
-  aSig <- lookupTypeOfType typ
-  debugPrint $ "aSig: " ++ show aSig
+--  debugPrint $ "typ: " ++ show typ
+  (iaps, aSig) <- lookupTypeOfType typ
+--  debugPrint $ "aSig: " ++ show aSig
   let cMap = constrs $ tMembers aSig
-  debugPrint $ "cMap: " ++ show cMap
+--  debugPrint $ "cMap: " ++ show cMap
   bests <- findBestMethod tArgs argTys (Map.keys cMap)
   case bests of
     [] -> fail $ "Type " ++ prettyPrint ctyp ++
@@ -455,7 +468,7 @@
         case Map.lookup sig cMap of
               Nothing -> panic (monadModule ++ ".lookupConstr")
                          $ "Sig must be one of the keys of constrMap: " ++ show sig
-              Just csig -> return (tps, csig)
+              Just csig -> return (tps, iaps, csig)
                  
 
 --lookupLock :: Name () -> TcCodeM LockSig
@@ -548,13 +561,131 @@
 startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty }
 -}
 
+-- Instance analysis
+
+getStateType :: Maybe (Name ())          -- field/var name (if decidable) 
+             -> Maybe TcStateType        -- containing object state type
+             -> TcType                   -- field/var/cell type
+             -> TcCodeM TcStateType
+getStateType mn mtyO ty 
+    | ty == actorT   = do actorIdT <$> getActorId mn mtyO
+    | ty == policyT  = do policyPolT <$> getPolicyBounds mn mtyO
+    | Just ct <- mClassType ty = instanceT ct <$> getInstanceActors mn ct
+    | otherwise = return $ stateType ty
+
+registerStateType :: Ident ()
+                  -> TcType
+                  -> Maybe (TcStateType) -> TcCodeM TcStateType
+registerStateType i tyV mSty | tyV == actorT = do
+  case mSty of
+    Nothing -> actorIdT <$> newActorId i -- fresh generation
+    Just sty -> case mActorId sty of
+                  Nothing -> panic (monadModule ++ ".registerStateType")
+                             $ "Actor state but non-actor target type: " 
+                                  ++ show (tyV, sty)
+                  Just aid -> do
+                    newActorIdWith i aid
+                    return $ actorIdT aid
+
+registerStateType i tyV mSty | tyV == policyT = do
+  let pbs = case mSty of
+              Nothing -> PolicyBounds bottom top
+              Just sty -> case mPolicyPol sty of
+                            Nothing -> panic (monadModule ++ ".registerStateType")
+                                       $ "Policy state but non-policy target type: "
+                                             ++ show (tyV, sty)
+                            Just bs -> bs
+  updateState $ \s -> 
+      s { policySt = Map.insert (mkSimpleName EName i) pbs $ policySt s }
+  return $ policyPolT pbs
+
+registerStateType i tyV mSty | Just ct <- mClassType tyV = do
+    debugPrint $ "registerStateType: " ++ show (i, tyV, mSty)
+    case mSty of
+      -- no initialiser
+      Nothing -> return $ instanceT ct [] -- ??
+      Just sty -> case mInstanceType sty of
+                    Just (_, aids) -> do
+                      updateState $ \s ->
+                          s { instanceSt = Map.insert (mkSimpleName EName i) aids 
+                                           $ instanceSt s }
+                      return $ instanceT ct aids
+                    Nothing | isNullType sty -> return $ instanceT ct []
+                            | otherwise -> panic (monadModule ++ ".registerStateType")
+                               $ "Instance state but non-instance target type: "
+                                         ++ show (tyV, sty)
+                                                  
+
+
+registerStateType _i tyV _mSty = return $ stateType tyV
+
+updateStateType :: Maybe (Name ())       -- field/var name (if decidable)
+                -> Maybe (TcType)        -- Containing object type
+                -> TcType                -- field/var/cell type
+                -> Maybe TcStateType     -- rhs state type (Nothing if no init)
+                -> TcCodeM TcStateType
+updateStateType mN mTyO tyV mSty | tyV == actorT = do
+  case mSty of
+    Just sty | Just aid <- mActorId sty -> do
+                                maybeM mTyO $ \tyO -> scrambleActors (Just tyO)
+                                maybeM mN $ \n -> setActorId n aid
+                                return sty
+
+             | otherwise -> panic (monadModule ++ ".updateStateType")
+                            $ "Actor state but non-actor target type: " 
+                                  ++ show (tyV, sty)
+    Nothing -> panic (monadModule ++ ".updateStateType")
+               $ "No state for actor assignment: " ++ show mN
+
+-- TODO
+{-
+updateStateType mN mTyO tyV mSty | tyV == policyT = do
+  case mSty of
+    Just sty | Just pbs <- mPolicyPol sty -> do
+-}
+updateStateType _mN _mTyO _ty (Just sty) = return sty
+updateStateType _mN _mTyO ty Nothing     = return $ stateType ty
+
+
+-- Instance Analysis
+
+getInstanceActors :: Maybe (Name ()) -> TcClassType -> TcCodeM [ActorId]
+getInstanceActors mn ct@(TcClassT tyN _) = do
+  instanceMap <- instanceSt <$> getState
+  case maybe Nothing (\n -> Map.lookup n instanceMap) mn of
+    Nothing  -> do
+      (iaps, _) <- lookupTypeOfType (clsTypeToType ct)
+      mapM (instanceActorId . Name () EName (Just tyN)) iaps
+    Just aids -> return aids
+  
+-- Policy Analysis
+
+getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds
+getPolicyBounds mn mtyO = do
+  policyMap <- policySt <$> getState
+  case maybe Nothing (\n -> Map.lookup n policyMap) mn of
+    Nothing -> case (mtyO, mn) of
+                 (Just styO, Just (Name _ _ _ i)) -> do
+                           tsig <- lookupTypeOfStateType styO
+                           case Map.lookup i $ policies $ tMembers tsig of
+                             Just pol -> return $ KnownPolicy pol
+                             Nothing  -> return $ PolicyBounds bottom top
+                 _ -> return $ PolicyBounds bottom top
+    Just pif -> return pif
+
 -- Actor Analysis
 
-getActorId :: Name () -> TcCodeM ActorId
-getActorId n = do
-  actorMap <- actorSt <$> getState
-  case Map.lookup n actorMap of
-    Nothing -> liftTcDeclM $ aliasActorId
+getActorId :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorId
+getActorId mn mtyO = do
+  actorMap <- actorSt <$> getState  
+  case maybe Nothing (\n -> Map.lookup n actorMap) mn of
+    Nothing -> case (mtyO, mn) of
+                 (Just styO, Just (Name _ _ _ i)) -> do
+                           tsig <- lookupTypeOfStateType styO
+                           case Map.lookup i $ actors $ tMembers tsig of
+                             Just aid -> return aid
+                             Nothing  -> liftTcDeclM $ unknownActorId
+                 _ -> liftTcDeclM $ unknownActorId
     Just ai -> return $ aID ai
 
 setActorId :: Name () -> ActorId -> TcCodeM ()
@@ -577,9 +708,9 @@
   newActorIdWith i aid
   return aid
 
-newAliasId :: Ident () -> TcCodeM ActorId
-newAliasId i = do
-  aid <- liftTcDeclM aliasActorId
+newUnknownId :: Ident () -> TcCodeM ActorId
+newUnknownId i = do
+  aid <- liftTcDeclM unknownActorId
   newActorIdWith i aid
   return aid
 
@@ -689,11 +820,10 @@
 getGlobalLockProps :: TcCodeM [TcClause TcAtom]
 getGlobalLockProps = do
   cs <- go <$> getTypeMap
-  debugPrint $ "Fetching global lock props: " ++ show 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
+                        tlps = map (go . tMembers . (\(_,_,x) -> x)) $ Map.elems $ types tm
                         plps = map go $ Map.elems $ packages tm
                     in concat $ lps ++ tlps ++ plps
 
@@ -725,18 +855,18 @@
     case Map.lookup exnTy exnMap of
       Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy)
       Just (rE, wE) -> do
-        constraint [] wX wE $
+        constraint [] wE wX $
                     "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++
                     callerSort ++ " " ++ callerName ++ ", has write effect " ++
                     prettyPrint wX ++
                     " but the context in which the " ++ callerSort ++ 
                     " is invoked expects its write effect to be no less restrictive than " ++ 
                     prettyPrint wE
-        constraint [] rE rX $  -- constraintLS?
+        constraint [] rX rE $  -- constraintLS?
                     "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++
                     callerSort ++ " " ++ callerName ++ ", has policy " ++ prettyPrint rX ++
                     " but the context in which the " ++ callerSort ++ 
-                    " is invoked expects its policy to be no less restrictive than " ++ 
+                    " is invoked expects its policy to be no more restrictive than " ++ 
                     prettyPrint rE
 
 
@@ -748,18 +878,19 @@
 -- 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, (=<:) :: MonadTcDeclM m => TcType -> TcType -> m Bool
+isAssignableTo :: MonadTcDeclM m => TcType -> TcType -> m Bool
 isAssignableTo t1 t2 = liftTcDeclM $ 
     if t1 == t2 -- identity conversion
      then return True
      else t1 `widensTo` t2 -- widening conversion
 
-(=<:) = flip isAssignableTo
+(=<:) :: MonadTcDeclM m => TcType -> TcStateType -> m Bool
+lhs =<: rhs = isAssignableTo (unStateType rhs) lhs
 
-isCastableTo, (<<:) :: MonadTcDeclM m
-                    => TcType 
-                        -> TcType 
-                        -> m (Bool, Bool) -- (Can be cast, needs reference narrowing)
+isCastableTo :: MonadTcDeclM m
+                => TcType 
+                    -> TcType 
+                    -> 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.
@@ -787,7 +918,8 @@
                      return (True, True)
        _ -> return (False, False)
 
-(<<:) = flip isCastableTo
+(<<:) :: MonadTcDeclM m => TcType -> TcStateType -> m (Bool, Bool)
+lhs <<: rhs = isCastableTo (unStateType rhs) lhs
 
 
 -- widening conversion can come in four basic shapes:
@@ -806,10 +938,11 @@
       TcClsRefT ct -> maybe (return False) 
                         (\pt -> TcPrimT pt `widensTo` t2) (unbox ct)
       _ -> return False
--- 5) Paragon-specific types
+{-- 5) Paragon-specific types
 widensTo t1 t2 | isPolicyType t1 && t2 == policyT  = return True
                | isLockType   t1 && t2 == booleanT = return True
                | isActorType  t1 && t2 == actorT   = return True
+-}
 widensTo _ _ = return False
 
 subTypeOf :: TcRefType -> TcRefType -> TcDeclM Bool
@@ -822,18 +955,17 @@
                     Left Nothing -> do
                           case rt of
                             TcClsRefT (TcClassT n tas) -> do
-                               (tps, tsig) <- fetchType n
+                               (tps, _iaps, tsig) <- fetchType n
                                return $ instantiate (zip tps tas) tsig
                             _ -> panic (monadModule ++ ".subTypeOf")
                                  $ show rt
                           
                     Left err -> panic (monadModule ++ ".subTypeOf")
                                 $ "Looking up type:" ++ show rt ++ "\nError: " ++ show err
-                    Right tsig -> return tsig
+                    Right (_,tsig) -> return tsig
           let sups  = tSupers tsig
               impls = tImpls tsig
---              obj   = if null sups then [objectT] else []
-              allS  = map TcClsRefT $ sups ++ impls -- ++ obj
+              allS  = map TcClsRefT $ sups ++ impls
           supsups <- mapM superTypes allS
           return $ concat $ allS:supsups
 
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs b/src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs
@@ -1,4 +1,8 @@
-module Language.Java.Paragon.TypeCheck.Monad.CodeState where
+module Language.Java.Paragon.TypeCheck.Monad.CodeState
+    (
+     module Language.Java.Paragon.TypeCheck.Monad.CodeState,
+     PolicyBounds(..), ActorPolicy, ActorPolicyBounds
+    ) where
 
 import Language.Java.Paragon.Syntax
 import Language.Java.Paragon.Pretty
@@ -14,14 +18,17 @@
 import qualified Data.Map as Map
 import Data.List (intersect, union)
 import Data.Maybe (fromJust)
+import Control.Monad (zipWithM {-, when -})
 
 codeStateModule :: String
 codeStateModule = typeCheckerBase ++ ".Monad.CodeState"
 
 data CodeState = CodeState {
-      actorSt   :: ActorMap,
-      lockMods  :: LockMods,
-      exnS      :: ExnsMap
+      actorSt    :: ActorMap,
+      policySt   :: PolicyMap,
+      instanceSt :: InstanceMap,
+      lockMods   :: LockMods,
+      exnS       :: ExnsMap
     }
   deriving (Eq, Show)
 
@@ -32,15 +39,101 @@
 
 mergeStates :: Uniq -> CodeState -> CodeState -> IO CodeState
 mergeStates u s1 s2 = do
-  newActors <- mergeActors u (actorSt s1) (actorSt s2)
-  newExns   <- mergeExns   u (exnS   s1) (exnS   s2)
+  newActors <- mergeActors    u (actorSt    s1) (actorSt    s2)
+  newPols   <- mergePolicies    (policySt   s1) (policySt   s2)
+  newInsts  <- mergeInstances u (instanceSt s1) (instanceSt s2)
+  newExns   <- mergeExns      u (exnS       s1) (exnS       s2)
   return $ CodeState { 
-               actorSt = newActors,
-               lockMods = lockMods s1 <++> lockMods s2,
-               exnS = newExns
+               actorSt    = newActors,
+               policySt   = newPols,
+               instanceSt = newInsts,
+               lockMods   = lockMods s1 <++> lockMods s2,
+               exnS       = newExns
              }
 
 ------------------------------------------
+-- Instance tracking
+------------------------------------------
+
+type InstanceMap = Map.Map (Name ()) [ActorId]
+{-type InstanceMap = Map.Map (Ident ()) InstanceSig
+
+data InstanceSig = ISig {
+      iType :: TcType,
+      iImplActorArgs :: [ActorId],
+      iMembers :: InstanceMap
+    }
+  deriving (Show, Eq)
+                 
+mergeInstances :: Uniq -> InstanceMap -> InstanceMap -> IO InstanceMap
+mergeInstances u im1 im2 = do
+    let newKeys = Map.keys im1 `intersect` Map.keys im2
+        oldVals = map (\k -> (fromJust (Map.lookup k im1), fromJust (Map.lookup k im2))) newKeys
+    newVals <- mapM mergeISigs oldVals
+    return $ Map.fromList $ zip newKeys newVals
+        where mergeISigs :: (InstanceSig, InstanceSig) -> IO InstanceSig
+              mergeISigs (is1, is2) = do
+                             when (iType is1 /= iType is2) $
+                                  panic (codeStateModule ++ ".mergeInstances:mergeISigs")
+                                      $ show (is1, is2)
+                             as <- mergeIas (iImplActorArgs is1) (iImplActorArgs is2)
+                             newMems <- mergeInstances u (iMembers is1) (iMembers is2)
+                             return $ ISig (iType is1) as newMems
+
+              mergeIas :: [ActorId] -> [ActorId] -> IO [ActorId]
+              mergeIas ias1 ias2 = zipWithM mergeIa ias1 ias2
+              
+              mergeIa :: ActorId -> ActorId -> IO ActorId
+              mergeIa ai1 ai2 
+                  | ai1 == ai2 = return ai1
+              mergeIa (Instance n _) _ = newInstance u n
+              mergeIa ai _ = panic (codeStateModule ++ ".mergeIas")
+                             $ "Instance has non-instance implicit argument: " ++ show ai
+
+-}
+
+mergeInstances :: Uniq -> InstanceMap -> InstanceMap -> IO InstanceMap
+mergeInstances u im1 im2 = do
+    let newKeys = Map.keys im1 `intersect` Map.keys im2
+        oldVals = map (\k -> (fromJust (Map.lookup k im1), fromJust (Map.lookup k im2))) newKeys
+    newVals <- mapM (uncurry mergeIas) oldVals
+    return $ Map.fromList $ zip newKeys newVals
+        where mergeIas :: [ActorId] -> [ActorId] -> IO [ActorId]
+              mergeIas ias1 ias2 = zipWithM mergeIa ias1 ias2
+              
+              mergeIa :: ActorId -> ActorId -> IO ActorId
+              mergeIa ai1 ai2 
+                  | ai1 == ai2 = return ai1
+              mergeIa (Instance n _) _ = newInstance u n
+              mergeIa ai _ = panic (codeStateModule ++ ".mergeIas")
+                             $ "Instance has non-instance implicit argument: " ++ show ai
+
+------------------------------------------
+-- Policy tracking
+------------------------------------------
+
+type PolicyMap = Map.Map (Name ()) ActorPolicyBounds
+
+mergePolicies :: PolicyMap -> PolicyMap -> IO PolicyMap
+mergePolicies pm1 pm2 = do
+    let newKeys = Map.keys pm1 `intersect` Map.keys pm2
+        oldVals = map (\k -> (fromJust (Map.lookup k pm1), fromJust (Map.lookup k pm2))) newKeys
+        newVals = map mergePs oldVals
+    return $ Map.fromList $ zip newKeys newVals
+
+mergePs :: (ActorPolicyBounds, ActorPolicyBounds) -> ActorPolicyBounds
+mergePs pis =
+    case pis of
+      (KnownPolicy p, KnownPolicy q)
+          | p == q    -> KnownPolicy p
+          | otherwise ->  mkBounds p q p q
+      (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2
+      (KnownPolicy  p,     PolicyBounds q1 q2) -> mkBounds p  q1 p  q2
+      (PolicyBounds p1 p2, KnownPolicy  q    ) -> mkBounds p1 q  p2 q
+
+  where mkBounds a b c d = PolicyBounds (a `meet` b) (c `join` d)
+
+------------------------------------------
 -- Actor analysis
 ------------------------------------------
 
@@ -65,7 +158,7 @@
 scramble' :: Uniq -> Stability -> ActorInfo -> IO ActorInfo
 scramble' u stab a@(AI _ stab') =
     if scrambles stab stab' 
-     then do aid' <- newAlias u
+     then do aid' <- newUnknown u
              return $ AI aid' stab'
      else return a
              
@@ -73,14 +166,14 @@
 mergeActors :: Uniq -> ActorMap -> ActorMap -> IO ActorMap
 mergeActors u a1 a2 = do
     let newKeys = Map.keys a1 `intersect` Map.keys a2
-        oldVals = map (\k -> (fromJust (Map.lookup k a1), fromJust (Map.lookup k a1))) newKeys
+        oldVals = map (\k -> (fromJust (Map.lookup k a1), fromJust (Map.lookup k a2))) newKeys
     newVals <- mapM (mergeInfo u) oldVals
     return $ Map.fromList $ zip newKeys newVals
 
 mergeInfo :: Uniq -> (ActorInfo, ActorInfo) -> IO ActorInfo
 mergeInfo _ (ai1,ai2) | ai1 == ai2 = return ai1
 mergeInfo u ((AI _ st),_) = do
-  aid <- newAlias u
+  aid <- newUnknown u
   return $ AI aid st
 
 ------------------------------------------
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
@@ -44,7 +44,8 @@
 setupStartState = do
   tm <- getTypeMap
   let aMap = gatherActorInfo tm
-  return $ CodeState aMap noMods Map.empty
+      pMap = gatherPolicyBounds tm
+  return $ CodeState aMap pMap Map.empty noMods Map.empty -- TODO: Will fields affect instances?
 
 
 gatherActorInfo :: TypeMap -> Map (Name ()) ActorInfo
@@ -54,7 +55,7 @@
               let acts = Map.assocs $ actors tm -- :: [(Ident, ActorId)]
                   aMap = Map.fromList $ map (mkInfo mPre $ fields tm) acts
                   tMap = gatherActorInfoAux TName mPre 
-                           (Map.assocs $ Map.map (tMembers . snd) $ types tm)
+                           (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm)
                   pMap = gatherActorInfoAux PName mPre (Map.assocs $ packages tm)
               in foldl1 Map.union [aMap, tMap, pMap]
 
@@ -81,6 +82,39 @@
                     aux (i,tm) = 
                         let pre = Name () nt mPre i
                         in gatherActorInfo' (Just pre) tm
+
+-- TODO: non-final policies should have bounds bottom/top
+gatherPolicyBounds :: TypeMap -> Map (Name ()) ActorPolicyBounds
+gatherPolicyBounds = gatherPolicyBounds' Nothing
+
+    where gatherPolicyBounds' mPre tm =
+              let pols = Map.assocs $ policies tm -- :: [(Ident, ActorPolicy)]
+                  aMap = Map.fromList $ map (mkPols mPre $ fields tm) pols
+                  tMap = gatherPolicyBoundsAux TName mPre
+                           (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm)
+                  pMap = gatherPolicyBoundsAux PName mPre (Map.assocs $ packages tm)
+              in foldl1 Map.union [aMap, tMap, pMap]
+
+          mkPols :: Maybe (Name ())
+                 -> Map (Ident ()) VarFieldSig 
+                 -> (Ident (), ActorPolicy) 
+                 -> (Name (), ActorPolicyBounds)
+          mkPols mPre fs (i,p) = 
+              case Map.lookup i fs of
+                Just _ -> (Name () EName mPre i, KnownPolicy p)
+                _ -> panic (tcCodeMonadModule ++ ".gatherActorInfo") $ 
+                     "No field for corresponding actor " ++ show i
+
+          gatherPolicyBoundsAux :: NameType 
+                              -> Maybe (Name ()) 
+                              -> [(Ident (), TypeMap)] 
+                              -> Map (Name ()) ActorPolicyBounds
+          gatherPolicyBoundsAux nt mPre = foldl Map.union Map.empty . map aux
+              where aux :: (Ident (), TypeMap) -> Map (Name ()) ActorPolicyBounds
+                    aux (i,tm) = 
+                        let pre = Name () nt mPre i
+                        in gatherPolicyBounds' (Just pre) tm
+
 
 
 -- Running in parallel
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
@@ -9,7 +9,8 @@
 
      fetchPkg, fetchType,
 
-     getTypeMap, getThisType, getSuperType, lookupTypeOfType,
+     getThisType, getThisStateType, getSuperType, 
+     getTypeMap, lookupTypeOfType, lookupTypeOfStateType,
 
      withTypeParam, extendGlobalTypeMap,
 
@@ -21,7 +22,7 @@
      evalLock, evalActor,
      evalSrcLockProps,
 
-     freshActorId, aliasActorId,
+     freshActorId, unknownActorId, instanceActorId,
 
      getReadPolicy, getWritePolicy, getLockPolicy,
      getParamPolicy, getReturnPolicy,
@@ -47,16 +48,31 @@
 
 import qualified Data.Map as Map
 import Data.List (partition)
+import Data.Maybe (catMaybes)
 
 tcDeclMModule :: String
 tcDeclMModule = typeCheckerBase ++ ".Monad.TcDeclM"
 
 type TypeCheck m ast = ast () -> m (ast T)
 
-lookupTypeOfType :: MonadTcDeclM m => TcType -> m TypeSig
+lookupTypeOfStateType :: MonadTcDeclM m => TcStateType -> m TypeSig
+lookupTypeOfStateType sty {-@(TcInstance{})-} = liftTcDeclM $ do
+  tm <- getTypeMap
+  case lookupTypeOfStateT sty tm of
+    Right tsig -> return tsig
+    Left Nothing -> fail $ "Unknown type: " ++ prettyPrint sty
+    Left (Just err) -> fail err
+{-
+lookupTypeOfStateType _sty@(TcType ty) = liftTcDeclM $ do
+  tm <- getTypeMap
+  case lookupTypeOfT ty tm of
+    Right (is, tsig) -> do
+      ias <- mapM (instanceActorId . Name () EName 
+-}
+lookupTypeOfType :: MonadTcDeclM m => TcType -> m ([Ident ()], TypeSig)
 lookupTypeOfType ty = liftTcDeclM $ do
   tm <- getTypeMap
-  debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm
+--  debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm
   case lookupTypeOfT ty tm of
     Right tsig -> return tsig
     Left Nothing -> fail $ "Unknown type: " ++ prettyPrint ty
@@ -75,7 +91,7 @@
      return ()
                        
 
-fetchType :: Name () -> TcDeclM ([TypeParam ()], TypeSig)
+fetchType :: Name () -> TcDeclM ([TypeParam ()],[Ident ()],TypeSig)
 fetchType n@(Name _ _ _ typName) = do
   withFreshCurrentTypeMap $ do
   debugPrint $ "Fetching type " ++ prettyPrint n ++ " ..."
@@ -100,7 +116,7 @@
                -- if using "clever lookup" instead of "clever setup"
                superTm <- case superTys of
                             [] -> return emptyTM
-                            [superTy] -> tMembers <$> lookupTypeOfType (clsTypeToType superTy)
+                            [superTy] -> tMembers . snd <$> lookupTypeOfType (clsTypeToType superTy)
                             _ -> panic (tcDeclMModule ++ ".fetchType")
                                  $ "More than one super class for class:"  ++ show superTys
 
@@ -112,11 +128,12 @@
                             tImpls   = implsTys,
                             tMembers = superTm { constrs = Map.empty }
                           }
-               extendGlobalTypeMap (extendTypeMapT n tps tsig)
+                   mDs = map unMemberDecl ds
+                   iaps = findImplActorParams mDs
+               extendGlobalTypeMap (extendTypeMapT n tps iaps tsig)
 
 --               (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
@@ -151,7 +168,7 @@
                -- Remove this line, and set tMembers to emptyTM,
                -- if using "clever lookup" instead of "clever setup"
                superTm <- foldl merge emptyTM <$> 
-                            mapM ((tMembers <$>) . lookupTypeOfType . clsTypeToType) superTys
+                            mapM ((tMembers . snd <$>) . lookupTypeOfType . clsTypeToType) superTys
 
                let tsig = TSig {
                             tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],
@@ -162,7 +179,7 @@
                             tMembers = superTm
                           }
 
-               extendGlobalTypeMap (extendTypeMapT n tps tsig)
+               extendGlobalTypeMap (extendTypeMapT n tps [] tsig)
 
 --               withTypeMapAlways (extendTypeMapT n tps tsig) $ do
                withFoldMap withTypeParam tps $ do
@@ -185,6 +202,11 @@
 
 fetchType n = panic (tcDeclMModule ++ ".fetchType") $ show n
 
+findImplActorParams :: [MemberDecl ()] -> [Ident ()]
+findImplActorParams mds = [ i | FieldDecl _ ms [typeQQ| actor |] vds <- mds,
+                                Final () `elem` ms, not (Static () `elem` ms),
+                                VarDecl _ (VarId _ i) Nothing <- vds ]
+
 -- Actors
 
 fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a
@@ -201,26 +223,26 @@
         (sstables, fstables) = partition (\(ms,_) -> Static () `elem` ms) stables
                                
     (ssas, ssvs) <- unzip <$> mapM spawnActorVd sspawns
-    (fsas, fsvs) <- unzip <$> mapM spawnActorVd fspawns
+    (fsas, fsvs) <- unzip <$> mapM paramActorVd fspawns
     (seas, sevs) <- unzip <$> mapM evalActorVd  sstables
     (feas, fevs) <- unzip <$> mapM evalActorVd  fstables
---    (aas, avs) <- unzip <$> mapM aliasActorVd unstables
+--    (aas, avs) <- unzip <$> mapM unknownActorVd unstables
 --    (eas, evs) <- unzip <$> mapM evalActorVd stables
-    let globTM = emptyTM { actors = Map.fromList (ssas ++ seas),
+    let globTM = emptyTM { actors = Map.fromList (ssas ++ fsas ++ seas ++ feas),
                            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"
+--      debugPrint "Actors fetched"
       tdra
     
         
-         where spawnActorVd, evalActorVd --, aliasActorVd
+         where spawnActorVd, evalActorVd, paramActorVd --, unknownActorVd
                    :: ([Modifier ()], VarDecl ())
                    -> TcDeclM ((Ident (), ActorId), (Ident (),VarFieldSig))
-                  -- Only Nothing for initializer
+                  -- Static, only Nothing for initializer
                spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do
                  a <- freshActorId (prettyPrint i)
                  p <- getReadPolicy ms
@@ -229,14 +251,22 @@
                spawnActorVd (_, VarDecl _ arvid _) =
                    fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
+               paramActorVd (ms, VarDecl _ (VarId _ i) _) = do
+                 let a = ActorTPVar i
+                 p <- getReadPolicy ms
+                 let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
+                 return ((i,a),(i,vti))
+               paramActorVd (_, VarDecl _ arvid _) =
+                   fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
+
 {-               -- All non-final
-               aliasActorVd (ms, VarDecl _ (VarId _ i) _) = do
+               unknownActorVd (ms, VarDecl _ (VarId _ i) _) = do
                  p <- getReadPolicy ms
                  let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
-                 a <- aliasActorId
+                 a <- unknownActorId
                  return ((i,a),(i,vti))
 
-               aliasActorVd (_, VarDecl _ arvid _) =
+               unknownActorVd (_, VarDecl _ arvid _) =
                    fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
  -}
                -- Final, with explicit initializer
@@ -248,8 +278,8 @@
                                tm <- getTypeMap
                                case lookupNamed actors nam tm of
                                  Just a -> return a
-                                 Nothing -> aliasActorId --fail "Internal error: no such actor"
-                        _ -> aliasActorId
+                                 Nothing -> unknownActorId --fail "Internal error: no such actor"
+                        _ -> unknownActorId
                  return ((i,a),(i,vti))
 
                evalActorVd (_, VarDecl _ _ Nothing) 
@@ -273,7 +303,7 @@
   let newTM = emptyTM { locks = Map.fromList lsigs }
   extendGlobalTypeMap (extendTypeMapN n $ merge newTM)
   withCurrentTypeMap (merge newTM) $ do
-       debugPrint $ "Locks fetched"
+--       debugPrint $ "Locks fetched"
        tdra
 
 getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM [TcClause TcAtom]
@@ -309,7 +339,7 @@
   extendGlobalTypeMap $ extendTypeMapN n $ merge globTM
   withCurrentTypeMap (merge loclTM) $ do
 --  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do
-                    debugPrint $ "Policies fetched"
+--                    debugPrint $ "Policies fetched"
                     tdra
 
       where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)
@@ -329,7 +359,7 @@
   withCurrentTypeMap (merge newTM) $ do
 --  withTypeMapAlways (extendTypeMapN n 
 --                     (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do
-                    debugPrint "TypeMethods fetched"
+--                    debugPrint "TypeMethods fetched"
                     tdra
 
     where paramsToIdents (i, (ps,b)) = do
@@ -354,7 +384,7 @@
                   methods = methodMap,
                   constrs = constrMap }
     extendGlobalTypeMap $ extendTypeMapN n $ merge newTM
-    debugPrint "Signatures fetched"
+--    debugPrint "Signatures fetched"
     return ()
     
  where
@@ -392,8 +422,8 @@
                    MethodDecl _ ms tps retT i ps exns _ -> do
                            withFoldMap withTypeParam tps $ do
                              tcty <- evalReturnType retT
-                             (pTys, pPols) <- unzip <$> mapM paramInfo ps
-                             rPol <- getReturnPolicy ms pPols 
+                             (pTys, pIs, pPols) <- unzip3 <$> mapM paramInfo ps
+                             rPol <- getReturnPolicy ms pPols
                              wPol <- getWritePolicy ms
                              exs <- mapM eSpecToSig exns
                              expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ]
@@ -402,7 +432,8 @@
                              let mti = MSig {
                                          mRetType = tcty,
                                          mRetPol  = rPol,
-                                         mPars    = pPols,
+                                         mPars    = pIs,
+                                         mParPols = pPols,
                                          mWrites  = wPol,
                                          mExpects = expects,
                                          mLMods   = (closes, opens),
@@ -426,14 +457,15 @@
                  case md of
                    ConstructorDecl _ ms tps _ ps exns _ -> do
                            withFoldMap withTypeParam tps $ do
-                             (pTys, pPols) <- unzip <$> mapM paramInfo ps
+                             (pTys, pIs, pPols) <- unzip3 <$> mapM paramInfo ps
                              wPol <- getWritePolicy ms
                              exs <- mapM eSpecToSig exns
                              expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ]
                              closes  <- mapM evalLock $ concat [ l | Closes  _ l <- ms ]
                              opens   <- mapM evalLock $ concat [ l | Opens   _ l <- ms ]
                              let cti = CSig {
-                                         cPars    = pPols,
+                                         cPars    = pIs,
+                                         cParPols = pPols,
                                          cWrites  = wPol,
                                          cExpects = expects,
                                          cLMods   = (closes, opens),
@@ -462,11 +494,11 @@
                      }
           return (ty, esig)
 
-   paramInfo :: FormalParam () -> TcDeclM (TcType, ActorPolicy)
+   paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)
    paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do
           pPol <- getParamPolicy i ms
           pTy  <- evalSrcType ty
-          return (pTy, pPol)
+          return (pTy, i, pPol)
    paramInfo (FormalParam _ _ _ _ arvid) = 
             fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
 
@@ -484,9 +516,9 @@
               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
+          let lti = LSig top 0 []
           withCurrentTypeMap (\tm ->
-              tm { fields = Map.insert i vti (fields tm) }) $ tcba
+              tm { locks = Map.insert i lti (locks tm) }) $ tcba
       TypeParam _ _i _ -> do
           --withCurrentTypeMap (\tm ->
           --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $ 
@@ -627,8 +659,10 @@
 -------------------------------------------------------------------
 -- Evaluating types
 
-evalReturnType :: Maybe (Type ()) -> TcDeclM TcType
-evalReturnType = maybe (return voidT) evalSrcType
+evalReturnType :: ReturnType () -> TcDeclM TcType
+evalReturnType (VoidType _) = return voidT
+evalReturnType (LockType _) = fail $ "lock as return type not yet implemented" -- return TcLockRetT
+evalReturnType (Type _ t)   = evalSrcType t
 
 evalSrcType :: Type () -> TcDeclM TcType
 evalSrcType (PrimType _ pt) = return $ TcPrimT pt
@@ -650,15 +684,15 @@
   debugPrint $ "Evaluating class type: " ++ show ct
   baseTm <- getTypeMap
   -- debugPrint $ "Current type map: " ++ show baseTm
-  (tps, _tsig) <- case lookupNamed types n baseTm of
-                    Nothing -> fetchType n 
-                            -- fail $ "Unknown type: " ++ prettyPrint n
-                    Just res -> return res
+  (tps,_iaps,_tsig) <- case lookupNamed types n baseTm of
+                         Nothing -> fetchType n 
+                                    -- fail $ "Unknown type: " ++ prettyPrint n
+                         Just res -> return res
 
-  debugPrint $ "Type found"
+--  debugPrint $ "Type found"
   tArgs <- mapM (uncurry evalSrcTypeArg) (zip tps tas)
-  debugPrint "Type arguments evaluated"
-  return $ TcClassT n tArgs
+--  debugPrint "Type arguments evaluated"
+  return $ TcClassT n tArgs -- TODO: Is this where I evaluate? Likely not.
 {-
       where aux :: TypeMap                            -- Typemap of outer type (or top-level)
                 -> [(Ident (), [TcTypeArg])]          -- Accumulated type (reversed)
@@ -761,7 +795,7 @@
   tm <- getTypeMap
   case lookupNamed actors n tm of
     Just aid -> return aid
-    Nothing -> aliasActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n
+    Nothing -> unknownActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n
 
 evalAtom :: Atom () -> TcDeclM TcAtom
 evalAtom (Atom _ n as) = TcAtom n <$> mapM evalActor as
@@ -780,7 +814,7 @@
                                   " but now it doesn't exist!"
                 Left (Just err) -> panic (tcDeclMModule ++ ".evalLock")
                                    $ err
-                Right tsig -> return $ tMembers tsig
+                Right (_, tsig) -> return $ tMembers tsig
 
   case Map.lookup i $ locks tm of
     Just lsig -> do
@@ -798,7 +832,7 @@
 evalSrcLockProps _ Nothing = return []
 evalSrcLockProps i (Just (LockProperties _ lcs)) = do
   cs <- mapM (evalLClause i) lcs
-  debugPrint $ "Properties: " ++ show cs
+--  debugPrint $ "Properties: " ++ show cs
   return cs
 
 evalLClause :: Ident () -> LClause () -> TcDeclM (TcClause TcAtom)
@@ -820,12 +854,14 @@
     Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n
 getActor (ActorTypeVar _ i) = return $ ActorTPVar i
 
-freshActorId :: String -> TcDeclM ActorId
+freshActorId :: MonadBase m => String -> m ActorId
 freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef
 
-aliasActorId :: TcDeclM ActorId
-aliasActorId = (liftIO . newAlias) =<< getUniqRef
+unknownActorId :: MonadBase m => m ActorId
+unknownActorId = (liftIO . newUnknown) =<< getUniqRef
   
+instanceActorId :: MonadBase m => Name () -> m ActorId
+instanceActorId n = (liftIO . flip newInstance n) =<< getUniqRef
 
 {-----------------------------------------------------
 -- The continuation monad
@@ -957,10 +993,17 @@
 getThisType :: MonadTcDeclM m => m TcClassType
 getThisType = liftTcDeclM getThisTypeTB
 
+getThisStateType :: MonadTcDeclM m => m TcStateType
+getThisStateType = do
+  ct <- getThisType
+  (is, tsig) <- lookupTypeOfType $ clsTypeToType ct
+  let aids = catMaybes $ map (\i -> Map.lookup i $ actors $ tMembers tsig) is
+  return $ instanceT ct aids
+
 getSuperType :: MonadTcDeclM m => m TcClassType
 getSuperType = do
   thisTy <- getThisType
-  thisSig <- lookupTypeOfType (clsTypeToType thisTy)
+  (_, thisSig) <- lookupTypeOfType (clsTypeToType thisTy)
   case tSupers thisSig of
     [] -> return objectT
     [s] -> return s
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,14 +1,16 @@
 {-# 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(..),
+     IsPolicy(..),
+     bottom, top, thisP, joinWThis, isTop, isBottom,
+     TcPolicy(..), PrgPolicy(..), PolicyBounds(..), 
+     TcClause(..), TcAtom(..), TcActor(..), TcMetaVar(..),
      {- toPolicyLit, -} {-toRecPolicy,-}
      lockToAtom, 
      {-zonkPolicy,-} substPolicy, firstRigid, substThis,
      flowAtomString,
 
-     ActorPolicy, AtomPolicy
+     ActorPolicy, AtomPolicy, ActorPolicyBounds
     ) where
 
 import Language.Java.Paragon.Syntax
@@ -39,6 +41,7 @@
 
 data TcPolicy a = RealPolicy (PrgPolicy a) 
                 | Join (TcPolicy a) (TcPolicy a)
+                | Meet (TcPolicy a) (TcPolicy a)
                 | VarPolicy (TcMetaVar a)
   deriving (Eq, Ord, Show, Data, Typeable)
 
@@ -50,17 +53,15 @@
   deriving (Eq,Ord,Show,Data,Typeable)
   
 
-{-
-data VarPolicy a = VPolicy [TcClause a]
-                 | VRigidVar (Ident ())
-                 | VThis
-                 | VJoin (VarPolicy a) (VarPolicy a)
-                 | VMeet (VarPolicy a) (VarPolicy a)
-                 | VMetaVar a
-  deriving (Eq,Ord,Show,Data,Typeable)
--}
+data PolicyBounds a
+    = KnownPolicy (TcPolicy a)
+    -- | Invariant: For 'PolicyBounds p q', p <= q
+    | PolicyBounds (TcPolicy a) (TcPolicy a)
+  deriving (Eq, Ord, Show, Data, Typeable)
 
+
 type ActorPolicy = TcPolicy TcActor
+type ActorPolicyBounds = PolicyBounds TcActor
 
 type AtomPolicy = TcPolicy TcAtom
 
@@ -113,6 +114,7 @@
 instance Pretty a => Pretty (TcPolicy a) where
     pretty (RealPolicy p) = pretty p
     pretty (Join p1 p2) = pretty p1 <+> char '*' <+> pretty p2
+    pretty (Meet p1 p2) = pretty p1 <+> char '+' <+> pretty p2
     pretty (VarPolicy mv) = pretty mv
 
 instance Pretty (TcMetaVar a) where
@@ -128,6 +130,10 @@
   pretty (TcActor aid) = pretty aid
   pretty (TcVar i) = char '\'' <> pretty i
 
+instance Pretty a => Pretty (PolicyBounds a) where
+  pretty (KnownPolicy p) = pretty p
+  pretty (PolicyBounds p q) = pretty p <> char '/' <> pretty q
+
 mkSimpleLName :: Ident () -> Name ()
 mkSimpleLName i = Name () LName Nothing i
 
@@ -178,6 +184,8 @@
   toPolicy :: PrgPolicy a -> p a
   fromPolicy :: p a -> Maybe (PrgPolicy a)
   includesThis :: p a -> Bool
+  join :: p TcActor -> p TcActor -> p TcActor
+  meet :: p TcActor -> p TcActor -> p TcActor
 
 instance IsPolicy PrgPolicy where
   toPolicy = id
@@ -188,6 +196,9 @@
   includesThis (TcMeet p q) = any includesThis [p,q]
   includesThis _ = False
 
+  join = lub
+  meet = glb
+
 instance IsPolicy TcPolicy where
   toPolicy = RealPolicy
   fromPolicy (RealPolicy p) = Just p
@@ -197,6 +208,34 @@
   includesThis (RealPolicy p) = includesThis p
   includesThis _ = False
 
+  join (RealPolicy p) (RealPolicy q) = RealPolicy $ p `lub` q
+  join p q = Join p q
+
+  meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q
+  meet p q = Meet p q
+
+instance IsPolicy PolicyBounds where
+  toPolicy = KnownPolicy . toPolicy
+  fromPolicy (KnownPolicy p) = fromPolicy p
+  fromPolicy _ = Nothing
+
+  includesThis (KnownPolicy p) = includesThis p
+  includesThis (PolicyBounds pb pt) = any includesThis [pb,pt]
+
+  join pb qb = case (pb,qb) of
+      (KnownPolicy p, KnownPolicy q) -> KnownPolicy $ p `join` q
+      (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2
+      (KnownPolicy  p,     PolicyBounds q1 q2) -> mkBounds p  q1 p  q2
+      (PolicyBounds p1 p2, KnownPolicy  q    ) -> mkBounds p1 q  p2 q
+    where mkBounds a b c d = PolicyBounds (a `join` b) (c `join` d)
+  meet pb qb = case (pb,qb) of
+      (KnownPolicy p, KnownPolicy q) -> KnownPolicy $ p `meet` q
+      (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2
+      (KnownPolicy  p,     PolicyBounds q1 q2) -> mkBounds p  q1 p  q2
+      (PolicyBounds p1 p2, KnownPolicy  q    ) -> mkBounds p1 q  p2 q
+    where mkBounds a b c d = PolicyBounds (a `meet` b) (c `meet` d)
+
+
 bottom, top, thisP :: IsPolicy pol => pol TcActor
 bottom = toPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []]
 top = toPolicy $ TcPolicy []
@@ -224,6 +263,7 @@
 lubWThis p q = lub p q
 
 lub :: (PrgPolicy TcActor) -> (PrgPolicy TcActor) -> (PrgPolicy TcActor)
+lub p1 p2 | p1 == p2 = p1 -- fake shortcut, we can do better!
 lub (TcPolicy cs1) (TcPolicy cs2) =
       let sameFixedCs = [ TcClause (TcActor aid) (as ++ substAll senv bs) 
                               | TcClause (TcActor aid) as <- cs1,
@@ -246,10 +286,6 @@
 
 lub p1 p2 = TcJoin p1 p2
 
-join :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor) 
-join (RealPolicy p) (RealPolicy q) = RealPolicy $ p `lub` q
-join p q = Join p q
-                          
 
 type Subst = [(Ident (), TcActor)]
 
@@ -284,18 +320,13 @@
 -- This one could be smartified
 glb (TcPolicy as) (TcPolicy bs) = TcPolicy $ as ++ bs
 glb p1 p2 = TcMeet p1 p2
-
-meet :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor)
-meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q
-meet _ _ = panic (policyModule ++ ".meet") 
-           "meet used on non-programmable policies"
-
-{-TO FIX
-recmeet :: TcPolicyRec -> TcPolicyRec -> TcPolicyRec
-recmeet (TcPolicyRec cs1) (TcPolicyRec cs2) = TcPolicyRec $ cs1 ++ cs2
-recmeet p1                p2                = TcMeetRec p1 p2
+{-
+includesVar :: ActorPolicy -> Bool
+includesVar (VarPolicy _) = True
+includesVar (Join p q) = includesVar p || includesVar q
+includesVar (Meet p q) = includesVar p || includesVar q
+includesVar _ = False
 -}
-
 ----------------------------------------------
 {-- Specialisation
 
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
@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternGuards #-}
 module Language.Java.Paragon.TypeCheck.TcExp where
 
 import Language.Java.Paragon.Syntax
@@ -16,7 +17,7 @@
 import Data.Maybe (fromJust)
 import qualified Data.Map as Map
 import Control.Applicative ( (<$>) )
-import Control.Arrow ( first )
+import Control.Arrow ( first, second )
 import Control.Monad ( when )
 
 tcExpModule :: String
@@ -45,47 +46,43 @@
 --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str
 --debugTc _ = return ()
 
-tcExp :: Exp () -> TcCodeM (TcType, ActorPolicy, Exp T)
+tcExp :: Exp () -> TcCodeM (TcStateType, ActorPolicy, Exp T)
 
 -- Rule PAREN
 tcExp (Paren _ e) = do (ty, p, e') <- tcExp e
-                       return (ty, p, Paren (Just ty) e')
+                       return (ty, p, Paren (toT ty) e')
                        
 
 -- Rule LIT
-tcExp (Lit _ l) = let ty = litType l in return (ty, bottom, Lit (Just ty) (notAppl l))
+tcExp (Lit _ l) = let ty = stateType $ litType l in return (ty, bottom, Lit (toT ty) (notAppl l))
 
 -- Rule THIS
 tcExp (This _) = do
-  ty <- getThisType
+  tTy <- getThisStateType
   --debugPrint $ "getThisType: " ++ show ty
-  let tTy = clsTypeToType ty
-  return (tTy, bottom, This $ Just tTy)
+--  let tTy = stateType $ clsTypeToType ty
+  return (tTy, bottom, This $ toT tTy)
 
 -- Rule BINOP
 tcExp (BinOp _ e1 op e2) = do
   (ty1, p1, e1') <- tcExp e1
   (ty2, p2, e2') <- tcExp e2
   tyRes <- opType op ty1 ty2
-  return (tyRes, p1 `join` p2, BinOp (Just tyRes) e1' (notAppl op) e2')
+  return (tyRes, p1 `join` p2, BinOp (toT tyRes) e1' (notAppl op) e2')
 
 -- Rule VAR/FIELD
 tcExp (ExpName _ n) =
     case n of
       Name _ EName mPre i -> do
-             (ty1, pol, _) <- lookupVar mPre i
-             ty <- case ty1 of
-                     TcPrimT (PolicyT _) -> policyPolT <$> getPolicy n
-                     TcPrimT (ActorT _)  -> actorIdT <$> getActorId n
-                     _ -> return ty1
-             return (ty, pol, ExpName (Just ty) (notAppl n))
+             (ty, pol, _) <- lookupVar mPre i
+             return (ty, pol, ExpName (toT ty) (notAppl n))
       Name _ LName mPre i -> do
              LSig pL arL _ <- lookupLock mPre i
              check (arL == 0) $
                    "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++
                    " arguments but has been given none."
              let ty = lockT [TcLock n []]
-             return $ (ty, pL, ExpName (Just ty) (notAppl n))
+             return $ (ty, pL, ExpName (toT ty) (notAppl n))
       Name _ EOrLName mPre i -> do
              tryCatch (tcExp $ ExpName () $ Name () EName mPre i)
                 (\_ -> tcExp $ ExpName () $ Name () LName mPre i)
@@ -95,14 +92,15 @@
   
 -- Rule VARASS/FIELDASS
 tcExp ex@(Assign _ lhs _op rhs) = do
-  debugPrint $ prettyPrint ex
+  debugPrint $ "\n##   " ++ prettyPrint ex ++ "    ##\n"
   (tyV, pV, mtyO, mEnt, mN, lhs') <- 
     case lhs of
       NameLhs _ n@(Name _ EName mPre iF) ->  do
           case mPre of
             Nothing -> do -- VARASS
                 (tyV, pV, _) <- lookupVar Nothing iF
-                return (tyV, pV, Nothing, Just (varE n), Just n, NameLhs (Just tyV) (notAppl n))
+                return (unStateType tyV, pV, Nothing, Just (varE n), Just n, 
+                                    NameLhs (toT tyV) (notAppl n))
             Just pre -> do -- FIELDASS
                 (Just tyO, tmO, pO) <- lookupPrefixName pre
                 case Map.lookup iF $ fields tmO of
@@ -114,7 +112,8 @@
                           "object when updating\n" ++
                           "Object policy: " ++ prettyPrint pO ++ "\n" ++
                           "Field policy: " ++ prettyPrint pF
-                     return (tyF, pF, Just tyO, Just (varE n), Just n, NameLhs (Just tyF) (notAppl n))
+                     return (tyF, pF, Just $ unStateType tyO, Just (varE n), Just n, 
+                                NameLhs (Just tyF) (notAppl n))
                   Nothing -> fail $ "Object " ++ prettyPrint pre ++ " of type " ++
                                     prettyPrint tyO ++ " does not have a field named " ++
                                     prettyPrint iF
@@ -134,11 +133,11 @@
                  "object when updating\n" ++
                  "Object policy: " ++ prettyPrint pE ++ "\n" ++
                  "Field policy: " ++ prettyPrint pF
-            return (tyF, pF, Just tyE, eEnt, Nothing, 
+            return (tyF, pF, Just $ unStateType tyE, eEnt, Nothing, 
                        FieldLhs (Just tyF) (PrimaryFieldAccess (Just tyF) e' (notAppl fi)))
       ArrayLhs _ (ArrayIndex _ arrE iE) -> do
             (tyA, pA, arrE') <- tcExp arrE
-            case tyA of
+            case unStateType tyA of
               TcRefT (TcArrayT tyElem pElem) -> do
                 (tyI, pI, iE') <- tcExp iE
                 check (isIntConvertible tyI) $
@@ -159,7 +158,7 @@
                      "array itself when updating\n" ++
                      "Array policy: " ++ prettyPrint pA ++ "\n" ++
                      "Element policy: " ++ prettyPrint pElem
-                return (tyElem, pElem, Just tyA, Nothing, Nothing, 
+                return (tyElem, pElem, Just $ unStateType tyA, Nothing, Nothing, 
                               ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE'))
 
               _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
@@ -198,24 +197,26 @@
 --             "be less restrictive than the policy of the object\n" ++
 --             "
 
+  styV <- updateStateType mN mtyO tyV (Just tyRhs)
   -- Update actor tracker if applicable
+{-  -- TODO: This should go into updateStateType
   maybeM (mActorId tyRhs) $ \aid -> do
-         maybeM mtyO $ \tyO -> scrambleActors (Just tyO)
+         maybeM mtyO $ \tyO -> scrambleActors (Just $ unStateType tyO)
          maybeM mN $ \n -> setActorId n aid
-  
-  return (tyV, pV, Assign (Just tyV) lhs' (notAppl _op) rhs')
+-}  
+  return (styV, pV, Assign (Just tyV) lhs' (notAppl _op) rhs')
 
 -- Rule CALL
 tcExp (MethodInv _ mi) = do
   (ty, p, mi') <- tcMethodOrLockInv mi
-  return (ty, p, MethodInv (Just ty) mi')
+  return (ty, p, MethodInv (toT ty) mi')
 
 -- Rule NEW
 tcExp (InstanceCreation _ tas ct args Nothing) = do
   -- debugPrint $ "tcExp: " ++ show e
   tyT <- liftTcDeclM $ evalSrcClsType ct
-  (ty, p, args') <- tcCreate tyT tas args
-  return (ty, p, InstanceCreation (Just ty) (map notAppl tas) (notAppl ct) 
+  (sty, p, args') <- tcCreate tyT tas args
+  return (sty, p, InstanceCreation (toT sty) (map notAppl tas) (notAppl ct) 
                    args' Nothing)
 
 -- Rule COND
@@ -230,33 +231,33 @@
         (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2
     check (ty1 == ty2) $ "Types of branches don't match"
     
-    return (ty1, pC `join` p1 `join` p2, Cond (Just ty1) c' e1' e2')
+    return (ty1, pC `join` p1 `join` p2, Cond (toT ty1) c' e1' e2')
 
 tcExp (PolicyExp _ pl) = do
   pRep <- tcPolicyExp pl
-  let ty = policyPolT $ RealPolicy pRep
-  return (ty, bottom, PolicyExp (Just ty) (notAppl pl))
+  let ty = policyPolT $ KnownPolicy $ RealPolicy pRep
+  return (ty, bottom, PolicyExp (toT ty) (notAppl pl))
 
 tcExp (PostIncrement _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isNumConvertible tyE) $ 
             "Post-increment operator used at non-numeric type " ++ prettyPrint tyE
-  return (tyE, pE, PostIncrement (Just tyE) e')
+  return (tyE, pE, PostIncrement (toT tyE) e')
 tcExp (PostDecrement _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isNumConvertible tyE) $ 
             "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE
-  return (tyE, pE, PostDecrement (Just tyE) e')
+  return (tyE, pE, PostDecrement (toT tyE) e')
 tcExp (PreIncrement _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isNumConvertible tyE) $ 
             "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE
-  return (tyE, pE, PreIncrement (Just tyE) e')
+  return (tyE, pE, PreIncrement (toT tyE) e')
 tcExp (PreDecrement _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isNumConvertible tyE) $ 
             "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE
-  return (tyE, pE, PreDecrement (Just tyE) e')
+  return (tyE, pE, PreDecrement (toT tyE) e')
 
 -- Unary promotion prefix operator
 
@@ -266,27 +267,27 @@
   check (isNumConvertible tyE) $
             "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE
   let ty = unaryNumPromote_ tyE
-  return (ty, pE, PrePlus (Just ty) e')
+  return (ty, pE, PrePlus (toT ty) e')
 
 tcExp (PreMinus _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isNumConvertible tyE) $
             "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE
   let ty = unaryNumPromote_ tyE
-  return (ty, pE, PreMinus (Just ty) e')
+  return (ty, pE, PreMinus (toT ty) e')
 
 tcExp (PreBitCompl _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isIntConvertible tyE) $
         "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE
   let ty = unaryNumPromote_ tyE
-  return (ty, pE, PreBitCompl (Just ty) e')
+  return (ty, pE, PreBitCompl (toT ty) e')
 
 tcExp (PreNot _ e) = do
   (tyE, pE, e') <- tcExp e
   check (isBoolConvertible tyE) $
         "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE
-  return (booleanT, pE, PreNot (Just booleanT) e')
+  return (stateType booleanT, pE, PreNot (Just booleanT) e')
 
 
 tcExp (Cast _ t e) = do
@@ -296,11 +297,12 @@
   check canCast $ "Wrong type at cast"
   when (canExn) $ -- TODO: could throw ClassCastException
              return ()
-  return (tyC, pE, Cast (Just tyC) (notAppl t) e')
+  styC <- updateStateType Nothing Nothing tyC (Just tyE)
+  return (styC, pE, Cast (Just tyC) (notAppl t) e')
 
 tcExp (FieldAccess _ fa) = do
   (ty, p, fa') <- tcFieldAccess fa
-  return (ty, p, FieldAccess (Just ty) fa')
+  return (ty, p, FieldAccess (toT ty) fa')
 
 -- Arrays
 
@@ -330,7 +332,7 @@
       dimPs'   = map (fmap notAppl) $ snd $ unzip dimEsPs
       dimEsPs' = zip (dimE1':dimEsRest) dimPs'
       dimImplPs' = map (fmap notAppl) dimImplPs
-  return (ty, pol1, 
+  return (stateType ty, pol1, 
             ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs')
 
       where checkDimExprs :: [ActorPolicy]                    -- Accumulated policies of earlier dimensions
@@ -351,7 +353,7 @@
               pNext <- evalMaybePol mp
               checkDimExprs (pPrev:accP) (e':accE) emps pNext
 
-            nonIntErr :: TcType -> String
+            nonIntErr :: TcStateType -> String
             nonIntErr ty = 
                 "Non-integral expression of type " ++ prettyPrint ty ++
                 " used as dimension expression in array creation"
@@ -368,19 +370,19 @@
   -- Literal array initializers have known length, 
   -- so their apparent policy is bottom
   let ty = mkArrayType baseTy dimPols
-  return (ty, bottom, 
+  return (stateType ty, bottom, 
             ArrayCreateInit (Just ty) (notAppl bt) (map (fmap notAppl) dimImplPs) arrInit')
 
 tcExp (ArrayAccess _ (ArrayIndex _ arrE iE)) = do
   (tyA, pA, arrE') <- tcExp arrE
-  case tyA of
+  case unStateType tyA of
     TcRefT (TcArrayT tyElem pElem) -> do
       (tyI, pI, iE') <- tcExp iE
       check (isIntConvertible tyI) $
             "Non-integral expression of type " ++ prettyPrint tyI
             ++ " used as array index expression"
---      constraintLS pI pA $ " " -- Not true: pI just adds to the outgoing level
-      return (tyElem, pElem `join` pA `join` pI, 
+      styElem <- getStateType Nothing Nothing tyElem
+      return (styElem, pElem `join` pA `join` pI, 
                     ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE'))
 
     _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
@@ -409,7 +411,7 @@
 --  debugPrint $ "Pols: " ++ show pols
 --  debugPrint $ "Exp:  " ++ show e
   (tyE,pE,e') <- tcExp e
-  let elemType = mkArrayType baseType pols
+  let elemType = stateType $ mkArrayType baseType pols
   check (tyE == elemType) $ 
             "Expression " ++ prettyPrint e 
             ++ " in array initializer has type " ++ prettyPrint tyE
@@ -425,19 +427,12 @@
 --------------------------
 -- Field Access
 
-tcFieldAccess :: FieldAccess () -> TcCodeM (TcType, ActorPolicy, FieldAccess T)
+tcFieldAccess :: FieldAccess () -> TcCodeM (TcStateType, ActorPolicy, FieldAccess T)
 tcFieldAccess (PrimaryFieldAccess _ e fi) = do
   (tyE,pE,e') <- tcExp e
-  case tyE of
-    -- Ugly hack to get the oft-used "length" function working
-{-    TcRefT (TcArrayT tyElem pElem) ->
-      if fi == Ident () "length" 
-       then return (intT, pE)
-       else fail $ "Unsupported array field: " ++ prettyPrint fi
--}             
-    _ -> do
-      VSig tyF pFi _ _ _ <- lookupFieldT tyE fi
-      return (tyF, pE `join` pFi, PrimaryFieldAccess (Just tyF) e' (notAppl fi))
+  VSig tyF pFi _ _ _ <- lookupFieldT tyE fi
+  styF <- getStateType Nothing Nothing tyF
+  return (styF, pE `join` pFi, PrimaryFieldAccess (toT styF) e' (notAppl fi))
 
 tcFieldAccess fa = error $ "Unsupported field access: " ++ prettyPrint fa
 
@@ -445,10 +440,10 @@
 -- Instance creation
 
 tcCreate :: TcClassType -> [TypeArgument ()] -> [Argument ()] 
-         -> TcCodeM (TcType, ActorPolicy, [Argument T])
-tcCreate ctyT tas args = do
+         -> TcCodeM (TcStateType, ActorPolicy, [Argument T])
+tcCreate ctyT@(TcClassT tyN _) tas args = do
   (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
-  (tps,genCti) <- lookupConstr ctyT tas tysArgs
+  (tps,iaps,genCti) <- lookupConstr ctyT tas (map unStateType tysArgs)
   -- TODO: Check that the arguments in tyT
   --       match those expected by the type
   -- TODO: Type argument inference
@@ -457,9 +452,13 @@
         "Constructor expects " ++ show (length tps) ++ 
         " arguments but has been given " ++ show (length tas)
   tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) (zip tps tas)
+  iaas  <- mapM (instanceActorId . Name () EName (Just tyN)) iaps
+  let itps = map (ActorParam ()) iaps
+      itas = map TcActualActor iaas
+      
  -- tm <- getTypeMap
-  let cti = instantiate (zip tps tArgs) genCti
-  let (CSig psPars pW lExp lMods exns) = cti
+  let cti = instantiate (zip (tps++itps) (tArgs++itas)) genCti
+      (CSig _psIs psPars pW lExp lMods exns) = cti
 
   -- Check lockstates
   l <- getCurrentLockState
@@ -500,14 +499,16 @@
   applyLockMods lMods    -- ==> S'' = S'[lockMods ||>>= lMods, 
   scrambleActors Nothing -- ==>          actors scrambled]
 
-  return (clsTypeToType ctyT, bottom, args')
+  styT <- getStateType Nothing Nothing $ clsTypeToType ctyT
 
+  return (styT, bottom, args')
+
 --------------------------
 -- Method invocations
 
 -- | Check a method invocation, which could possibly represent
 --   a lock query expression.
-tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)
+tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcStateType, 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,20 +531,20 @@
             ++ " arguments but has been given " ++ show (length args)
 
   (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
-  debugPrint $ "args': " ++ show 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
+  -- debugPrint $ "tyR: " ++ show tyR
   return (tyR, foldl1 join (pL:psArgs),
-             MethodCallOrLockQuery (Just tyR) (notAppl nam) args')
+             MethodCallOrLockQuery (toT tyR) (notAppl nam) args')
       
 tcMethodOrLockInv mi = tcMethodInv mi
 
 -- | Check a true method invocation
-tcMethodInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)
+tcMethodInv :: MethodInvocation () -> TcCodeM (TcStateType, ActorPolicy, MethodInvocation T)
 tcMethodInv mi = do
   debugPrint $ "tcMethodInv: " ++ prettyPrint mi
   (n, msig, args, psArgs, pE, ef) <-
@@ -551,35 +552,45 @@
         MethodCallOrLockQuery _ n@(Name _ MName mPre i) args -> do
             -- This is a true method call
             (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
-            (pPath, tps, msig) <- lookupMethod mPre i [] tysArgs
+            (pPath, tps, msig) <- lookupMethod mPre i [] (map unStateType tysArgs)
+            debugPrint $ "msig: " ++ show msig
             check (null tps) $
                   "Method " ++ prettyPrint i ++ " expects " ++
                   show (length tps) ++ " type arguments but has been\
                   \ given 0"
             return $ (n, msig, args, psArgs, pPath, 
-                           \ty -> MethodCallOrLockQuery (Just ty) (notAppl n) args')
+                           \ty -> MethodCallOrLockQuery (toT ty) (notAppl n) args')
         MethodCallOrLockQuery _ n _ -> panic (tcExpModule ++ ".tcMethodInv")
                             $ "Unexpected name: " ++ show n
         PrimaryMethodCall _ e tas i args -> do
             (tyE, pE, e') <- tcExp e
             (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
             let tas' = map (ActualArg ()) tas
-            (tps, genMSig) <- lookupMethodT tyE i tas' tysArgs
+            (tps, genMSig) <- lookupMethodT tyE i tas' (map unStateType tysArgs)
             tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ 
                                      zip tps tas'
             let msig = instantiate (zip tps tArgs) genMSig
             return $ (mkSimpleName MName i, msig, args, psArgs, pE,
-                      \ty -> PrimaryMethodCall (Just ty) e' (map notAppl tas) (notAppl i) args')
+                      \ty -> PrimaryMethodCall (toT ty) e' (map notAppl tas) (notAppl i) args')
         _ -> fail $ "tcMethodInv: Unsupported method call"
 
-  let (MSig tyR pR psPars pW lExp lMods exns) = msig
+  let (MSig tyR pR psIs psPars pW lExp lMods exns) = msig
   -- Check lockstates
   l <- getCurrentLockState
   check (null (lExp \\ l)) $ 
             "Lockstate too weak when calling method " ++ prettyPrint n ++ ":\n" ++ 
             "Required lock state: " ++ prettyPrint lExp ++ "\n" ++
             "Current lock state: " ++ prettyPrint l
-       -- Check argument constraints
+  -- Check argument constraints
+  debugPrint $ "psIs:   " ++ show psIs
+  debugPrint $ "psArgs: " ++ show psArgs
+  debugPrint $ "psPars: " ++ show psPars
+  debugPrint $ "pR: " ++ show pR ++ "\n"
+  let subst = zip psIs psArgs
+      (pR':pW':psPars') = map (substParPols subst) (pR:pW:psPars)
+      exns' = map (second (substExnParPols subst)) exns
+  debugPrint $ "psPars': " ++ show psPars'
+  debugPrint $ "pR': " ++ show pR'
   mapM_ (\(arg,argP,parP) -> 
                   constraintLS argP parP $
                       "Method applied to argument with too restrictive policy:\n" ++ 
@@ -587,31 +598,55 @@
                       "Argument: " ++ prettyPrint arg ++ "\n" ++
                       "  with policy: " ++ prettyPrint argP ++ "\n" ++
                       "Declared policy bound: " ++ prettyPrint parP
-             ) (zip3 args psArgs psPars)
+             ) (zip3 args psArgs psPars')
   -- Check E[branchPC](*) <= pW
   bpcs <- getBranchPC_
-  constraintPC bpcs pW $ \p src ->
-          "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++
+  constraintPC bpcs pW' $ \p src ->
+          "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW' ++
           " not allowed in " ++ src ++
           " with write effect bound " ++ prettyPrint p          
   -- Check exnPC(S) <= pW
   epc <- getExnPC
-  constraintPC epc pW $ \p src -> 
-           "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++
+  constraintPC epc pW' $ \p src -> 
+           "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW' ++
            " not allowed in " ++ src ++
            " with write effect bound " ++ prettyPrint p
   -- Check Exns(X)[write] <= E[exns](X)[write] AND
   -- Check Exns(X)[read]  >= E[exns](X)[read]  
-  mapM_ (uncurry $ exnConsistent (Left n)) exns
+  mapM_ (uncurry $ exnConsistent (Left n)) exns'
 
   -- Fix outgoing state
-  let exns' = map (first ExnType) exns
-  activateExns exns'     -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
+  let exnsT = map (first ExnType) exns'
+  activateExns exnsT     -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
   applyLockMods lMods    -- ==> S'' = S'[lockMods ||>>= lMods, 
   scrambleActors Nothing -- ==>          actors scrambled]
 
-  return (tyR, pE `join` pR, ef tyR)
+  styR <- getStateType Nothing Nothing tyR
+  return (styR, pE `join` pR, ef styR)
 
+
+substExnParPols :: [(Ident (), ActorPolicy)] -> ExnSig -> ExnSig
+substExnParPols subst (ExnSig rX wX _ms) = 
+    ExnSig (substParPols subst rX) (substParPols subst wX) _ms
+
+substParPols :: [(Ident (), ActorPolicy)] -> ActorPolicy -> ActorPolicy
+substParPols subst (RealPolicy pol) = substParPrgPols pol
+    where substParPrgPols :: PrgPolicy TcActor -> ActorPolicy
+          substParPrgPols p@(TcRigidVar i) = 
+              case lookup i subst of
+                Just newP -> newP
+                Nothing -> RealPolicy p
+          substParPrgPols (TcJoin p q) = 
+              substParPrgPols p `join` substParPrgPols q
+          substParPrgPols (TcMeet p q) = 
+              substParPrgPols p `meet` substParPrgPols q
+          substParPrgPols p = RealPolicy p
+
+substParPols subst (Join p q) = substParPols subst p `join` substParPols subst q
+substParPols subst (Meet p q) = substParPols subst p `meet` substParPols subst q
+substParPols _ p = p
+
+
 -----------------------------------
 -- Policy expressions
 -- Treat them as pure compile-time for now
@@ -621,12 +656,12 @@
   tcCs <- mapM tcClause cs
   return (TcPolicy tcCs)
 tcPolicyExp pe@(PolicyOf _ i) = do
-  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
+  (_, _, 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
@@ -655,19 +690,25 @@
 tcActor (Actor _ n) = TcActor <$> tcActorName n
 
 tcActorName :: ActorName () -> TcCodeM ActorId
-tcActorName (ActorName    _ n) = getActorId n
+tcActorName (ActorName    _ n) = do
+  (sty,_,_) <- tcExp $ ExpName () n --getActorId (Just n) Nothing -- TODO: Look up preTy?
+  case mActorId sty of
+    Just aid -> return aid
+    Nothing  -> panic (tcExpModule ++ ".tcActorName")
+                $ "Non-actor type for actor name: " ++ show (n, sty)
+
 tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i
 
 -----------------------------------
 --    Types of operators         --
 -----------------------------------
 
-opType :: Op () -> TcType -> TcType -> TcCodeM TcType
+opType :: Op () -> TcStateType -> TcStateType -> TcCodeM TcStateType
 -- 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))
-opType (Add  _) t1 t2 | t1 == clsTypeToType stringT || t2 == clsTypeToType stringT 
-                          = return $ clsTypeToType stringT
+opType (Add  _) t1 t2 | let sT = stateType (clsTypeToType stringT),
+                        t1 == sT || t2 == sT = return sT
 
 opType op t1 t2
     -- Numeric operators
@@ -698,7 +739,7 @@
         check (isNumConvertible t2) $
               "Numerical comparison operator " ++ prettyPrint op ++ 
                 " used with non-numeric operand of type " ++ prettyPrint t2
-        return booleanT
+        return $ stateType booleanT
 
     | op `elem` [Equal (), NotEq ()] = do
         case binaryNumPromote t1 t2 of
@@ -708,7 +749,7 @@
           _ -> fail $ "Equality operator " ++ prettyPrint op ++
                        " used with incomparable operands of types " ++
                        prettyPrint t1 ++ " and " ++ prettyPrint t2
-        return booleanT
+        return $ stateType booleanT
 
     | op `elem` [And (), Or (), Xor ()] =
         if isBoolConvertible t1 
@@ -716,7 +757,7 @@
            check (isBoolConvertible t2) $ 
                      "Logical operator " ++ prettyPrint op ++
                       " used with non-boolean operand of type " ++ prettyPrint t2
-           return booleanT
+           return $ stateType booleanT
          else if isIntConvertible t1
                then do
                  check (isIntConvertible t2) $
@@ -733,7 +774,7 @@
         check (isBoolConvertible t2) $
                   "Logical operator " ++ prettyPrint op ++
                     " used with non-boolean operand of type " ++ prettyPrint t2
-        return booleanT
+        return $ stateType booleanT
 
 opType op _ _ = panic (tcExpModule ++ ".opType") $ show op
 {-
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
@@ -92,7 +92,7 @@
   (mForInit', forf) <- withInits mForInit $ do
     s <- getState
     (tyC, pC, mTest') <- case mTest of
-                           Nothing -> return (booleanT, bottom, Nothing)
+                           Nothing -> return (stateType booleanT, bottom, Nothing)
                            Just test -> do
                               (ty, p, test') <- tcExp test
                               return (ty, p, Just test')
@@ -147,11 +147,11 @@
 
 -- Rule RETURNVOID
 tcStmt (Return _ Nothing) = do
-  (tyR, pR) <- getReturn
+  (tyR, _pR) <- getReturn
   check (tyR == voidT) $ "Encountered unexpected empty return statement"
-  check (pR == top)   $ "Internal error: tcStmt: " 
-                          ++ "void return with non-top return policy should never happen"
-
+{-  check (pR == top)   $ "Internal error: tcStmt: " 
+                          ++ "void return with non-top return policy should never happen: " ++ show pR
+-}
   pc <- getCurrentPC returnE
   throwExn ExnReturn pc
   return $ Return Nothing Nothing
@@ -187,7 +187,8 @@
 
 -- Rule THROW
 tcStmt (Throw _ eX) = do
-  (tyX, pX, eX') <- tcExp eX
+  (styX, pX, eX') <- tcExp eX
+  let tyX = unStateType styX
   -- TODO: check (tyX <: "Throwable")
   (rX, wX) <- lookupExn tyX
   -- Check E[branchPC](X) <= E[exns](X)[write]
@@ -401,15 +402,18 @@
 
 -- Rule LOCALVARDECL
 tcLocalVars pV tyV fin (vd@(VarDecl _ (VarId _ i) Nothing):vds) acc cont = do
+  _styV <- registerStateType i tyV Nothing
+{-  -- TODO: Merge this into updateStateType
   tyV' <- if tyV == actorT
            then actorIdT <$> newActorId i
-           else return tyV
-  extendVarEnv i (VSig tyV' pV False False fin) $ do
+           else return $ stateType tyV -}
+  extendVarEnv i (VSig tyV pV False False fin) $ do
   addBranchPC (varE (mkSimpleName EName i)) $ do
     tcLocalVars pV tyV fin vds (notAppl vd : acc) cont    
 
 -- Rule LOCALVARINIT (Exp)
-tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitExp _ e)):vds) acc cont = do
+tcLocalVars pV tyV fin (vd0@(VarDecl _ (VarId _ i) (Just (InitExp _ e))):vds) acc cont = do
+  debugPrint $ "\n##    " ++ prettyPrint vd0 ++ "    ##\n"
   (tyE, pE, e') <- tcExp e
   checkM (tyV =<: tyE) $ 
              "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV
@@ -417,12 +421,15 @@
       "Cannot assign result of expression " ++ prettyPrint e ++
       " with policy " ++ prettyPrint pE ++
       " to variable " ++ prettyPrint i ++ " with policy " ++ prettyPrint pV               
+
+  _styV <- registerStateType i tyV (Just tyE)
+{-  -- TODO: Merge this into updateStateType
   tyV' <- case mActorId tyE of
-            Nothing -> return tyV
+            Nothing -> return $ stateType tyV
             Just aid -> do
               newActorIdWith i aid
-              return $ actorIdT aid
-  extendVarEnv i (VSig tyV' pV False False fin) $ do
+              return $ actorIdT aid -}
+  extendVarEnv i (VSig tyV pV False False fin) $ do
   addBranchPC (varE (mkSimpleName EName i)) $ do
     let vd = VarDecl Nothing (VarId Nothing $ notAppl i) (Just (InitExp Nothing e'))
     tcLocalVars pV tyV fin vds (vd:acc) cont
diff --git a/src/Language/Java/Paragon/TypeCheck/TypeMap.hs b/src/Language/Java/Paragon/TypeCheck/TypeMap.hs
--- a/src/Language/Java/Paragon/TypeCheck/TypeMap.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TypeMap.hs
@@ -49,7 +49,8 @@
 data MethodSig = MSig {
       mRetType :: TcType,
       mRetPol  :: ActorPolicy,
-      mPars    :: [ActorPolicy],
+      mPars    :: [Ident ()],
+      mParPols :: [ActorPolicy],
       mWrites  :: ActorPolicy,
       mExpects :: [TcLock],
       mLMods   :: ([TcLock],[TcLock]),
@@ -65,7 +66,8 @@
   deriving (Show, Data, Typeable)
 
 data ConstrSig = CSig {
-      cPars    :: [ActorPolicy],
+      cPars    :: [Ident ()],
+      cParPols :: [ActorPolicy],
       cWrites  :: ActorPolicy,
       cExpects :: [TcLock],
       cLMods   :: ([TcLock],[TcLock]),
@@ -108,7 +110,7 @@
       -- typemethod eval info
       typemethods :: Map (Ident ()) ([Ident ()], Block ()),
       -- types and packages
-      types       :: Map (Ident ()) ([TypeParam ()], TypeSig),
+      types       :: Map (Ident ()) ([TypeParam ()], [Ident ()], TypeSig),
       packages    :: Map (Ident ()) TypeMap
     }
   deriving (Show, Data, Typeable)
@@ -150,7 +152,7 @@
 pkgsAndTypes :: TypeMap -> Map (Ident ()) TypeMap
 pkgsAndTypes tm = Map.union (packages tm)
                     -- disregard type parameters
-                    (Map.map (tMembers . snd) $ types tm)
+                    (Map.map (tMembers . (\(_,_,x) -> x)) $ types tm)
 
 
 merge :: TypeMap -> TypeMap -> TypeMap
@@ -185,20 +187,20 @@
             newTm = go is leafTm eTm
         in tm { packages = Map.insert i newTm mTm }
 
-extendTypeMapT :: Name () -> [TypeParam ()] -> TypeSig -> TypeMap -> TypeMap
+extendTypeMapT :: Name () -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap
 extendTypeMapT = go . flattenName
   where
-    go :: [Ident ()] -> [TypeParam ()] -> TypeSig -> TypeMap -> TypeMap
-    go [] _ _ _ = panic (typeMapModule ++ ".extendTypeMapT")
-                  "Empty ident list"
-    go [i] tps tSig tm =
-        tm { types = Map.insert i (tps, tSig) (types tm) }
-    go (i:is) tps tSig tm =
+    go :: [Ident ()] -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap
+    go [] _ _ _ _ = panic (typeMapModule ++ ".extendTypeMapT")
+                    "Empty ident list"
+    go [i] tps iaps tSig tm =
+        tm { types = Map.insert i (tps,iaps,tSig) (types tm) }
+    go (i:is) tps iaps tSig tm =
         let mTm = packages tm 
             eTm = case Map.lookup i mTm of
                     Just innerTm -> innerTm
                     Nothing -> emptyTM
-            newTm = go is tps tSig eTm
+            newTm = go is tps iaps tSig eTm
         in tm { packages = Map.insert i newTm mTm }
 
 extendTypeMapN :: Name () -> (TypeMap -> TypeMap) -> TypeMap -> TypeMap
@@ -209,13 +211,13 @@
                 "Empty ident list"
     go [i] tmf tm =
         let mTm = types tm
-            (tps,tSig) = case Map.lookup i mTm of
-                           Just tyInfo -> tyInfo
-                           Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $
-                                      "Type not yet initialized: " ++ prettyPrint i
+            (tps,iaps,tSig) = case Map.lookup i mTm of
+                                Just tyInfo -> tyInfo
+                                Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $
+                                           "Type not yet initialized: " ++ prettyPrint i
             tTm = tMembers tSig
             newSig = tSig { tMembers = tmf tTm }
-        in tm { types = Map.insert i (tps, newSig) mTm }
+        in tm { types = Map.insert i (tps,iaps,newSig) mTm }
 
     go (i:is) tmf tm =
         let mTm = packages tm
@@ -230,12 +232,13 @@
 --    Working with the lookups      --
 --------------------------------------
 
+-- TODO: This is an anomaly!!!
 lookupNamed :: (TypeMap -> Map (Ident ()) a) -> Name () -> TypeMap -> Maybe a
 lookupNamed recf (Name _ _ Nothing i) tm = Map.lookup i (recf tm)
 lookupNamed recf nam@(Name _ _ (Just pre) i) tm = do
     newTm <- case nameType pre of
                TName -> do
-                 (_tps, tsig) <- lookupNamed types pre tm
+                 (_tps, _iaps, tsig) <- lookupNamed types pre tm
                  --if not (null tps)
                   --then Nothing
                   --else 
@@ -253,17 +256,49 @@
 lookupNamed _ _ _ = panic (typeMapModule ++ ".lookupNamed")
                     "AntiQName should not appear in AST being type-checked"
 
+
+lookupTypeOfStateT :: TcStateType -> TypeMap -> Either (Maybe String) TypeSig
+lookupTypeOfStateT (TcInstance (TcClassT n tas) iaas) startTm = 
+    case n of
+      Name _ TName _ _ -> 
+          let mSig = lookupNamed types n startTm
+          in case mSig of
+               Nothing -> Left Nothing
+               Just (tps, iaps, tsig) 
+                   -- TODO: Type argument inference
+                   | length tps /= length tas -> Left $ Just $ 
+                             "Wrong number of type arguments in class type.\n" ++
+                             "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++
+                             " arguments but has been given " ++ show (length tas)
+                   | length iaps /= length iaas -> panic (typeMapModule ++ ".lookupTypeOfStateT")
+                                                   $ "Too few implicit arguments: " ++ show (iaps, iaas)
+                   | otherwise -> let itps = map (ActorParam ()) iaps
+                                      itas = map TcActualActor iaas
+                                  in Right $ instantiate (zip (tps++itps) (tas++itas)) tsig
+
+      Name _ _ _ _ -> Left Nothing
+      _ -> panic (typeMapModule ++ ".lookupTypeOfT") $ show n
+
+lookupTypeOfStateT (TcType t) tm = 
+    case lookupTypeOfT t tm of
+      Right (is, tsig) | null is -> Right tsig
+                       | otherwise -> panic (typeMapModule ++ ".lookupTypeOfStateT")
+                                      $ "Needs implicit actor arguments: " ++ show (t, is)
+      Left err -> Left err
+  
+lookupTypeOfStateT _ _ = Left Nothing
+
 -- | lookupTypeOfT will, given a type T and a top-level type environment,
 --   return the type environment for T tagged with Right.
 --   Left denotes an error, which wraps:
 --   * If T is not a refType, return Nothing
 --   * If T is given the wrong number of type arguments, return Just errorMessage.
-lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) TypeSig
+lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig)
 lookupTypeOfT (TcRefT refT) = lookupTypeOfRefT refT
 lookupTypeOfT _ = const $ Left Nothing
 
-lookupTypeOfRefT :: TcRefType -> TypeMap -> Either (Maybe String) TypeSig
-lookupTypeOfRefT (TcArrayT ty pol) _ = Right $ hardCodedArrayTM ty pol
+lookupTypeOfRefT :: TcRefType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig)
+lookupTypeOfRefT (TcArrayT ty pol) _ = Right $ ([], hardCodedArrayTM ty pol)
 lookupTypeOfRefT (TcTypeVar _ ) _ = panic (typeMapModule ++ ".lookupTypeOfRefT")
                                     "TcTypeVar should have been instantiated"
 lookupTypeOfRefT TcNullT _ = Left $ Just $ "Cannot dereference null"
@@ -273,15 +308,18 @@
           let mSig = lookupNamed types n startTm
           in case mSig of
                Nothing -> Left Nothing
-               Just (tps, tsig) -> 
-                   if length tps == length tas
-                    then Right $ instantiate (zip tps tas) tsig
-                    else Left $ Just $ 
+               Just (tps, iaps, tsig) 
+                   -- TODO: Type argument inference
+                   | length tps /= length tas -> Left $ Just $ 
                              "Wrong number of type arguments in class type.\n" ++
                              "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++
                              " arguments but has been given " ++ show (length tas)
+--                   | not (null iaps) -> panic (typeMapModule ++ ".lookupTypeOfRefT")
+--                                        $ "Too many implicit arguments: " ++ show iaps
+                   | otherwise -> Right $ (iaps, instantiate (zip tps tas) tsig)
+
       Name _ _ _ _ -> Left Nothing
-      _ -> panic (typeMapModule ++ ".lookupTypeOfT") $ show n
+      _ -> panic (typeMapModule ++ ".lookupTypeOfRefT") $ show n
 
 --------------------------------------
 --   Type argument instantiation    --
diff --git a/src/Language/Java/Paragon/TypeCheck/Types.hs b/src/Language/Java/Paragon/TypeCheck/Types.hs
--- a/src/Language/Java/Paragon/TypeCheck/Types.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Types.hs
@@ -22,13 +22,24 @@
 typesModule = typeCheckerBase ++ ".Types"
 
 type T = Maybe TcType -- Used for annotated AST
+
 notAppl :: Functor f => f a -> f T
 notAppl = fmap (const Nothing)
 
+toT :: TcStateType -> T
+toT = Just . unStateType
 
+data TcStateType
+    = TcInstance TcClassType [ActorId]
+    | TcActorIdT ActorId
+    | TcPolicyPolT ActorPolicyBounds
+    | TcLockT [TcLock]
+    | TcType TcType
+  deriving (Eq, Ord, Show, Data, Typeable)
+
 data TcType
-    = TcPrimT (PrimType ()) | TcRefT TcRefType | TcVoidT
-    | TcActorIdT ActorId | TcPolicyPolT ActorPolicy | TcLockT [TcLock]
+    = TcPrimT (PrimType ()) | TcRefT TcRefType | TcVoidT -- | TcLockRetT
+--    | TcActorIdT ActorId | TcPolicyPolT ActorPolicy | TcLockT [TcLock]
   deriving (Eq, Ord, Show, Data, Typeable)
 
 data TcRefType
@@ -39,7 +50,7 @@
   deriving (Eq, Ord, Show, Data, Typeable)
 
 data TcClassType
-    = TcClassT (Name ()) [TcTypeArg] -- | TcNullT -- Ignore wildcards for now
+    = TcClassT (Name ()) [TcTypeArg] -- [ActorId] -- Ignore wildcards for now
   deriving (Eq, Ord, Show, Data, Typeable)
 
 data TcTypeArg
@@ -49,8 +60,6 @@
     | TcActualLockState [TcLock]
   deriving (Eq, Ord, Show, Data, Typeable)
 
--- type TcTypeArg = TcTypeArgRaw ActorId TcPolicy TcLock
-
 ------------------------------------
 -- Constructors
 
@@ -67,19 +76,33 @@
 actorT   = TcPrimT (ActorT   ())
 policyT  = TcPrimT (PolicyT  ())
 
+stateType :: TcType -> TcStateType
+stateType = TcType
+
+unStateType :: TcStateType -> TcType
+unStateType tcst = case tcst of
+                     TcInstance ct _ -> TcRefT $ TcClsRefT ct
+                     TcActorIdT    _ -> actorT
+                     TcPolicyPolT  _ -> policyT
+                     TcLockT       _ -> booleanT
+                     TcType        t -> t
+
 nullT, voidT :: TcType
 nullT    = TcRefT TcNullT
 voidT    = TcVoidT
 
-actorIdT :: ActorId -> TcType
+actorIdT :: ActorId -> TcStateType
 actorIdT = TcActorIdT
 
-policyPolT :: ActorPolicy -> TcType
+policyPolT :: ActorPolicyBounds -> TcStateType
 policyPolT = TcPolicyPolT
 
-lockT :: [TcLock] -> TcType
+lockT :: [TcLock] -> TcStateType
 lockT = TcLockT
 
+instanceT :: TcClassType -> [ActorId] -> TcStateType
+instanceT = TcInstance
+
 {-
 clsTypeWArg :: Name () -> [TcTypeArg] -> TcType
 clsTypeWArg n = TcClassT n
@@ -132,11 +155,13 @@
 --                  Just n -> n
 --                  Nothing -> error $ "typeName_: " ++ show typ
 
-isClassType, isRefType, isNullType :: TcType -> Bool
-isClassType (TcRefT (TcClsRefT (TcClassT _ _))) = True
+isClassType, isRefType, isNullType :: TcStateType -> Bool
+isClassType (TcType (TcRefT (TcClsRefT (TcClassT{})))) = True
+isClassType (TcInstance{}) = True
 isClassType _ = False
 
-isRefType (TcRefT _) = True
+isRefType (TcType (TcRefT _)) = True
+isRefType (TcInstance{}) = True
 isRefType _ = False
 
 mNameRefType :: TcRefType -> Maybe (Name ())
@@ -144,28 +169,28 @@
     if null as then Just (mkUniformName_ AmbName $ flattenName n) else Nothing
 mNameRefType _ = Nothing
 
-isNullType (TcRefT TcNullT) = True
+isNullType (TcType (TcRefT TcNullT)) = True
 isNullType _ = False
 
-mActorId :: TcType -> Maybe ActorId
+mActorId :: TcStateType -> Maybe ActorId
 mActorId (TcActorIdT aid) = Just aid
 mActorId _ = Nothing
 
-mLocks :: TcType -> Maybe [TcLock]
+mLocks :: TcStateType -> Maybe [TcLock]
 mLocks (TcLockT ls) = Just ls
 mLocks _ = Nothing
 
-mPolicyPol :: TcType -> Maybe ActorPolicy
+mPolicyPol :: TcStateType -> Maybe ActorPolicyBounds
 mPolicyPol (TcPolicyPolT p) = Just p
 mPolicyPol _ = Nothing
 
-isLockType :: TcType -> Bool
+isLockType :: TcStateType -> Bool
 isLockType = isJust . mLocks
 
-isActorType :: TcType -> Bool
+isActorType :: TcStateType -> Bool
 isActorType = isJust . mActorId
 
-isPolicyType :: TcType -> Bool
+isPolicyType :: TcStateType -> Bool
 isPolicyType = isJust . mPolicyPol
 
 mArrayType :: TcType -> Maybe (TcType, [ActorPolicy])
@@ -175,6 +200,14 @@
       Just (t, ps) -> (t, p:ps)
 mArrayType _ = Nothing
 
+mClassType :: TcType -> Maybe TcClassType
+mClassType (TcRefT (TcClsRefT (ct@TcClassT{}))) = Just ct
+mClassType _ = Nothing
+
+mInstanceType :: TcStateType -> Maybe (TcClassType, [ActorId])
+mInstanceType (TcInstance ct aids) = Just (ct, aids)
+mInstanceType _ = Nothing
+
 -------------------------------------------
 -- Type operations
 
@@ -204,48 +237,17 @@
 
 
 box :: PrimType () -> Maybe (TcClassType)
-box pt = case pt of
-   BooleanT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Boolean"])
-            []
-   ByteT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Byte"])
-            []
-   ShortT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Short"])
-            []
-   CharT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Character"])
-            []
-   IntT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Integer"])
-            []
-   LongT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Long"])
-            []
-   FloatT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Float"])
-            []
-   DoubleT () -> 
-       Just $
-            TcClassT 
-            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Double"])
-            []
-   _ -> Nothing
+box pt = let mkClassType str = Just $ TcClassT (mkName_ TName PName $ map (Ident ()) ["java", "lang", str]) []
+         in case pt of
+              BooleanT () -> mkClassType "Boolean"
+              ByteT    () -> mkClassType "Byte"
+              ShortT   () -> mkClassType "Short"
+              CharT    () -> mkClassType "Character"
+              IntT     () -> mkClassType "Integer"
+              LongT    () -> mkClassType "Long"
+              FloatT   () -> mkClassType "Float"
+              DoubleT  () -> mkClassType "Double"
+              _ -> Nothing
 
 unbox :: TcClassType -> Maybe (PrimType ())
 unbox (TcClassT n _) =
@@ -262,40 +264,39 @@
 --unbox TcNullT = Nothing
 
 
-unboxType :: TcType -> Maybe (PrimType ())
-unboxType (TcRefT (TcClsRefT ct)) = unbox ct
+unboxType :: TcStateType -> Maybe (PrimType ())
+unboxType sty | TcRefT (TcClsRefT ct) <- unStateType sty = unbox ct
 unboxType _ = Nothing
 
 
 unIdent :: Ident a -> String
 unIdent (Ident _ x) = x
-unIdent _ = panic (typesModule ++ ".unIdent")
-            "AntiQIdent should not appear in AST being typechecked"
+unIdent (AntiQIdent _ str) = panic (typesModule ++ ".unIdent")
+                             $ "AntiQIdent should not appear in AST being typechecked: " ++ str
 
-isNumConvertible :: TcType -> Bool
-isNumConvertible ty = 
-    ty `elem` [byteT, shortT, intT, longT, charT, floatT, doubleT] ||
-    case unboxType ty of
+isNumConvertible :: TcStateType -> Bool
+isNumConvertible sty = 
+    unStateType sty `elem` [byteT, shortT, intT, longT, charT, floatT, doubleT] ||
+    case unboxType sty of
       Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT]) -> True
       _ -> False
 
-isIntConvertible :: TcType -> Bool
-isIntConvertible ty =
-    ty `elem` [byteT, shortT, intT, longT, charT] ||
-    case unboxType ty of
+isIntConvertible :: TcStateType -> Bool
+isIntConvertible sty =
+    unStateType sty `elem` [byteT, shortT, intT, longT, charT] ||
+    case unboxType sty of
       Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT]) -> True
       _ -> False
 
-isBoolConvertible :: TcType -> Bool
-isBoolConvertible t = t == booleanT 
+isBoolConvertible :: TcStateType -> Bool
+isBoolConvertible t = unStateType t == booleanT -- includes lock types
                       || unboxType t == Just (BooleanT ())
-                      || isLockType t
 
 
-unaryNumPromote :: TcType -> Maybe (PrimType ())
-unaryNumPromote ty
-    | TcPrimT pt <- ty            = numPromote pt
-    | Just    pt <- unboxType ty  = numPromote pt
+unaryNumPromote :: TcStateType -> Maybe (PrimType ())
+unaryNumPromote sty
+    | TcPrimT pt <- unStateType sty  = numPromote pt
+    | Just    pt <- unboxType   sty  = numPromote pt
     | otherwise = Nothing
 
     where numPromote :: PrimType () -> Maybe (PrimType ())
@@ -304,32 +305,39 @@
               | pt `elem` map ($()) [ByteT, ShortT, IntT, CharT] = Just $ IntT ()
               | otherwise = Nothing
 
-unaryNumPromote_ :: TcType -> TcType
-unaryNumPromote_ = TcPrimT . fromJust . unaryNumPromote
+unaryNumPromote_ :: TcStateType -> TcStateType
+unaryNumPromote_ = stateType . TcPrimT . fromJust . unaryNumPromote
 
-binaryNumPromote :: TcType -> TcType -> Maybe (PrimType ())
+binaryNumPromote :: TcStateType -> TcStateType -> Maybe (PrimType ())
 binaryNumPromote t1 t2 = do
     pt1 <- unaryNumPromote t1
     pt2 <- unaryNumPromote t2
     return $ max pt1 pt2
       
-binaryNumPromote_ :: TcType -> TcType -> TcType
-binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2
+binaryNumPromote_ :: TcStateType -> TcStateType -> TcStateType
+binaryNumPromote_ t1 t2 = stateType . TcPrimT . fromJust $ binaryNumPromote t1 t2
 
 
 
 ---------------------------------------------
 -- Pretty printing
 
+instance Pretty TcStateType where
+  pretty tcst =
+      case tcst of
+        TcActorIdT aid -> text "actor[" <> pretty aid <> text "]"
+        TcPolicyPolT p -> text "policy[" <> pretty p <> text "]"
+        TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]"
+        TcInstance ct aids -> pretty ct <> 
+                              (hsep $ char '[' : punctuate (char ',') (map pretty aids)) <> char ']'
+        TcType ty -> pretty ty
+
 instance Pretty TcType where
   pretty tct =
       case tct of
         TcPrimT pt -> pretty pt
         TcRefT rt -> pretty rt
         TcVoidT -> text "void"
-        TcActorIdT aid -> text "actor[" <> pretty aid <> text "]"
-        TcPolicyPolT p -> text "policy[" <> pretty p <> text "]"
-        TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]"
 
 instance Pretty TcRefType where
   pretty tcrt =