diff --git a/paragon.cabal b/paragon.cabal
--- a/paragon.cabal
+++ b/paragon.cabal
@@ -1,5 +1,5 @@
 Name:                   paragon
-Version:                0.1.24
+Version:                0.1.25
 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.24"
+versionString = "0.1.25"
 
 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
@@ -47,8 +47,8 @@
 
 type Resolve ast = ast () -> NameRes (ast ())
 
-rnTypeDecl :: Resolve TypeDecl
-rnTypeDecl (ClassTypeDecl _ (ClassDecl _ ms ci tps mSuper impls cb)) = do
+mkTpsExpn :: [TypeParam ()] -> Expansion
+mkTpsExpn tps =
     let acts = [ aI | ActorParam _ aI <- tps ]
         pols = [ pI | PolicyParam _ pI <- tps ]
         lsts = [ lI | LockStateParam _ lI <- tps ]
@@ -59,8 +59,11 @@
                   concatMap mkEExpansion pols ++
                   concatMap mkLExpansion lsts ++
                   concatMap mkTExpansion typs
+    in expns
 
-    extendExpansion expns $
+rnTypeDecl :: Resolve TypeDecl
+rnTypeDecl (ClassTypeDecl _ (ClassDecl _ ms ci tps mSuper impls cb)) = do
+    extendExpansion (mkTpsExpn tps) $
       ClassTypeDecl () <$> 
           (ClassDecl ()
               <$> mapM rnModifier ms
@@ -70,18 +73,7 @@
               <*> mapM rnClassType impls
               <*> rnClassBody cb)
 rnTypeDecl (InterfaceTypeDecl _ (InterfaceDecl _ ms ii tps supers ib)) = do
-    let acts = [ aI | ActorParam _ aI <- tps ]
-        pols = [ pI | PolicyParam _ pI <- tps ]
-        lsts = [ lI | LockStateParam _ lI <- tps ]
-        typs = [ tI | TypeParam _ tI _ <- tps ]
-    
-        expns = Map.fromList $
-                  concatMap mkEExpansion acts ++
-                  concatMap mkEExpansion pols ++
-                  concatMap mkLExpansion lsts ++
-                  concatMap mkTExpansion typs
-
-    extendExpansion expns $
+    extendExpansion (mkTpsExpn tps) $
       InterfaceTypeDecl () <$>
           (InterfaceDecl ()
               <$> mapM rnModifier ms
@@ -471,6 +463,13 @@
 rnPolicyExp pe = 
     case pe of
       PolicyLit _ cs -> PolicyLit () <$> mapM rnClause cs
+      PolicyOf _ i -> do
+              -- just see if it exists
+              _ <- rnName (Name () EName Nothing i)
+              return pe
+      PolicyTypeVar _ i -> do
+              _ <- rnName (Name () EName Nothing i)
+              return pe
       _ -> return pe
 
 -- Types
@@ -687,11 +686,12 @@
 
 buildMapFromTd :: TypeDecl () -> Expansion -> PiReader (Expansion, Expansion)
 buildMapFromTd td expn = do --return . Map.fromList $
-    (i, supers) <- case td of
-                     ClassTypeDecl     _ (ClassDecl     _ _ i _ mSuper _ _) -> return (i, maybe [] (:[]) mSuper)
-                     InterfaceTypeDecl _ (InterfaceDecl _ _ i _ supers _  ) -> return (i, supers)
-                     _ -> fail $ "Enums not yet supported"
-    rnSups <- runNameRes (mapM rnClassType supers) expn
+    (i, tps, supers) <- 
+        case td of
+          ClassTypeDecl     _ (ClassDecl     _ _ i tps mSuper _ _) -> return (i, tps, maybe [] (:[]) mSuper)
+          InterfaceTypeDecl _ (InterfaceDecl _ _ i tps supers _  ) -> return (i, tps, supers)
+          _ -> fail $ "Enums not yet supported"
+    rnSups <- runNameRes (mapM rnClassType supers) (Map.union expn (mkTpsExpn tps))
     superExpns <- mapM buildMapFromSuper rnSups
     let iExpn = Map.fromList $ mkTExpansion i
     return $ (iExpn, unionExpnMaps superExpns)
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
@@ -1193,7 +1193,9 @@
 arrPols :: P (Maybe (Policy ()))
 arrPols = do
   _ <- arrBrackets
-  opt $ ExpName () <$> angles (nameRaw eName)
+  opt $ angles argExp1
+--  ExpName () <$> angles (nameRaw eName)
+--      <|> PolicyExp () <$> policyExp
 
 nonArrayType :: P (Type ())
 nonArrayType = PrimType () <$> primType <|> 
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
@@ -77,7 +77,7 @@
 typeCheckCd (ClassDecl _ ms i tps mSuper _impls (ClassBody _ decls)) = do
   --debug "typeCheckCd"
   withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do
-  staticWPol <- getWritePolicy ms
+  staticWPol <- RealPolicy <$> getWritePolicy ms
   
   let memberDecls = [ mdecl | MemberDecl _ mdecl  <- decls ]
       inits       = [ idecl | idecl@(InitDecl {}) <- decls ]
@@ -175,7 +175,8 @@
                   spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
                     a <- freshActorId (prettyPrint i)
                     p <- getReadPolicy ms
-                    let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
+                    let vti = VSig actorT (RealPolicy p) False 
+                              (Static () `elem` ms) (Final () `elem` ms)
                     withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
                                                     fields = Map.insert i vti (fields tm) }) $
                       tcra
@@ -197,7 +198,8 @@
                   -- Final, with explicit initializer
                   evalActorVd (ms, VarDecl _ (VarId _ i) (Just (InitExp _ e))) tcra = do
                     p <- getReadPolicy ms
-                    let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
+                    let vti = VSig actorT (RealPolicy p) False 
+                              (Static () `elem` ms) (Final () `elem` ms)
                     a <- case e of
                            ExpName _ n -> do
                              tm <- getTypeMap
@@ -226,7 +228,7 @@
   lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
     pol <- getLockPolicy ms
     prs <- evalSrcLockProps i mProps
-    return $ LSig pol (length mps) prs
+    return $ LSig (RealPolicy pol) (length mps) prs
   withCurrentTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
     tcba
 
@@ -271,7 +273,7 @@
               mRetPol  = bottom,
               mWrites  = top,
               mPars    = pis,
-              mParPols = [ bottom | _ <- ps ],
+              mParBounds = [ bottom | _ <- ps ],
               mExpects = [],
               mLMods   = noMods,
               mExns    = []
@@ -398,7 +400,7 @@
     -- 3. Add signature to typemap
     return $ VSig {
                  varType = ty,
-                 varPol  = rPol,
+                 varPol  = RealPolicy rPol,
                  varParam  = False,
                  varStatic = Static () `elem` ms,
                  varFinal  = Final  () `elem` ms
@@ -438,10 +440,10 @@
     wPol <- getWritePolicy ms
     let mti = MSig {
                 mRetType = ty,
-                mRetPol  = rPol,
-                mWrites  = wPol,
+                mRetPol  = RealPolicy rPol,
+                mWrites  = RealPolicy wPol,
                 mPars    = pIs,
-                mParPols = pPols,
+                mParBounds = map RealPolicy pPols,
                 mExpects = es,
                 mLMods   = lms,
                 mExns    = xSigs
@@ -474,9 +476,9 @@
     -- 5. Add signature to typemap
     wPol <- getWritePolicy ms
     let cti = CSig {
-              cWrites  = wPol,
+              cWrites  = RealPolicy wPol,
               cPars    = pIs,
-              cParPols = pPols,
+              cParBounds = map RealPolicy pPols,
               cExpects = es,
               cLMods   = lms,
               cExns    = xSigs
@@ -502,9 +504,9 @@
 
 typeCheckSignature _ _ tcba = tcba
 
-withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM a -> TcDeclM a
+withParam :: (FormalParam (), TcType, PrgPolicy TcActor) -> TcDeclM a -> TcDeclM a
 withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do
-    let vsig = VSig ty p True (Static () `elem` ms) (Final () `elem` ms)
+    let vsig = VSig ty (RealPolicy p) True (Static () `elem` ms) (Final () `elem` ms)
     withCurrentTypeMap $ \tm -> 
         tm { fields = Map.insert i vsig (fields tm) }
 
@@ -528,8 +530,8 @@
     wPol <- getWritePolicy ms
     lms  <- checkLMMods ms
     let xSig = ExnSig {
-               exnReads = rPol,
-               exnWrites = wPol,
+               exnReads = RealPolicy rPol,
+               exnWrites = RealPolicy wPol,
                exnMods = lms
              }
     return (ty, xSig)
@@ -555,7 +557,7 @@
   let es = concat [ l | Expects _ l <- ms ]
   mapM evalLock es
 
-typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)
+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), PrgPolicy TcActor)
 typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do
   withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do
     -- 1. Check parameter type
@@ -563,7 +565,7 @@
     -- 2. Typecheck and evaluate policy modifier
     checkPolicyMods st ms 
        "typeCheckSignature: At most one read modifier allowed per parameter"
-    rPol <- getParamPolicy i ms
+    rPol <- getParamPolicy ms
     return (if ell then arrayType ty bottom else ty, i, rPol)
 typeCheckParam _ (FormalParam _ _ _ _ arvid) =
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
@@ -615,7 +617,9 @@
 ------------------------------------------------------------------------------
 -- Bodies
 
-typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM [MemberDecl T]
+typeCheckMemberDecls :: ActorPolicy 
+                     -> ActorPolicy 
+                     -> [MemberDecl ()] -> TcDeclM [MemberDecl T]
 typeCheckMemberDecls sLim cLim ms = do
   st <- setupStartState
   mapM (typeCheckMemberDecl sLim cLim st) ms
@@ -683,15 +687,18 @@
   let isVarArity = case reverse ps of
                      [] -> False
                      (FormalParam _ _ _ b _ : _) -> b
-  Just (MSig tyRet pRet _pIs 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
 
   -- Setup the environment in which to check the body
-  let parVsigs = [ (iP, VSig t p True False (isFinal ms)) |
-                    (FormalParam _ ms _ _ (VarId _ iP), t, p) <- zip3 ps tysPs pPars ]
+  let parMods  = [ (iP, ms) | (FormalParam _ ms _ _ (VarId _ iP)) <- ps ]
+      parVsigs = [ (iP, VSig t (ofPol iP) True False (isFinal ms)) |
+                    ((iP, ms), t) <- zip parMods tysPs ]
+      pBs  = zip pIs pPars
       pars = map fst parVsigs
-      exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
+      exnPols = map (second $ 
+                     \es -> (exnReads es, exnWrites es)) xSigs
       exnLMods = map (second exnMods) xSigs
       parEnts = [ (VarEntity $ mkSimpleName EName iP, []) | iP <- pars ]
       exnEnts = [ (ExnEntity t, []) | t <- map fst xSigs ]
@@ -702,7 +709,8 @@
               lockstate = expLs,
               returnI = Just (tyRet, pRet),
               exnsE = Map.fromList exnPols,
-              branchPCE = (branchMap, [(pWri, writeErr)])
+              branchPCE = (branchMap, [(pWri, writeErr)]),
+              parBounds = pBs
             }
 
   -- debug $ "Using env: " ++ show env
@@ -743,10 +751,12 @@
 
   -- Setup the environment in which to check the body
   tm <- getTypeMap
-  let parVsigs = [ (i, VSig t p True False (isFinal ms)) |
-                    (FormalParam _ ms _ _ (VarId _ i), t, p) <- zip3 ps tysPs pPars ]
+  let parVsigs = [ (i, VSig t (ofPol i) True False (isFinal ms)) |
+                    (FormalParam _ ms _ _ (VarId _ i), t) <- zip ps tysPs ]
       pars = map fst parVsigs
-      exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
+      pBs  = zip pars pPars
+      exnPols = map (second $ 
+                     \es -> (exnReads es, exnWrites es)) xSigs
       exnLMods = map (second exnMods) xSigs
       parEnts = [ VarEntity $ mkSimpleName EName i | i <- pars ]
       exnEnts = [ ExnEntity t | t <- map fst xSigs ]
@@ -761,7 +771,8 @@
               lockstate = expLs,
               returnI = error "Cannot return from constructor",
               exnsE = Map.fromList exnPols,
-              branchPCE = (branchMap, [(pWri, writeErr)])
+              branchPCE = (branchMap, [(pWri, writeErr)]),
+              parBounds = pBs
             }
 
   --debug $ "Using branch map: " ++ show (branchPCE env)
@@ -791,8 +802,10 @@
 unknownIfActor (i, ty)
     | ty == actorT = unknownActorId >>= \aid -> return [(i, aid)]
     | otherwise = return []
-                
 
+ofPol :: Ident () -> ActorPolicy
+ofPol = RealPolicy . TcRigidVar
+
 checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM ()
 checkExnMods st (xTy, lms) = do
   let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st)
@@ -800,7 +813,12 @@
     check (lms `models` lockMods sX) $
               "Declared exception lock modifiers not general enough: "
               ++ show lms
-
+{-
+getParamBound :: ActorPolicy -> PrgPolicy TcActor
+getParamBound (RealPolicy (TcRigidVar _)) = top
+getParamBound (RealPolicy p) = p
+getParamBound _ = top
+-}
 
 tcMethodBody :: TypeCheck (TcCodeM) MethodBody
 tcMethodBody (MethodBody _ mBlock) = 
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
@@ -3,27 +3,29 @@
 
 import qualified Data.Map as Map
 
+--import Language.Java.Paragon.Syntax (Ident) -- get rid of!
+
 import Language.Java.Paragon.TypeCheck.Policy
 --import Language.Java.Paragon.TypeCheck.Containment
 import Language.Java.Paragon.TypeCheck.Locks
 --import Language.Java.Paragon.TypeCheck.Monad.TcCont
 import Language.Java.Paragon.Interaction
-import Data.IORef
-import Data.List (partition, union)
-import Language.Java.Paragon.Monad.Base (orM)
---import Control.Monad (filterM)
+import Data.List (union)
+import Language.Java.Paragon.Syntax (Ident)
 
 constraintsModule :: String
 constraintsModule = typeCheckerBase ++ ".Constraints"
 
-data Constraint = LRT [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)
+data Constraint = 
+    LRT [(Ident (), ActorPolicy)] 
+            [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)
   deriving (Show, Eq)
 
 type ConstraintWMsg = (Constraint, String)
 
 
 splitCstrs :: Constraint -> [Constraint]
-splitCstrs (LRT g ls p q) = map (\x -> LRT g ls x q) (disjoin p)
+splitCstrs (LRT bs g ls p q) = map (\x -> LRT bs 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!!
@@ -33,28 +35,23 @@
 
 
 --Check if a given constraint p<=q verifies that q is an unknown policy of a variable
-isCstrVar :: Constraint -> IO Bool
-isCstrVar (LRT _ _ _ (RealPolicy _))    = return False
-isCstrVar (LRT _ _ _ (VarPolicy (TcMetaVar _ ref))) = do
-  mpol <- readIORef ref
-  case mpol of
-    Nothing -> return True 
-    Just _  -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""
-isCstrVar (LRT _ _ _ _) 
+isCstrVar :: Constraint -> Bool
+isCstrVar (LRT _ _ _ _ (RealPolicy _))    = False
+isCstrVar (LRT _ _ _ _ (VarPolicy (TcMetaVar _ _))) = True
+isCstrVar (LRT _ _ _ _ _) 
     = panic (constraintsModule ++ ".isCstrVar") 
       "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
-noVarLeft (LRT _ _ (RealPolicy _) _)    = return True
-noVarLeft (LRT _ _ (VarPolicy (TcMetaVar _ ref)) _) = do
-  mpol <- readIORef ref
-  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 (Meet p q) r) = noVarLeft (LRT g ls p r) `orM` noVarLeft (LRT g ls q r)
+noVarLeft :: Constraint -> Bool
+noVarLeft (LRT _ _ _ (RealPolicy _) _)    = True
+noVarLeft (LRT _ _ _ (VarPolicy (TcMetaVar _ _)) _) = False
+noVarLeft (LRT bs g ls (Join p q) r) = 
+    noVarLeft (LRT bs g ls p r) || noVarLeft (LRT bs g ls q r)
+noVarLeft (LRT bs g ls (Meet p q) r) = 
+    noVarLeft (LRT bs g ls p r) || noVarLeft (LRT bs g ls q r)
 
+{-
 partitionM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint], [Constraint])
 partitionM f xs = do
   xs' <- mapM (\x -> do 
@@ -63,6 +60,7 @@
          xs
   xs'' <- return $ partition fst xs'
   return $ ((map snd $ fst xs''), (map snd $ snd xs''))
+-}
 
 {-
 filterM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint])
@@ -76,9 +74,9 @@
 -}
 
 linker :: (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))]) -> Constraint -> (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))])
-linker m (LRT _ ls p (VarPolicy x)) = case (Map.lookup x m) of
-                                        Nothing -> Map.insert x [(ls, p)] m
-                                        Just ps -> Map.insert x ((ls, p):ps) m
+linker m (LRT _ _ ls p (VarPolicy x)) = case (Map.lookup x m) of
+                                          Nothing -> Map.insert x [(ls, p)] m
+                                          Just ps -> Map.insert x ((ls, p):ps) m
 linker _ _                          = panic "linker shouldn't be called on a non-variable constraint" ""
 
 
@@ -94,8 +92,8 @@
 -- Add to a set of constraints the ones obtained by substituting a policy to a MetaVariable
 substitution :: (TcMetaVar TcActor) -> ([TcLock], (TcPolicy TcActor)) -> [Constraint] -> [Constraint]
 substitution _ _ [] = []
-substitution x (ls, px) ((c@(LRT g ls' p q)):cs) = 
+substitution x (ls, px) ((c@(LRT bs g ls' p q)):cs) = 
     let (ls'', psubst) = substPol x (ls, px) (ls',p) in
     case ((psubst == p) && (ls'' == ls')) of
       True  -> c:(substitution x (ls, px) cs)
-      False -> (LRT g ls'' psubst q):c:(substitution x (ls, px) cs)
+      False -> (LRT bs g ls'' psubst q):c:(substitution x (ls, px) cs)
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
@@ -20,56 +20,73 @@
 containmentModule :: String
 containmentModule = typeCheckerBase ++ ".Containment"
 
-lrt :: [TcClause TcAtom] -> 
-       [TcLock] -> 
-       TcPolicy TcActor -> 
-       TcPolicy TcActor -> 
+lrt :: [(Ident (), ActorPolicy)] ->         -- upper bounds of rigid vars
+       [TcClause TcAtom] ->                       -- global recursive properties
+       [TcLock] ->                                -- current lock state
+       TcPolicy TcActor ->                        -- p
+       TcPolicy TcActor ->                        -- q
        Either Bool Constraint
-lrt g ls p q =
+lrt bs g ls p q =
     case (p, q) of
-      (_, 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 _ _) -> Right (LRT bs g ls p q)
+      (Meet _ _, _) -> Right (LRT bs g ls p q)
+      (RealPolicy rp, RealPolicy rq) -> lrtReal bs g ls rp rq
       (Join p1 p2, _) -> let
-                    ap1 = lrt g ls p1 q
-                    ap2 = lrt g ls p2 q
+                    ap1 = lrt bs g ls p1 q
+                    ap2 = lrt bs g ls p2 q
                     in case (ap1, ap2) of
                          _ | Left False `elem` [ap1, ap2] -> Left False
                          (Left True, _) -> ap2
                          (_, Left True) -> ap1 
-                         _ -> Right (LRT g ls p q)
+                         _ -> Right (LRT bs g ls p q)
       (_, Meet q1 q2) -> let
-                    ap1 = lrt g ls p q1
-                    ap2 = lrt g ls p q2
+                    ap1 = lrt bs g ls p q1
+                    ap2 = lrt bs 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)
+                         _ -> Right (LRT bs g ls p q)
+      (VarPolicy _, _) -> Right (LRT bs g ls p q)
+      (_, VarPolicy _) -> Right (LRT bs g ls p q)
 
 
-lrtReal :: [TcClause TcAtom] 
+lrtReal :: [(Ident (), ActorPolicy)]
+        -> [TcClause TcAtom] 
         -> [TcLock]
         -> PrgPolicy TcActor 
         -> PrgPolicy TcActor 
-        -> Bool
+        -> Either Bool Constraint
 --lrtReal _ _ p q | any includesThis [p,q] =
 --                    panic (containmentModule ++ ".lrtReal")
 --                              $ "THIS in containment check: " ++ show (p,q)
-lrtReal g ls (TcPolicy p) (TcPolicy q) =  lrtC g ls p q
-lrtReal g ls (TcJoin p1 p2) q = lrtReal g ls p1 q && lrtReal g ls p2 q
-lrtReal g ls p (TcMeet q1 q2) = lrtReal g ls p q1 && lrtReal g ls p q2
-lrtReal g ls p q
+lrtReal _bs g ls (TcPolicy p) (TcPolicy q) =  Left $ lrtC g ls p q
+lrtReal bs g ls (TcJoin p1 p2) q = 
+    lrt bs g ls (Join (RealPolicy p1) (RealPolicy p2)) (RealPolicy q)
+lrtReal bs g ls p (TcMeet q1 q2) =
+     lrt bs g ls (RealPolicy p) (Meet (RealPolicy q1) (RealPolicy q2))
+lrtReal bs g ls p q
         | Just i <- firstRigid (TcJoin p q) = 
                     let subi pol x = substPolicy [(i, x)] pol
-                        [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, top]) [p,q]
-                    in lrtReal g ls pb qb && lrtReal g ls pt qt
+                        bound = maybe top id $ lookup i bs
+                        [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, bound]) [p,q]
+                        ap1 = lrt bs g ls pb qb
+                        ap2 = lrt bs g ls pt qt
+                    in case (ap1, ap2) of
+                         _ | Left False `elem` [ap1, ap2] -> Left False
+                         (Left True, _) -> ap2
+                         (_, Left True) -> ap1 
+                         _ -> Right (LRT bs g ls (RealPolicy p) (RealPolicy q))
         | any includesThis [p,q] =
                     let [[pb,pt],[qb,qt]] = map (\y -> map (flip substThis y) [bottom, top]) [p,q]
-                    in lrtReal g ls pb qb && lrtReal g ls pt qt
-lrtReal _ _ p q = 
+                        ap1 = lrt bs g ls pb qb
+                        ap2 = lrt bs g ls pt qt
+                    in case (ap1, ap2) of
+                         _ | Left False `elem` [ap1, ap2] -> Left False
+                         (Left True, _) -> ap2
+                         (_, Left True) -> ap1 
+                         _ -> Right (LRT bs g ls (RealPolicy p) (RealPolicy q))
+lrtReal _ _ _ p q = 
     panic (containmentModule ++ ".lrtReal") 
     $ "Error: Non-computed policy provided to lrt: " ++ show (p, q)
 
diff --git a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
--- a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs
@@ -55,7 +55,7 @@
   let def = foldl join bottom ppols
   return $ mpol `orUse` def
 -}
-evaluate :: Policy () -> TcDeclM (TcPolicy TcActor)
+evaluate :: Policy () -> TcDeclM (PrgPolicy TcActor)
 evaluate = evalPolicy
 {-evaluate (PolicyExp _ pe) = evalPolicyExp pe
 evaluate (ExpName _ n) = -- getPolicy n
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
@@ -96,8 +96,8 @@
 import Control.Applicative ( (<$>), (<*>) )
 --import Control.Arrow ( first, second )
 import qualified Data.Map as Map
-import Data.IORef
-import Data.List (union, intersperse)
+--import Data.IORef
+import Data.List (union, intersperse, partition)
 
 --debug :: String -> TcDeclM ()
 --debug str = liftIO $ finePrint $ "DEBUG: " ++ str
@@ -176,7 +176,7 @@
     debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ show sty
     tm <- getTypeMap
     case lookupTypeOfStateT sty tm of
-      Right newSig -> return (Just sty, tMembers newSig, p)
+      Right newSig -> return (Just sty, instThis p $ tMembers newSig, p)
       Left (Just err) -> fail err
       _ -> panic (monadModule ++ ".lookupPrefixName")
            $ "Unknown variable or field: " ++ show n
@@ -193,7 +193,7 @@
                    debugPrint $ "lookupPrefixName: EName: " ++ prettyPrint n ++ 
                                   " :: " ++ prettyPrint ty
                    -- debugPrint $ show (packages baseTm2) ++ "\n"
-                   sty <- getStateType (Just n) mPreSty ty 
+                   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
@@ -387,14 +387,14 @@
   case Map.lookup i $ locks preTm of
     Just lsig -> return lsig
     Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope"
-
-getPolicy :: Name () -> TcCodeM ActorPolicy
+{-
+getPolicy :: Name () -> TcCodeM (PrgPolicy TcActor)
 getPolicy n = do
   tm <- getTypeMap
   case lookupNamed policies n tm of
     Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n
     Just p -> return p
-
+-}
 
 lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig
 lookupFieldT typ i = do
@@ -486,6 +486,9 @@
     Just ps -> return ps
     Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX
 
+registerExn_ :: TcType -> PrgPolicy TcActor -> PrgPolicy TcActor -> TcCodeM a -> TcCodeM a
+registerExn_ tyX rX wX = registerExn tyX (RealPolicy rX) (RealPolicy wX)
+
 registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM a -> TcCodeM a
 registerExn tyX rX wX = registerExns [(tyX, (rX,wX))]
 
@@ -643,7 +646,8 @@
   case mSty of
     Just sty | Just pbs <- mPolicyPol sty -> do
 -}
-updateStateType _mN _mTyO _ty (Just sty) = return sty
+updateStateType _mN _mTyO ty _mSty | isPrimType (stateType ty) = return $ stateType ty
+updateStateType _mN _mTyO _ty (Just sty) = return sty -- BOGUS!!!
 updateStateType _mN _mTyO ty Nothing     = return $ stateType ty
 
 
@@ -657,7 +661,7 @@
       (iaps, _) <- lookupTypeOfType (clsTypeToType ct)
       mapM (instanceActorId . Name () EName (Just tyN)) iaps
     Just aids -> return aids
-  
+
 -- Policy Analysis
 
 getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds
@@ -668,7 +672,7 @@
                  (Just styO, Just (Name _ _ _ i)) -> do
                            tsig <- lookupTypeOfStateType styO
                            case Map.lookup i $ policies $ tMembers tsig of
-                             Just pol -> return $ KnownPolicy pol
+                             Just pol -> return $ KnownPolicy $ RealPolicy pol
                              Nothing  -> return $ PolicyBounds bottom top
                  _ -> return $ PolicyBounds bottom top
     Just pif -> return pif
@@ -726,10 +730,10 @@
 
 -- Exception tracking
 
-getExnPC :: TcCodeM [(ActorPolicy, String)]
+getExnPC :: TcCodeM [(TcPolicy TcActor, String)]
 getExnPC = exnPC <$> getState
 
-throwExn :: ExnType -> ActorPolicy -> TcCodeM ()
+throwExn :: ExnType -> TcPolicy TcActor -> TcCodeM ()
 throwExn et pX = do
   uref <- getUniqRef
   state <- getState
@@ -746,15 +750,15 @@
         in s { exnS = newEmap }
   
 
-activateExns :: [(ExnType, ExnSig)] -> TcCodeM ()
+activateExns :: [(ExnType, (ActorPolicy, LockMods))] -> TcCodeM ()
 activateExns exns = do
   uref <- getUniqRef
   state <- getState
   let (ts, sigs) = unzip exns
-  xPoints <- mapM (\sigX -> do
+  xPoints <- mapM (\(wX, modsX) -> do
                      s <- liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO
-                           state { lockMods = lockMods state ||>> exnMods sigX }
-                     return (s, exnWrites sigX)) sigs
+                           state { lockMods = lockMods state ||>> modsX }
+                     return (s, wX)) sigs
   let oldXmap = exnS state
       newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints)
   mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap
@@ -791,11 +795,10 @@
 
 -- Policy inference
 
-newMetaPolVar :: TcCodeM ActorPolicy
-newMetaPolVar = do
+newMetaPolVar :: Ident () -> TcCodeM ActorPolicy
+newMetaPolVar i = do
   uniq <- liftIO . getUniq =<< getUniqRef
-  ref  <- liftIO (newIORef Nothing)
-  return $ VarPolicy (TcMetaVar uniq ref)
+  return $ VarPolicy (TcMetaVar uniq i)
 
 --newRigidPolVar :: TcCodeM TcPolicy
 --newRigidPolVar = do
@@ -809,7 +812,8 @@
 constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM ()
 constraint ls p q str = do -- addConstraint $ LRT ls p1 p2
   g <- getGlobalLockProps
-  case lrt g ls p q of
+  bs <- getParamPolicyBounds
+  case lrt bs g ls p q of
     Left b -> do
 --      debugTc $ "constraint: p1: " ++ show p1
 --      debugTc $ "constraint: p2: " ++ show p2
@@ -817,6 +821,9 @@
       check b (str {-++ "\n\nState: " ++ show st -})
     Right c -> addConstraint c str
 
+getParamPolicyBounds :: TcCodeM [(Ident (), ActorPolicy)]
+getParamPolicyBounds = parBounds <$> getEnv
+
 getGlobalLockProps :: TcCodeM [TcClause TcAtom]
 getGlobalLockProps = do
   cs <- go <$> getTypeMap
@@ -844,8 +851,9 @@
   
 
 
-exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM ()
-exnConsistent caller exnTy (ExnSig rX wX _) = do
+exnConsistent :: Either (Name ()) TcClassType
+              -> TcType -> (ActorPolicy, ActorPolicy) -> TcCodeM ()
+exnConsistent caller exnTy (rX,wX) = do
     exnMap <- exnsE <$> getEnv
     --debugTc $ "Using exnMap: " ++ show exnMap
     let (callerName, callerSort) = 
@@ -975,28 +983,36 @@
 ------------------------------------------
 
 -- Resolution thanks to the transitive closure.
-solve :: MonadIO m => [ConstraintWMsg] -> m ()
-solve cs = 
-    liftIO $ do
-      let wcs = [c | (c, _) <- cs]                                 --Extract constraints
-          wcs' = concat $ map splitCstrs wcs                       --Split them : (Join p q <= r)<=>((p<=r)/\(q<=r))
-      cvars <- filterM isCstrVar wcs'                               --Get the "p<=X" constraints, X MetaVar
-      let cvarsm = foldl linker Map.empty cvars                    --Map to X the list of p s.t. p<=X
+solve :: [ConstraintWMsg] -> TcDeclM ()
+solve cs = do
+      let wcs     = [c | (c, _) <- cs]                                 --Extract constraints
+          wcs'    = concat $ map splitCstrs wcs                       --Split them : (Join p q <= r)<=>((p<=r)/\(q<=r))
+      --print "wcs"
+      --mapM_ print wcs
+      --print "wcs'"
+      --mapM_ print wcs'
+          cvars   = filter isCstrVar wcs'                               --Get the "p<=X" constraints, X MetaVar
+      --print "cvars"
+      --mapM_ print cvars
+          cvarsm  = foldl linker Map.empty cvars                    --Map to X the list of p s.t. p<=X
           csubsts = Map.foldrWithKey                               --Realize the substitutions
                              (\x pxs cs' -> foldr 
                               (\px cs'' -> substitution x px cs'') 
                               cs' pxs) 
                              wcs' cvarsm
-      (_toInfer, ccstright) <- partitionM isCstrVar csubsts
-      toBeChecked <- filterM noVarLeft ccstright
-      mapM_ (checkCstr ("The system failed to infer the set of unspecified policies " ++ (Map.foldrWithKey (\x _ s -> (show x) ++ " , " ++ s) "" cvarsm))) toBeChecked
+          (_toInfer, ccstright) = partition isCstrVar csubsts
+          toBeChecked = filter noVarLeft ccstright
+      mapM_ (checkCstr ("The system failed to infer the set of unspecified policies ")) toBeChecked
 
-checkCstr :: String -> Constraint -> IO ()
-checkCstr str (LRT g ls p q) = do
-  case lrt g ls p q of
+
+
+checkCstr :: String -> Constraint -> TcDeclM ()
+checkCstr str (LRT bs g ls p q) = do
+  case lrt bs g ls p q of
     Left b  -> do
       check b str
-    Right _ -> panic "This set of constraint should be solved !" ""
+    Right _ -> panic (monadModule ++ ".checkCstr")
+               $ "This set of constraint should be solved !"
 
 
 {-
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs b/src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs
@@ -22,22 +22,24 @@
 data CodeEnv = CodeEnv  {
       vars      :: Map (Ident ()) VarFieldSig,
       lockstate :: [TcLock],
-      returnI   :: Maybe (TcType, (TcPolicy TcActor)),
-      exnsE     :: Map TcType ((TcPolicy TcActor), (TcPolicy TcActor)),
-      branchPCE :: (Map Entity [((TcPolicy TcActor), String)], [((TcPolicy TcActor), String)])
+      returnI   :: Maybe (TcType, ActorPolicy),
+      exnsE     :: Map TcType (ActorPolicy, ActorPolicy),
+      branchPCE :: (Map Entity [(ActorPolicy, String)], [(ActorPolicy, String)]),
+      parBounds :: [(Ident (), ActorPolicy)]
     }
   deriving (Show, Data, Typeable)
 
 -- Env to use when typechecking expressions not inside method
 -- bodies, e.g. in field initializers and policy modifiers
-simpleEnv :: (TcPolicy TcActor) -> String -> CodeEnv
+simpleEnv :: ActorPolicy -> String -> CodeEnv
 simpleEnv brPol str = 
     CodeEnv {
       vars = Map.empty,
       lockstate = [],
       returnI = Nothing,
       exnsE = Map.empty,
-      branchPCE = (Map.empty, [(brPol,str)])
+      branchPCE = (Map.empty, [(brPol,str)]),
+      parBounds = []
     }
 
 data Entity = VarEntity (Name ())
@@ -66,11 +68,11 @@
 --    Working with the branchPC     --
 --------------------------------------
 
-branchPC :: Maybe Entity -> CodeEnv -> [((TcPolicy TcActor), String)]
+branchPC :: Maybe Entity -> CodeEnv -> [(ActorPolicy, String)]
 branchPC men (CodeEnv { branchPCE = (bm, def) }) = 
     flip (maybe def) men $ \en ->
         maybe def id (Map.lookup en bm)
 
-joinBranchPC :: (TcPolicy TcActor) -> String -> CodeEnv -> CodeEnv
+joinBranchPC :: ActorPolicy -> String -> CodeEnv -> CodeEnv
 joinBranchPC p str env = let (bm, def) = branchPCE env
                          in env { branchPCE = (Map.map ((p, str):) bm, (p,str):def) }
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
@@ -183,7 +183,7 @@
 type ExnsMap  = Map.Map ExnType ExnPoint
 data ExnType  = ExnType TcType | ExnContinue | ExnBreak | ExnReturn
   deriving (Eq, Ord, Show)
-data ExnPoint = ExnPoint { epState :: CodeState, epWrite :: (TcPolicy TcActor) }
+data ExnPoint = ExnPoint { epState :: CodeState, epWrite :: TcPolicy TcActor }
   deriving (Eq, Show)
 
 
@@ -207,7 +207,7 @@
                     "Both ExnPoint arguments cannot be missing!"
 
 -- This should probably be pre-computed each time the map is updated instead
-exnPC :: CodeState -> [((TcPolicy TcActor), String)]
+exnPC :: CodeState -> [(ActorPolicy, String)]
 exnPC s = map (\(tyX,ptX) -> (epWrite ptX, errorSrc tyX)) $ Map.assocs $ exnS s
 
 errorSrc :: ExnType -> String
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
@@ -27,10 +27,12 @@
 import Language.Java.Paragon.TypeCheck.Constraints (ConstraintWMsg, Constraint)
 import Language.Java.Paragon.TypeCheck.Actors
 import Language.Java.Paragon.TypeCheck.Locks (noMods)
+import Language.Java.Paragon.TypeCheck.Policy
 import Language.Java.Paragon.TypeCheck.TypeMap
 
 import Control.Monad 
 import Control.Applicative
+import Control.Arrow (second)
 
 import qualified Data.Map as Map
 
@@ -88,8 +90,9 @@
 gatherPolicyBounds = gatherPolicyBounds' Nothing
 
     where gatherPolicyBounds' mPre tm =
-              let pols = Map.assocs $ policies tm -- :: [(Ident, ActorPolicy)]
-                  aMap = Map.fromList $ map (mkPols mPre $ fields tm) pols
+              let pols = Map.assocs $ policies tm -- :: [(Ident, PrgPolicy)]
+                  aMap = Map.fromList $ map (mkPols mPre $ fields tm) 
+                         $ map (second RealPolicy) pols
                   tMap = gatherPolicyBoundsAux TName mPre
                            (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm)
                   pMap = gatherPolicyBoundsAux PName mPre (Map.assocs $ packages tm)
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
@@ -107,33 +107,35 @@
                check (typName == cuName) $
                      "File name " ++ prettyPrint typName ++
                      " does not match class name " ++ prettyPrint cuName
-               superTys <- --map (TcRefT . TcClsRefT) <$>
+               withFoldMap withTypeParam tps $ do
+                 superTys <- --map (TcRefT . TcClsRefT) <$>
                               mapM evalSrcClsType (maybe [] (:[]) mSuper)
-               implsTys  <- --map (TcRefT . TcClsRefT) <$>
+                 implsTys  <- --map (TcRefT . TcClsRefT) <$>
                               mapM evalSrcClsType impls
                
-               -- Remove this line, and set tMembers to emptyTM,
-               -- if using "clever lookup" instead of "clever setup"
-               superTm <- case superTys of
-                            [] -> return emptyTM
-                            [superTy] -> tMembers . snd <$> lookupTypeOfType (clsTypeToType superTy)
-                            _ -> panic (tcDeclMModule ++ ".fetchType")
+                 -- Remove this line, and set tMembers to emptyTM,
+                 -- if using "clever lookup" instead of "clever setup"
+                 superTm <- case superTys of
+                              [] -> return emptyTM
+                              [superTy] -> tMembers . snd <$> 
+                                           lookupTypeOfType (clsTypeToType superTy)
+                              _ -> panic (tcDeclMModule ++ ".fetchType")
                                  $ "More than one super class for class:"  ++ show superTys
 
-               let tsig = TSig {
-                            tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],
-                            tIsClass = True,
-                            tIsFinal = Final () `elem` ms,
-                            tSupers  = superTys,
-                            tImpls   = implsTys,
-                            tMembers = superTm { constrs = Map.empty }
-                          }
-                   mDs = map unMemberDecl ds
-                   iaps = findImplActorParams mDs
-               extendGlobalTypeMap (extendTypeMapT n tps iaps tsig)
+                 let tsig = TSig {
+                              tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],
+                              tIsClass = True,
+                              tIsFinal = Final () `elem` ms,
+                              tSupers  = superTys,
+                              tImpls   = implsTys,
+                              tMembers = superTm { constrs = Map.empty }
+                            }
+                     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
+--               withFoldMap withTypeParam tps $ do
                  fetchActors n mDs $ do
                  fetchLocks  n mDs $ do
                  fetchPols   n mDs $ do
@@ -245,7 +247,7 @@
                   -- Static, only Nothing for initializer
                spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do
                  a <- freshActorId (prettyPrint i)
-                 p <- getReadPolicy ms
+                 p <- RealPolicy <$> getReadPolicy ms
                  let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
                  return ((i,a),(i,vti))
                spawnActorVd (_, VarDecl _ arvid _) =
@@ -253,7 +255,7 @@
 
                paramActorVd (ms, VarDecl _ (VarId _ i) _) = do
                  let a = ActorTPVar i
-                 p <- getReadPolicy ms
+                 p <- RealPolicy <$> getReadPolicy ms
                  let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
                  return ((i,a),(i,vti))
                paramActorVd (_, VarDecl _ arvid _) =
@@ -271,7 +273,7 @@
  -}
                -- Final, with explicit initializer
                evalActorVd (ms, VarDecl _ (VarId _ i) (Just (InitExp _ e))) = do
-                 p <- getReadPolicy ms
+                 p <- RealPolicy <$> getReadPolicy ms
                  let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
                  a <- case e of
                         ExpName _ nam -> do
@@ -299,7 +301,7 @@
                      pol <- getLockPolicy ms
                      modPrs <- getLockModProps i ms
                      prs <- evalSrcLockProps i mProps
-                     return (i, LSig pol (length mps) (modPrs ++ prs))
+                     return (i, LSig (RealPolicy pol) (length mps) (modPrs ++ prs))
   let newTM = emptyTM { locks = Map.fromList lsigs }
   extendGlobalTypeMap (extendTypeMapN n $ merge newTM)
   withCurrentTypeMap (merge newTM) $ do
@@ -342,7 +344,7 @@
 --                    debugPrint $ "Policies fetched"
                     tdra
 
-      where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)
+      where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), PrgPolicy TcActor)
             fetchPol (i,e,_) = (i,) <$> evalPolicy e
 -- end policies
 
@@ -403,7 +405,7 @@
                    FieldDecl _ ms ty vds -> do                      
                       tcty <- evalSrcType ty
                       pol  <- getReadPolicy ms
-                      let vti = VSig tcty pol 
+                      let vti = VSig tcty (RealPolicy pol)
                                   False (Static () `elem` ms) (Final () `elem` ms)
                       ids <- mapM unVarDecl vds
                       let newFm = foldl (\m i -> Map.insert i vti m) fm ids
@@ -430,14 +432,14 @@
                              closes  <- mapM evalLock $ concat [ l | Closes  _ l <- ms ]
                              opens   <- mapM evalLock $ concat [ l | Opens   _ l <- ms ]
                              let mti = MSig {
-                                         mRetType = tcty,
-                                         mRetPol  = rPol,
-                                         mPars    = pIs,
-                                         mParPols = pPols,
-                                         mWrites  = wPol,
-                                         mExpects = expects,
-                                         mLMods   = (closes, opens),
-                                         mExns    = exs
+                                         mRetType   = tcty,
+                                         mRetPol    = RealPolicy rPol,
+                                         mPars      = pIs,
+                                         mParBounds = map RealPolicy pPols,
+                                         mWrites    = RealPolicy wPol,
+                                         mExpects   = expects,
+                                         mLMods     = (closes, opens),
+                                         mExns      = exs
                                        }
                                  isVarArity = case reverse ps of
                                                 [] -> False
@@ -464,12 +466,12 @@
                              closes  <- mapM evalLock $ concat [ l | Closes  _ l <- ms ]
                              opens   <- mapM evalLock $ concat [ l | Opens   _ l <- ms ]
                              let cti = CSig {
-                                         cPars    = pIs,
-                                         cParPols = pPols,
-                                         cWrites  = wPol,
-                                         cExpects = expects,
-                                         cLMods   = (closes, opens),
-                                         cExns    = exs
+                                         cPars      = pIs,
+                                         cParBounds = map RealPolicy pPols,
+                                         cWrites    = RealPolicy wPol,
+                                         cExpects   = expects,
+                                         cLMods     = (closes, opens),
+                                         cExns      = exs
                                        }
                                  isVarArity = case reverse ps of
                                                 [] -> False
@@ -488,15 +490,15 @@
           opens  <- mapM evalLock $ concat [ l | Opens  _ l <- ms ]
           closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ]
           let esig = ExnSig {
-                       exnReads = rPol,
-                       exnWrites = wPol,
+                       exnReads = RealPolicy rPol,
+                       exnWrites = RealPolicy wPol,
                        exnMods = (closes, opens)
                      }
           return (ty, esig)
 
-   paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)
+   paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), PrgPolicy TcActor)
    paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do
-          pPol <- getParamPolicy i ms
+          pPol <- getParamPolicy ms
           pTy  <- evalSrcType ty
           return (pTy, i, pPol)
    paramInfo (FormalParam _ _ _ _ arvid) = 
@@ -513,7 +515,7 @@
       PolicyParam _ i -> do
            let vti = VSig policyT top False False True
            withCurrentTypeMap (\tm ->
-              tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),
+              tm { policies = Map.insert i (TcRigidVar i) (policies tm),
                    fields = Map.insert i vti (fields tm) }) $ tcba
       LockStateParam _ i -> do
           let lti = LSig top 0 []
@@ -620,7 +622,7 @@
 ------------------------------------------------------------
 
 -------------------------------------------------------------------------------------      
-getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM ActorPolicy
+getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM (PrgPolicy TcActor)
 getReadPolicy mods = 
     case [pol |Reads _ pol <- mods ] of -- !!0 -- Read Policy? what if no read policy?
       [pol] -> evalPolicy pol
@@ -639,23 +641,20 @@
       [] -> return top
       _ -> fail "At most one read modifier allowed per lock"
 
-getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM ActorPolicy
-getParamPolicy i mods =
+getParamPolicy :: [Modifier ()] -> TcDeclM (PrgPolicy TcActor)
+getParamPolicy mods =
     case [pol | Reads _ pol <- mods ] of
        [pol] -> evalPolicy pol
-       [] -> return $ ofPol i
+       [] -> return top
        _ -> fail "At most one read modifier allowed per parameter"
 
-getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM ActorPolicy
+getReturnPolicy :: [Modifier ()] -> [PrgPolicy TcActor] -> TcDeclM (PrgPolicy TcActor)
 getReturnPolicy mods pPols = 
     case [pol | Reads _ pol <- mods ] of
       [pol] -> evalPolicy pol
       [] -> return $ foldl join bottom pPols
       _ -> fail "At most one return modifier allowed per method"
 
-ofPol :: Ident () -> ActorPolicy
-ofPol = RealPolicy . TcRigidVar
-
 -------------------------------------------------------------------
 -- Evaluating types
 
@@ -731,10 +730,13 @@
 -- Actors may only be names -- TODO: must be final
 evalSrcNWTypeArg (ActorParam {}) (ActualName _ n) = TcActualActor <$> evalActorId n
 -- Policies may be names, or special expressions -- TODO: names must be final
-evalSrcNWTypeArg (PolicyParam {}) (ActualName _ n) = TcActualPolicy <$> evalPolicy (ExpName () n)
-evalSrcNWTypeArg (PolicyParam {}) (ActualExp  _ e) = TcActualPolicy <$> evalPolicy e
+evalSrcNWTypeArg (PolicyParam {}) (ActualName _ n) = 
+    TcActualPolicy . RealPolicy <$> evalPolicy (ExpName () n)
+evalSrcNWTypeArg (PolicyParam {}) (ActualExp  _ e) = 
+    TcActualPolicy . RealPolicy <$> evalPolicy e
 -- Lock states must be locks
-evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls
+evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = 
+    TcActualLockState <$> mapM evalLock ls
 
 evalSrcNWTypeArg tp nwta = 
     fail $ "Trying to instantiate type parameter " ++ prettyPrint tp ++
@@ -747,7 +749,7 @@
 evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls
 -}
 
-evalPolicy :: Exp () -> TcDeclM ActorPolicy
+evalPolicy :: Exp () -> TcDeclM (PrgPolicy TcActor)
 evalPolicy e = case e of
   ExpName _ n -> do
     -- debug $ "evalPolicy: " ++ show n
@@ -770,11 +772,11 @@
   Paren _ p -> evalPolicy p
   _ -> fail "evalPolicy: More here!"
 
-evalPolicyExp :: PolicyExp () -> TcDeclM ActorPolicy
-evalPolicyExp (PolicyLit _ cs) = (RealPolicy . TcPolicy) <$> mapM evalClause cs
-evalPolicyExp (PolicyOf _ i)   = return $ RealPolicy $ TcRigidVar i
-evalPolicyExp (PolicyThis _)   = return $ RealPolicy $ TcThis
-evalPolicyExp (PolicyTypeVar _ i) = return $ RealPolicy $ TcRigidVar i
+evalPolicyExp :: PolicyExp () -> TcDeclM (PrgPolicy TcActor)
+evalPolicyExp (PolicyLit _ cs) = TcPolicy <$> mapM evalClause cs
+evalPolicyExp (PolicyOf _ i)   = return $ TcRigidVar i
+evalPolicyExp (PolicyThis _)   = return $ TcThis
+evalPolicyExp (PolicyTypeVar _ i) = return $ TcRigidVar i
 
 evalClause :: Clause () -> TcDeclM (TcClause TcActor)
 evalClause (Clause _ h b) = do
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
@@ -20,7 +20,6 @@
 import Language.Java.Paragon.TypeCheck.Actors
 import Language.Java.Paragon.TypeCheck.Locks
 
-import Data.IORef
 import Data.List ( (\\) {-, groupBy, nub-}  )
 import Data.Maybe 
 
@@ -65,7 +64,7 @@
 
 type AtomPolicy = TcPolicy TcAtom
 
-data TcMetaVar a = TcMetaVar Int (IORef (Maybe (TcPolicy a)))
+data TcMetaVar a = TcMetaVar Int (Ident ())
 --  deriving (Data, Typeable)
 
 instance Data (TcMetaVar a) where
@@ -422,18 +421,18 @@
 -- Policy substitution
 
 -- Invariant: policies are always closed by the env
-substPolicy :: [(Ident (), PrgPolicy TcActor)] -> PrgPolicy TcActor -> PrgPolicy TcActor
+substPolicy :: [(Ident (), ActorPolicy)] -> PrgPolicy TcActor -> ActorPolicy
 substPolicy env (TcRigidVar i) 
     | Just q <- lookup i env = q
 substPolicy env (TcJoin p1 p2) =
     let pol1 = substPolicy env p1
         pol2 = substPolicy env p2
-    in pol1 `lub` pol2
+    in pol1 `join` pol2
 substPolicy env (TcMeet p1 p2) =
     let pol1 = substPolicy env p1
         pol2 = substPolicy env p2
-    in pol1 `glb` pol2
-substPolicy _ p = p
+    in pol1 `meet` pol2
+substPolicy _ p = RealPolicy p
 
 firstRigid :: PrgPolicy a -> Maybe (Ident ())
 firstRigid (TcRigidVar i) = Just i
@@ -441,17 +440,17 @@
 firstRigid (TcMeet p q) = listToMaybe $ catMaybes $ map firstRigid [p,q]
 firstRigid _ = Nothing
 
-substThis :: PrgPolicy TcActor -> PrgPolicy TcActor -> PrgPolicy TcActor
+substThis :: ActorPolicy -> PrgPolicy TcActor -> ActorPolicy
 substThis p TcThis = p
 substThis p (TcJoin p1 p2) =
     let pol1 = substThis p p1
         pol2 = substThis p p2
-    in pol1 `lub` pol2
+    in pol1 `join` pol2
 substThis p (TcMeet p1 p2) =
     let pol1 = substThis p p1
         pol2 = substThis p p2
-    in pol1 `glb` pol2
-substThis _ p = p
+    in pol1 `meet` pol2
+substThis _ p = RealPolicy p
 
 {-
 mkPolicySubst :: [TcPolicy] -> [TcPolicy] -> [(Ident (), TcPolicy)]
diff --git a/src/Language/Java/Paragon/TypeCheck/TcExp.hs b/src/Language/Java/Paragon/TypeCheck/TcExp.hs
--- a/src/Language/Java/Paragon/TypeCheck/TcExp.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TcExp.hs
@@ -17,7 +17,7 @@
 import Data.Maybe (fromJust)
 import qualified Data.Map as Map
 import Control.Applicative ( (<$>) )
-import Control.Arrow ( first, second )
+-- import Control.Arrow ( first, second )
 import Control.Monad ( when )
 
 tcExpModule :: String
@@ -153,14 +153,14 @@
                              "  has policy " ++ prettyPrint pA ++ "\n" ++
                              "Index: " ++ prettyPrint iE ++ "\n" ++
                              "  has policy " ++ prettyPrint pI
-                constraint [] pA pElem $
+                constraint [] pA (RealPolicy pElem) $
                      "Cannot update element in array resulting from expression " ++ 
                      prettyPrint arrE ++ 
                      ": policy of elements must be no less restrictive than that of the " ++
                      "array itself when updating\n" ++
                      "Array policy: " ++ prettyPrint pA ++ "\n" ++
                      "Element policy: " ++ prettyPrint pElem
-                return (tyElem, pElem, Just $ unStateType tyA, Nothing, Nothing, 
+                return (tyElem, RealPolicy pElem, Just $ unStateType tyA, Nothing, Nothing, 
                               ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE'))
 
               _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
@@ -324,7 +324,8 @@
 
   -- Check that the remaining dimexprs each conform to
   -- the policy given at the level outside it
-  (polEDims, dimEsRest) <- checkDimExprs [] [] dimEsPsRest =<< evalMaybePol mDimP1
+  (polEDims, dimEsRest) <- checkDimExprs [] [] dimEsPsRest 
+                             =<< evalMaybePol mDimP1
 
   -- Evaluate given policies for implicit dimensions
   polIDims <- mapM evalMaybePol dimImplPs
@@ -337,17 +338,17 @@
   return (stateType ty, pol1, 
             ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs')
 
-      where checkDimExprs :: [ActorPolicy]                    -- Accumulated policies of earlier dimensions
+      where checkDimExprs :: [PrgPolicy TcActor]              -- Accumulated policies of earlier dimensions
                           -> [Exp T]                          -- Accumulated annotated expressions
                           -> [(Exp (), Maybe (Policy ()))]    -- Remaining dimexprs/pols
-                          -> ActorPolicy                      -- Policy of previous dimension
-                          -> TcCodeM ([ActorPolicy], [Exp T])
+                          -> PrgPolicy TcActor                -- Policy of previous dimension
+                          -> TcCodeM ([PrgPolicy TcActor], [Exp T])
             checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE)
             checkDimExprs accP accE ((e,mp):emps) pPrev = do
               (tyE,pE,e') <- tcExp e
               check (isIntConvertible tyE) $ nonIntErr tyE
               -- Each dimexpr must satisfy the policy of the outer dim
-              constraintLS pE pPrev $
+              constraintLS pE (RealPolicy pPrev) $
                            "Array dimension expression has too restrictive policy:\n" ++
                            "Expression: " ++ prettyPrint e ++ "\n" ++
                            "  with policy: " ++ prettyPrint pE ++ "\n" ++
@@ -384,7 +385,7 @@
             "Non-integral expression of type " ++ prettyPrint tyI
             ++ " used as array index expression"
       styElem <- getStateType Nothing Nothing tyElem
-      return (styElem, pElem `join` pA `join` pI, 
+      return (styElem, RealPolicy pElem `join` pA `join` pI, 
                     ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE'))
 
     _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
@@ -396,10 +397,10 @@
 --------------------------
 -- Array initializers
 
-tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck TcCodeM ArrayInit
+tcArrayInit :: TcType -> [PrgPolicy TcActor] -> TypeCheck TcCodeM ArrayInit
 tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do
   (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits
-  mapM_ (\(p,e) -> constraintLS p pol1 $
+  mapM_ (\(p,e) -> constraintLS p (RealPolicy pol1) $
                     "Expression in array initializer has too restrictive policy:\n" ++
                     "Expression: " ++ prettyPrint e ++
                     "  with policy: " ++ prettyPrint p ++
@@ -408,7 +409,7 @@
   return $ ArrayInit Nothing inits'
 tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions"
 
-tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T)
+tcVarInit :: TcType -> [PrgPolicy TcActor] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T)
 tcVarInit baseType pols (InitExp _ e) = do
 --  debugPrint $ "Pols: " ++ show pols
 --  debugPrint $ "Exp:  " ++ show e
@@ -423,7 +424,7 @@
   arr' <- tcArrayInit baseType pols arr
   return (bottom, InitArray Nothing arr')
 
-evalMaybePol :: Maybe (Policy ()) -> TcCodeM ActorPolicy
+evalMaybePol :: Maybe (Policy ()) -> TcCodeM (PrgPolicy TcActor)
 evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy)
 
 --------------------------
@@ -432,7 +433,7 @@
 tcFieldAccess :: FieldAccess () -> TcCodeM (TcStateType, ActorPolicy, FieldAccess T)
 tcFieldAccess (PrimaryFieldAccess _ e fi) = do
   (tyE,pE,e') <- tcExp e
-  VSig tyF pFi _ _ _ <- lookupFieldT tyE fi
+  VSig tyF pFi _ _ _ <- instThis pE <$> lookupFieldT tyE fi
   styF <- getStateType Nothing Nothing tyF
   return (styF, pE `join` pFi, PrimaryFieldAccess (toT styF) e' (notAppl fi))
 
@@ -460,7 +461,7 @@
       
  -- tm <- getTypeMap
   let cti = instantiate (zip (tps++itps) (tArgs++itas)) genCti
-      (CSig _psIs psPars pW lExp lMods exns) = cti
+      (CSig psIs psPars pW lExp lMods exns) = cti
 
   -- Check lockstates
   l <- getCurrentLockState
@@ -469,6 +470,14 @@
             "Required lock state: " ++ prettyPrint lExp ++ "\n" ++
             "Current lock state: " ++ prettyPrint l
   -- Check argument constraints
+  let subst = zip psIs psArgs
+      (pW':psPars') = map (substParPols subst) (pW:psPars)
+      (exnPs, exnAcs) = 
+          unzip [ ((t, (rX', wX')),  (ExnType t, (wX', modsX))) |
+                  (t, ExnSig rX wX modsX) <- exns,
+                  let rX' = substParPols subst rX, 
+                  let wX' = substParPols subst wX 
+                ]
   mapM_ (\(arg,argP,parP) -> 
              constraintLS argP parP $
                  "Constructor applied to argument with too restrictive policy:\n" ++ 
@@ -476,28 +485,27 @@
                  "Argument: " ++ prettyPrint arg ++
                  "  with policy: " ++ prettyPrint argP ++
                  "Declared policy bound: " ++ prettyPrint parP
-        ) (zip3 args psArgs psPars)
+        ) (zip3 args psArgs psPars')
   -- Check E[branchPC](*) <= pW
   bpcs <- getBranchPC_
-  constraintPC bpcs pW $ \p src ->
+  constraintPC bpcs pW' $ \p src ->
        "Constructor " ++ prettyPrint ctyT ++ 
-       " with declared write effect " ++ prettyPrint pW ++
+       " 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 ->
+  constraintPC epc pW' $ \p src ->
       "Constructor " ++ prettyPrint ctyT ++ 
-      " with declared write effect " ++ prettyPrint pW ++
+      " 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 (Right ctyT)) exns
+  mapM_ (uncurry $ exnConsistent (Right ctyT)) exnPs
 
   -- Fix outgoing state
-  let exns' = map (first ExnType) exns
-  activateExns exns'     -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
+  activateExns exnAcs    -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
   applyLockMods lMods    -- ==> S'' = S'[lockMods ||>>= lMods, 
   scrambleActors Nothing -- ==>          actors scrambled]
 
@@ -568,7 +576,7 @@
             (tyE, pE, e') <- tcExp e
             (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args
             let tas' = map (ActualArg ()) tas
-            (tps, genMSig) <- lookupMethodT tyE i tas' (map unStateType tysArgs)
+            (tps, genMSig) <- instThis pE <$> lookupMethodT tyE i tas' (map unStateType tysArgs)
             tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ 
                                      zip tps tas'
             let msig = instantiate (zip tps tArgs) genMSig
@@ -584,15 +592,14 @@
             "Required lock state: " ++ prettyPrint lExp ++ "\n" ++
             "Current lock state: " ++ prettyPrint l
   -- 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'
+      (exnPs, exnAcs) = 
+          unzip [ ((t, (rX', wX')),  (ExnType t, (wX', modsX))) |
+                  (t, ExnSig rX wX modsX) <- exns,
+                  let rX' = substParPols subst rX, 
+                  let wX' = substParPols subst wX 
+                ]
   mapM_ (\(arg,argP,parP) -> 
                   constraintLS argP parP $
                       "Method applied to argument with too restrictive policy:\n" ++ 
@@ -615,38 +622,39 @@
            " 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)) exnPs
 
   -- Fix outgoing state
-  let exnsT = map (first ExnType) exns'
-  activateExns exnsT     -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
+--  let exnsT = [ (ExnType tX, (wX, modsX)) | ((tX, (_, wX)), modsX) <- zip exnsPs ]
+--      exnsT = map (first ExnType) exnPs
+  activateExns exnAcs    -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]
   applyLockMods lMods    -- ==> S'' = S'[lockMods ||>>= lMods, 
   scrambleActors Nothing -- ==>          actors scrambled]
 
   styR <- getStateType Nothing Nothing tyR
-  return (styR, pE `join` pR, ef styR)
+  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
+--substExnParPols :: [(Ident (), ActorPolicy)] -> ExnSig -> (ActorPolicy, ActorPolicy)
+--substExnParPols subst (ExnSig rX wX _ms) = 
+--    (substParPrgPols subst rX, substParPrgPols subst wX)
 
 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 (RealPolicy pol) = substParPrgPols subst pol
 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
+
+substParPrgPols :: [(Ident (), ActorPolicy)] -> PrgPolicy TcActor -> ActorPolicy
+substParPrgPols subst p@(TcRigidVar i) = 
+    case lookup i subst of
+      Just newP -> newP
+      Nothing -> RealPolicy p
+substParPrgPols subst (TcJoin p q) = 
+    substParPrgPols subst p `join` substParPrgPols subst q
+substParPrgPols subst (TcMeet p q) = 
+    substParPrgPols subst p `meet` substParPrgPols subst q
+substParPrgPols _ p = RealPolicy p
 
 
 -----------------------------------
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
@@ -47,7 +47,8 @@
              $ "if-statement requires a condition of type compatible with boolean\n"
                ++ "Found type: " ++ prettyPrint tyC
   extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do
-    (s1', s2') <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2
+    (s1', s2') <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) 
+                  ||| tcStmt s2
     return $ IfThenElse Nothing c' s1' s2'
 
 -- Rule IFTHEN
@@ -219,11 +220,12 @@
   tyP <- liftTcDeclM $ evalSrcType t
   -- TODO check tyP <: "Throwable"
   pR <- liftTcDeclM $ getReadPolicy ms -- getParamPolicy i ms
-  pW <- newMetaPolVar               -- \pi, where \pi is fresh
+  pW <- newMetaPolVar i              -- \pi, where \pi is fresh
   addBranchPC (exnE tyP) $          -- E' = E[branchPC{tyP +-> bottom},
-    registerExn tyP pR pW $ do      --        exns{tyP +-> (pR, \pi)}]
+    registerExn tyP (RealPolicy pR) pW $ do      --        exns{tyP +-> (pR, \pi)}]
       block' <- tcBlock block
-      extendVarEnv i (VSig tyP pR True False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}]
+      extendVarEnv i (VSig tyP (RealPolicy pR) True False (isFinal ms)) $ do 
+                                         -- E* = E[vars{x +-> (tyP, pR)}]
         msX <- getExnState (ExnType tyP)
         maybeM msX $ mergeWithState  -- S* = St <> St[exns](X)[state]
         cBlock' <- tcBlock cBlock
@@ -359,7 +361,7 @@
     (_,_,es') <- unzip3 <$> mapM tcExp es
     (Just $ ForInitExps Nothing es',) <$> tca
 withInits (Just (ForLocalVars _ ms t vds)) tca = do
-  pV  <- localVarPol ms
+  pV  <- localVarPol ms vds
   tyV <- liftTcDeclM $ evalSrcType t
   (vds', a) <- tcLocalVars pV tyV (isFinal ms) vds [] $ tca
   return $ (Just $ ForLocalVars Nothing (map notAppl ms) (notAppl t) vds', a)
@@ -384,7 +386,7 @@
 
 -- Rule LOCALVARINIT/LOCALVARDECL
 tcBlockStmts (LocalVars _ ms t vds : bss) = do
-  pV  <- localVarPol ms
+  pV  <- localVarPol ms vds
   tyV <- liftTcDeclM $ evalSrcType t
 --  debugTc $ "Array type pre: " ++ prettyPrint t
   (vds', bss') <- tcLocalVars pV tyV (isFinal ms) vds [] $ 
@@ -452,11 +454,13 @@
     fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd
 
 
-localVarPol :: [Modifier ()] -> TcCodeM ActorPolicy
-localVarPol ms = 
+localVarPol :: [Modifier ()] -> [VarDecl ()] -> TcCodeM ActorPolicy
+localVarPol ms vds = 
     case [ p | Reads _ p <- ms ] of
-      [] -> newMetaPolVar --return bottom
-      [p] -> liftTcDeclM $ evalPolicy p
+      [] -> newMetaPolVar . getVarId . head $ vds     -- TODO a TcVarPolicy for each variable, or a shared one ?
+            where getVarId (VarDecl _ (VarId _ i) _) = i
+                  getVarId (VarDecl _ (VarDeclArray _ vdi) _) = getVarId $ VarDecl () vdi Nothing 
+      [p] -> liftTcDeclM $ RealPolicy <$> evalPolicy p
       _ -> fail $ "Only one read policy allowed on local variable"
 
 ---------------------------------------------------
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
@@ -47,14 +47,14 @@
   deriving (Show, Data, Typeable)
 
 data MethodSig = MSig {
-      mRetType :: TcType,
-      mRetPol  :: ActorPolicy,
-      mPars    :: [Ident ()],
-      mParPols :: [ActorPolicy],
-      mWrites  :: ActorPolicy,
-      mExpects :: [TcLock],
-      mLMods   :: ([TcLock],[TcLock]),
-      mExns    :: [(TcType, ExnSig)]
+      mRetType   :: TcType,
+      mRetPol    :: ActorPolicy,
+      mPars      :: [Ident ()],
+      mParBounds :: [ActorPolicy],
+      mWrites    :: ActorPolicy,
+      mExpects   :: [TcLock],
+      mLMods     :: ([TcLock],[TcLock]),
+      mExns      :: [(TcType, ExnSig)]
     }
   deriving (Show, Data, Typeable)
 
@@ -66,12 +66,12 @@
   deriving (Show, Data, Typeable)
 
 data ConstrSig = CSig {
-      cPars    :: [Ident ()],
-      cParPols :: [ActorPolicy],
-      cWrites  :: ActorPolicy,
-      cExpects :: [TcLock],
-      cLMods   :: ([TcLock],[TcLock]),
-      cExns    :: [(TcType, ExnSig)]
+      cPars      :: [Ident ()],
+      cParBounds :: [ActorPolicy],
+      cWrites    :: ActorPolicy,
+      cExpects   :: [TcLock],
+      cLMods     :: ([TcLock],[TcLock]),
+      cExns      :: [(TcType, ExnSig)]
     }
   deriving (Show, Data, Typeable)
 
@@ -105,7 +105,7 @@
       constrs     :: ConstrMap,
       locks       :: Map (Ident ()) LockSig,
       -- known policy-level entities
-      policies    :: Map (Ident ()) ActorPolicy,
+      policies    :: Map (Ident ()) (PrgPolicy TcActor),
       actors      :: Map (Ident ()) ActorId,
       -- typemethod eval info
       typemethods :: Map (Ident ()) ([Ident ()], Block ()),
@@ -128,7 +128,7 @@
                 packages    = Map.empty
               }
 
-hardCodedArrayTM :: TcType -> ActorPolicy -> TypeSig
+hardCodedArrayTM :: TcType -> PrgPolicy TcActor -> TypeSig
 hardCodedArrayTM ty p = 
     let memTM = emptyTM {
                   fields = Map.fromList [(Ident () "length", VSig intT thisP False False True)]
@@ -365,3 +365,10 @@
           as   = [ (i, n ) | (ActorParam     _ i, TcActualActor      n) <- pas ]
           ps   = [ (i, p ) | (PolicyParam    _ i, TcActualPolicy     p) <- pas ]
           locs = [ (i, ls) | (LockStateParam _ i, TcActualLockState ls) <- pas ]
+
+
+instThis :: Data a => ActorPolicy -> a -> a
+instThis p = transformBi instThisPol
+  where instThisPol :: ActorPolicy -> ActorPolicy
+        instThisPol (RealPolicy q) = substThis p q
+        instThisPol q = q
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
@@ -44,7 +44,7 @@
 
 data TcRefType
     = TcClsRefT TcClassType
-    | TcArrayT TcType ActorPolicy
+    | TcArrayT TcType (PrgPolicy TcActor)
     | TcTypeVar (Ident ())
     | TcNullT
   deriving (Eq, Ord, Show, Data, Typeable)
@@ -129,10 +129,10 @@
 clsTypeToType :: TcClassType -> TcType
 clsTypeToType = TcRefT . TcClsRefT
 
-arrayType :: TcType -> ActorPolicy -> TcType
+arrayType :: TcType -> PrgPolicy TcActor -> TcType
 arrayType = (TcRefT .) . TcArrayT
 
-mkArrayType :: TcType -> [ActorPolicy] -> TcType
+mkArrayType :: TcType -> [PrgPolicy TcActor] -> TcType
 mkArrayType = foldr (flip arrayType)
 
 
@@ -155,7 +155,7 @@
 --                  Just n -> n
 --                  Nothing -> error $ "typeName_: " ++ show typ
 
-isClassType, isRefType, isNullType :: TcStateType -> Bool
+isClassType, isRefType, isPrimType, isNullType :: TcStateType -> Bool
 isClassType (TcType (TcRefT (TcClsRefT (TcClassT{})))) = True
 isClassType (TcInstance{}) = True
 isClassType _ = False
@@ -164,6 +164,9 @@
 isRefType (TcInstance{}) = True
 isRefType _ = False
 
+isPrimType (TcType (TcPrimT _)) = True
+isPrimType _ = False
+
 mNameRefType :: TcRefType -> Maybe (Name ())
 mNameRefType (TcClsRefT (TcClassT n as)) =
     if null as then Just (mkUniformName_ AmbName $ flattenName n) else Nothing
@@ -193,7 +196,7 @@
 isPolicyType :: TcStateType -> Bool
 isPolicyType = isJust . mPolicyPol
 
-mArrayType :: TcType -> Maybe (TcType, [ActorPolicy])
+mArrayType :: TcType -> Maybe (TcType, [PrgPolicy TcActor])
 mArrayType (TcRefT (TcArrayT ty p)) = Just $
     case mArrayType ty of
       Nothing -> (ty, [p])