diff --git a/paragon.cabal b/paragon.cabal
--- a/paragon.cabal
+++ b/paragon.cabal
@@ -1,5 +1,5 @@
 Name:                   paragon
-Version:                0.1.13
+Version:                0.1.15
 License:                BSD3
 License-File:           LICENSE
 Author:                 Niklas Broberg
diff --git a/src/Language/Java/Paragon.hs b/src/Language/Java/Paragon.hs
--- a/src/Language/Java/Paragon.hs
+++ b/src/Language/Java/Paragon.hs
@@ -33,7 +33,7 @@
   deriving (Show, Eq)
 
 versionString, usageHeader :: String
-versionString = "Paragon Compiler version: 0.1.13"
+versionString = "Paragon Compiler version: 0.1.15"
 usageHeader = "Usage: parac [OPTION...] files..."
 
 options :: [OptDescr Flag]
@@ -68,10 +68,13 @@
 
 compile :: [Flag] -> String -> IO ()
 compile flags filePath = do
-  let (directory,fileName) = splitFileName filePath --relative or absolute path?
+  finePrint $ "Filepath: " ++ filePath
+  let (directoryRaw,fileName) = splitFileName filePath --relative or absolute path?
+      -- Workaround for old and buggy 'filepath' versions
+      directory = if null directoryRaw then "./" else directoryRaw
   let pDir = case [ dir | PiPath dir <- flags ] of
                p:_ -> p
-               _ -> "."
+               _ -> "./"
   fc <- readFile filePath
   ast <- liftE $ parser compilationUnit fc
   extraPrint "Parsing complete!"
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
@@ -668,10 +668,10 @@
 -- For loops
 
 forInit :: P (ForInit ())
-forInit = (do
+forInit = (try $ do
     (m,t,vds) <- localVarDecl
     return $ ForLocalVars () m t vds) <|>
-    seplist1 stmtExp comma >>= return . ForInitExps ()
+    ForInitExps () <$> seplist1 stmtExp comma
 
 forUp :: P [Exp ()]
 forUp = seplist1 stmtExp comma
@@ -910,6 +910,9 @@
      FieldAccess () fa -> return fa
      _ -> fail ""
 
+fieldAccessExp :: P (Exp ())
+fieldAccessExp = FieldAccess () <$> fieldAccess
+
 {-
 fieldAccess :: P FieldAccess
 fieldAccess = try fieldAccessNPS <|> do
@@ -1115,7 +1118,12 @@
     (tok Op_AAnd    >> return (CAnd      ())) <|>
     (tok Op_OOr     >> return (COr       ()))
 
+typeArgInfixOp :: P (Op ())
+typeArgInfixOp = 
+    (tok Op_Star >> return (Mult ())) <|> 
+    (tok Op_Plus >> return (Add  ()))
 
+
 ----------------------------------------------------------------------------
 -- Types
 
@@ -1197,6 +1205,58 @@
 bounds = tok KW_Extends >> seplist1 refType (tok Op_And)
 
 typeArgs :: P [TypeArgument ()]
+typeArgs = tok Op_LThan {- < -} >> typeArgsSuffix
+
+typeArgsSuffix :: P [TypeArgument ()]
+typeArgsSuffix =
+  (do tok Op_Query
+      wcArg <- Wildcard () <$> opt wildcardBound
+      rest <- typeArgsEnd
+      return $ wcArg:rest) <|>
+  (do lArg <- ActualArg () <$> parens (ActualLockState () <$> seplist1 lock comma)
+      rest <- typeArgsEnd
+      return $ lArg:rest) <|>
+  (try $ do rt   <- refType
+            rest <- typeArgsEnd
+            let tArg = case nameOfRefType rt of
+                         Just n -> ActualName () n
+                         _ -> ActualType () rt
+            return $ (ActualArg () tArg):rest) <|>
+  (do eArg <- ActualArg () . ActualExp () <$> argExp
+      rest <- typeArgsEnd
+      return $ eArg:rest)
+
+      where nameOfRefType :: RefType () -> Maybe (Name ())
+            nameOfRefType (ClassRefType _ (ClassType _ ias)) =
+                let (is, as) = unzip ias
+                in if all null as then Just (Name () is) else Nothing
+            nameOfRefType _ = Nothing
+
+typeArgsEnd :: P [TypeArgument ()]
+typeArgsEnd = 
+    (tok Op_GThan {- > -} >> return []) <|>
+    (tok Comma >> typeArgsSuffix)
+
+argExp :: P (Exp ())
+argExp = do
+  e1 <- argExp1
+  fe <- argExpSuffix
+  return $ fe e1
+
+argExp1 :: P (Exp ())
+argExp1 = PolicyExp () <$> policyExp 
+          <|> try methodInvocationExp
+          <|> try fieldAccessExp
+          <|> ExpName () <$> name
+
+argExpSuffix :: P (Exp () -> Exp ())
+argExpSuffix = 
+    (do op <- typeArgInfixOp
+        e2 <- argExp
+        return $ \e1 -> BinOp () e1 op e2) <|> return id
+
+{-
+typeArgs :: P [TypeArgument ()]
 typeArgs = angles $ seplist1 typeArg comma
 
 typeArg :: P (TypeArgument ())
@@ -1209,14 +1269,20 @@
                  ActualPolicy () . ExpName () <$> (tok KW_P_Policy >> name) <|>
                  ActualActor () <$> (tok KW_P_Actor >> name) <|>
                  ActualType () <$> refType
-
+-}
 wildcardBound :: P (WildcardBound ())
 wildcardBound = tok KW_Extends >> ExtendsBound () <$> refType
     <|> tok KW_Super >> SuperBound () <$> refType
 
 nonWildTypeArgs :: P [NonWildTypeArgument ()]
-nonWildTypeArgs = angles $ seplist nonWildTypeArg (tok Comma)
+nonWildTypeArgs = typeArgs >>= mapM checkNonWild
+  where checkNonWild (ActualArg _ arg) = return arg
+        checkNonWild _ = fail "Use of wildcard in non-wild context"
 
+
+--nonWildTypeArgs :: P [NonWildTypeArgument ()]
+--nonWildTypeArgs = angles $ seplist nonWildTypeArg (tok Comma)
+
 ----------------------------------------------------------------------------
 -- Names
 
@@ -1426,7 +1492,7 @@
           actIs = [ i | ActorParam _ i <- pars ]
           polIs = [ i | PolicyParam _ i <- pars ]
 
--- Instantiation is needed for all four kinds.
+{-- Instantiation is needed for all four kinds.
 instantiate :: Data a => [(TypeParam (), TypeArgument ())] -> a -> a
 instantiate pas = transformBi instT 
                   . transformBi instA 
@@ -1471,7 +1537,12 @@
 
 
           typs = [ (i,rt) | (TypeParam _ i _,    ActualArg _ (ActualType      _ rt)) <- pas ]
-          as   = [ (i,n)  | (ActorParam  _ i,    ActualArg _ (ActualActor     _ n )) <- pas ]
-          ps   = [ (i,p)  | (PolicyParam _ i,    ActualArg _ (ActualPolicy    _ p )) <- pas ]
+          as   = [ (i,e)  | (ActorParam  _ i,    ActualArg _ (ActualExp       _ e )) <- pas ]
+              ++ [ (i, ExpName () $ Name () $ fst $ unzip iargs)  
+                       | (ActorParam   _ i,    ActualArg _ (ActualType _ (ClassRefType _ (ClassType _ iargs))) <- pas ]
+          ps   = [ (i,e)  | (PolicyParam _ i,    ActualArg _ (ActualExp    _ e )) <- pas ]
+              ++ [ (i, ExpName () $ Name () $ fst $ unzip iargs)  
+                       | (PolicyParam  _ i,    ActualArg _ (ActualType _ (ClassRefType _ (ClassType _ iargs))) <- pas ]
           lps  = [ (i,le) | (LockStateParam _ i, ActualArg _ (ActualLockState _ le)) <- pas ]
 
+-}
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
@@ -350,6 +350,7 @@
   pretty (ForLocalVars _ mods t vds) =
     hsep $ map pretty mods ++
             pretty t: punctuate comma (map pretty vds)
+  pretty (ForInitExps _ es) = hsep $ punctuate comma $ map pretty es
 
 
 -----------------------------------------------------------------------
@@ -562,10 +563,10 @@
   pretty (Wildcard _ mBound) = char '?' <+> maybePP mBound
 
 instance Pretty (NonWildTypeArgument a) where
+  pretty (ActualName   _ n) = pretty n
   pretty (ActualType   _ t) = pretty t
-  pretty (ActualPolicy _ p) = text "policy" <+> pretty p
-  pretty (ActualActor  _ n) = text "actor" <+> pretty n
-  pretty (ActualLockState _ ls) = text "lock[]" <+> ppArgs ls -- HACK ALERT
+  pretty (ActualExp _ e) = pretty e
+  pretty (ActualLockState _ ls) = {- text "lock[]" <+> -} ppArgs ls -- HACK ALERT
 
 instance Pretty (WildcardBound a) where
   pretty (ExtendsBound _ rt) = text "extends" <+> pretty rt
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
@@ -490,9 +490,9 @@
   deriving (Eq,Ord,Show,Typeable,Data,Functor)
 
 data NonWildTypeArgument a
-    = ActualType a (RefType a)
-    | ActualPolicy a (Policy a)
-    | ActualActor  a (Name a)
+    = ActualName a (Name a)      -- Can mean a type or an exp
+    | ActualType a (RefType a)
+    | ActualExp a (Exp a)        -- Constrained to argExp
     | ActualLockState a [Lock a]
   deriving (Eq,Ord,Show,Typeable,Data,Functor)
 
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
@@ -3,6 +3,7 @@
 import Language.Java.Paragon.Syntax
 import Language.Java.Paragon.Parser
 import Language.Java.Paragon.Pretty
+import Language.Java.Paragon.Verbosity
 
 import Language.Java.Paragon.TypeCheck.Actors
 import Language.Java.Paragon.TypeCheck.Constraints
@@ -35,15 +36,16 @@
 
 typeCheck :: DirectoryPath -> DirectoryPath -> CompilationUnit () -> IO (CompilationUnit ())
 typeCheck currentDir piDir ast@(CompilationUnit _ pkg imps [td]) = do
+      finePrint $ "Current dir: " ++ show currentDir
       let (skoTd, skoTy) = skolemTypeDecl td
       e <- runTcCont skoTy $ do
              withEnvFromImps piDir "" allImps $ do
-               --debug "Import env setup"
+               debug "Import env setup"
                withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do
-                 --debug "TypeMap completed"
+                 debug "Initial type map completed"
                  tm <- getTypeMap
-                 --debug $ "TypeMap: " ++ show tm
-                 withExpandedNames skoTd $ \fullTd -> do
+                 debug $ "Initial type map: " ++ show tm
+                 withExpandedNames piDir allImps skoTd $ \fullTd -> do
                     --debug $ "Full AST:\n" ++ prettyPrint fullTd
                     typeCheckTd fullTd
                     -- debug $ "Type checking completed!"
@@ -55,12 +57,13 @@
    where allImps = defaultImportDecls ++ imps
                                                          
 
-withExpandedNames :: TypeDecl () -> (TypeDecl () -> TcCont r a) -> TcCont r a
-withExpandedNames td tcbaf = do
+withExpandedNames :: DirectoryPath -> [ImportDecl ()] -> TypeDecl () -> (TypeDecl () -> TcCont r a) -> TcCont r a
+withExpandedNames piDir imps td tcbaf = do
+  mNames <- buildExpansionMap piDir imps
   tm <- getTypeMap
   --debug $ "TypeMap: " ++ show tm
-  let mNames = buildExpansionMap tm
-      fullTd = expandNames mNames td
+  -- let mNames = buildExpansionMap tm
+  let fullTd = expandNames mNames td
   --debug $ "ExpansionMap: " ++ show mNames
   tcbaf fullTd
 
@@ -80,6 +83,41 @@
               Nothing -> ct
         expandCT ct = ct
 
+buildExpansionMap :: DirectoryPath -> [ImportDecl ()] -> TcCont r (Map (Ident ()) [Ident ()])
+buildExpansionMap piDir imps = foldM (buildExpMapFromImp piDir) Map.empty imps
+
+buildExpMapFromImp :: DirectoryPath 
+                   -> Map (Ident ()) [Ident ()] 
+                   -> ImportDecl () 
+                   -> TcCont r (Map (Ident ()) [Ident ()])
+buildExpMapFromImp piDir em imp@(ImportDecl _ stat (Name _ is) onDemand) = 
+    case (stat, onDemand) of
+      (False, False) -> do -- Single-type: import pkg.path.TypeName;
+          let relative  = pathOf is
+              absoluteFile = piDir ++ pSep:relative ++ ".pi"
+              className = last is
+          checkM (liftIO $ doesFileExist absoluteFile) $
+                     "Cannot find interface file for import " ++ prettyPrint imp
+          return $ Map.insert className is em
+      (False, True) -> do -- On-demand package: import pkg.path.*;
+          let relative  = pathOf is
+              absoluteDir = piDir ++ pSep:relative ++ [pSep]
+          checkM (liftIO $ doesDirectoryExist absoluteDir) $
+                     "Cannot find package for import " ++ prettyPrint imp
+          names <- liftIO $ getDirectoryContents absoluteDir
+          let classNames = 
+                  [ Ident () base
+                    | name <- names
+                    , let (base, extn) = (takeBaseName name, takeExtension name)
+                    , extn == ".pi"
+                  --  , base /= thisStr 
+                  ]
+              newMap = Map.fromList (zip classNames (map ((is++) . return) classNames))
+          return $ Map.union em newMap
+
+  
+
+{-
 buildExpansionMap :: TypeMap -> Map (Ident ()) [Ident ()]
 buildExpansionMap tm = 
   let fs = Map.keys (fields tm)
@@ -90,7 +128,7 @@
       ptms = map (second buildExpansionMap) pts
       mps = map (\(i,mp) -> Map.map (i:) mp) ptms
   in foldl Map.union m1 mps
-
+-}
 ------------------------------------------------------------------
 -- Implicitly imported core packages
 -- TODO: Not yet used.
@@ -121,6 +159,8 @@
 withEnvFromImp :: DirectoryPath -> String -> (ImportDecl ()) -> TcCont r a -> TcCont r a
 -- import java.*;
 withEnvFromImp piDir thisStr imp@(ImportDecl _ False (Name _ pkgNames) True) tcba = do
+    when (null pkgNames) $
+         debug $ "Setting up import from current dir: " ++ show piDir
     --debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames)
     let relative    = pathOf pkgNames
         absoluteDir = piDir ++ pSep:relative ++ [pSep]
@@ -130,6 +170,7 @@
                                , let (base, extn) = (takeBaseName name, takeExtension name)
                                , extn == ".pi"
                                , base /= thisStr ]
+    debug $ "Found files: " ++ show classPathsAndNames
     withEnvFromPkg pkgNames classPathsAndNames $ tcba
 
 -- import java.TypeName;
@@ -141,8 +182,21 @@
         pkgNames = init clsPkgName
     withEnvFromSingleClass pkgNames absoluteFile className $ tcba
 
+-- import static java.TypeName.Ident;
+withEnvFromImp piDir _ imp@(ImportDecl _ True (Name _ pathToIdent) False) tcba = do
+   error "Single static import not yet supported"
 
+-- import static java.TypeName.*;
+withEnvFromImp piDir _ imp@(ImportDecl _ True (Name _ clsPkgName) True) tcba = do
+   let relative = pathOf clsPkgName
+       absoluteFile = piDir ++ pSep:relative ++ ".pi"
+       (Ident _ className) = last clsPkgName
+       pkgNames = init clsPkgName
+   withEnvFromSingleClass [] absoluteFile className $ tcba
+  
 
+
+
 withEnvFromPkg :: [Ident ()] -> [(FilePath, String)] -> TcCont r a -> TcCont r a
 withEnvFromPkg [] [] tcba = tcba -- Hack for the "this" package
 withEnvFromPkg pkgPath [] tcba = do
@@ -205,7 +259,7 @@
         
             where spawnActor, evalActor, aliasActor :: ([Modifier ()],VarDecl ()) -> TcCont r a -> TcCont r a
                   spawnActor (ms, VarDecl _ (VarId _ i) _) tcba = do
-                    a <- freshActorId
+                    a <- freshActorId (prettyPrint i)
                     p <- getReadPolicy ms
                     let vti = VSig actorT p (Static () `elem` ms) (Final () `elem` ms)
                     withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
@@ -531,13 +585,14 @@
   withFoldMap typeCheckLockDecl ls $ tcba
 
 typeCheckLockDecl :: MemberDecl () -> TcCont r a -> TcCont r a
-typeCheckLockDecl (LockDecl _ ms i mps props) tcba = do
-{--        lPol <- getLockPolicy ms
-        -- TODO: Store lock properties!
-        let arity = length mps
-        withTypeMap (\tm -> 
-          tm { lockArities = Map.insert i arity (lockArities tm) }) $ -}
-            tcba
+typeCheckLockDecl (LockDecl _ ms i mps mprops) tcba = do
+  lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
+    pol <- getLockPolicy ms
+--    return $ VSig (lockT []) pol True True
+    -- TODO: Check properties!
+    return $ LSig pol (length mps)
+  withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
+    tcba
 
 -- end Locks
 ---------------------------------------------------------------
@@ -670,6 +725,7 @@
                       ++ concat (intersperse ", " (map prettyPrint fis))  ++ ":\n") $ do
     -- 1. Check field type
     ty <- evalSrcType t
+    debug $ "Type evaluated to: " ++ show ty
     -- _  <- lookupTypeOfT ty <$> getTypeMap -- TODO
     -- 2. Typecheck and evaluate field policy
     let rPolExps = [ e | Reads _ e <- ms ]
@@ -694,6 +750,7 @@
               addField vti (VarDecl _ (VarId _ i) _) =
                   withTypeMap $ \tm -> 
                       tm { fields = Map.insert i vti (fields tm) }
+              addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd
 
 -- Methods
 typeCheckSignature st md@(MethodDecl _ ms tps retT i ps exns mb) tcba
@@ -705,12 +762,13 @@
     withFoldMap withTypeParam tps $ do
     -- 1. Check return type
     ty <- evalReturnType retT
+    {- We've checked this in evalReturnType already
     when (isRefType ty) $ do 
       mTm <- lookupTypeOfT ty <$> getTypeMap
       case mTm of
         Just _ -> return ()
         Nothing -> fail $ "Unknown type: " ++ prettyPrint ty
-
+    -}
     -- 2. Typecheck and evaluate policy modifiers
     withFoldMap withParam ps $ checkPolicyMods st ms 
       "typeCheckSignature: At most one return/write modifier allowed per method"
@@ -768,16 +826,16 @@
   withTypeMap (\tm -> tm { constrs = Map.insert pTs (tps,cti) (constrs tm) }) $
     tcba
 
--- Locks
-typeCheckSignature st ld@(LockDecl _ ms i mps mprops) tcba = do
+-- Locks -- already handled
+-- typeCheckSignature st ld@(LockDecl _ ms i mps mprops) tcba = tcba
   --debug $ "typeCheckSignature: " ++ prettyPrint ld
-  lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
-    pol <- getLockPolicy ms
+--  lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
+--    pol <- getLockPolicy ms
 --    return $ VSig (lockT []) pol True True
     -- TODO: Check properties!
-    return $ LSig pol (length mps)
-  withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
-    tcba
+--    return $ LSig pol (length mps)
+--  withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $
+--    tcba
 
 typeCheckSignature _ _ tcba = tcba
 
@@ -793,11 +851,11 @@
 typeCheckExnSig st (ExceptionSpec _ ms xT) = do
   withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do
     ty <- TP.TcRefT <$> evalSrcRefType xT
-    -- Check that type exists
+    {-- Check that type exists - now done in evalSrcRefType
     mTm <- lookupTypeOfT ty <$> getTypeMap
     case mTm of
       Just _ -> return ()
-      Nothing -> fail $ "Unknown exception type: " ++ prettyPrint ty
+      Nothing -> fail $ "Unknown exception type: " ++ prettyPrint ty -}
     checkPolicyMods st ms 
        "typeCheckSignature: At most one read/write modifier allowed per exception"
     rPol <- getReadPolicy ms
@@ -847,7 +905,7 @@
   -- tm <- getTypeMap
   -- debug $ show tm
   -- debug $ "typeCheckPolicyMod " ++ show polExp
-  ((ty, _pol), cs) <- runTc (simpleEnv top) st 
+  ((ty, _pol), cs) <- runTc (simpleEnv top $ "policy modifier " ++ prettyPrint polExp) st 
                         (--liftBase (debug "inside runTC") >> 
                                   tcExp polExp)
   check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?"
@@ -870,7 +928,7 @@
 typeCheckInitDecl :: TcPolicy -> TcState -> Block () -> TcCont r TcState
 typeCheckInitDecl lim st bl = do
     tm <- getTypeMap
-    (st,cs) <- runTc (simpleEnv lim) st $
+    (st,cs) <- runTc (simpleEnv lim $ "initializer block") st $
                       addBranchPCList (Map.keys (fields tm)) $ do
                         tcBlock bl
                         getState
@@ -908,10 +966,14 @@
   case mInit of
     Nothing -> return ()
     Just (InitExp _ e) -> do
-      (_,cs) <- runTc (simpleEnv lim) st $ do
+      (_,cs) <- runTc (simpleEnv lim $ "field initializer " ++ prettyPrint e) st $ do
                   (ty, pol) <- tcExp e
                   checkM (liftCont $ ty <: matchTy) $ "typeCheckVarDecl: type mismatch"
-                  constraint_ pol matchPol
+                  constraint [] pol matchPol $
+                          "Cannot assign result of expression " ++ prettyPrint e ++
+                          " with policy " ++ prettyPrint pol ++
+                          " to location " ++ prettyPrint i ++ 
+                          " with policy " ++ prettyPrint matchPol
       solve cs
     Just (InitArray _ arr) ->
       case mArrayType matchTy of
@@ -919,7 +981,7 @@
                         ++ " of non-array type " ++ prettyPrint matchTy
                         ++ " given literal array initializer"
         Just (baseTy, pols) -> do
-         (_,cs) <- runTc (simpleEnv lim) st $
+         (_,cs) <- runTc (simpleEnv lim $ "array initializer " ++ prettyPrint arr) st $
                      tcArrayInit baseTy pols arr
          solve cs
 --    _ -> error $ "typeCheckVarDecl: Array syntax not yet supported"
@@ -940,15 +1002,16 @@
       pars = map fst parVtis
       exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
       exnLMods = map (second exnMods) xSigs
-      parEnts = [ (VarEntity $ Name () [i], bottom) | i <- pars ]
-      exnEnts = [ (ExnEntity t, bottom) | t <- map fst xSigs ]
-      branchMap = Map.insert returnE bottom $ Map.fromList (parEnts ++ exnEnts)
+      parEnts = [ (VarEntity $ Name () [i], []) | i <- pars ]
+      exnEnts = [ (ExnEntity t, []) | t <- map fst xSigs ]
+      branchMap = Map.insert returnE [] $ Map.fromList (parEnts ++ exnEnts)
+      writeErr = "body of method " ++ prettyPrint i
       env = TcEnv {
               vars = Map.fromList parVtis,
               lockstate = expLs,
               returnI = Just (tyRet, pRet),
               exnsE = Map.fromList exnPols,
-              branchPCE = (branchMap, pWri)
+              branchPCE = (branchMap, [(pWri, writeErr)])
             }
 
   -- debug $ "Using env: " ++ show env
@@ -988,13 +1051,14 @@
       fieEnts = concat [ [ThisFieldEntity i,VarEntity (Name () [i])] 
                              | (i, VSig _ _ False _) <- Map.assocs (fields tm) ]
   --debug $ "fieEnts: " ++ show fieEnts
-  let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat bottom)
+  let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat [])
+      writeErr = "body of constructor " ++ prettyPrint ci
       env = TcEnv {
               vars = Map.fromList parVtis,
               lockstate = expLs,
               returnI = error "Cannot return from constructor",
               exnsE = Map.fromList exnPols,
-              branchPCE = (branchMap, pWri)
+              branchPCE = (branchMap, [(pWri, writeErr)])
             }
 
   --debug $ "Using branch map: " ++ show (branchPCE env)
@@ -1088,4 +1152,4 @@
 
 
 debug :: String -> TcCont r ()
-debug str = liftIO $ putStrLn $ "DEBUG: " ++ str
+debug str = liftIO $ finePrint $ "DEBUG: " ++ str
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
@@ -17,7 +17,7 @@
 -- 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 | Alias Int | ActorTPVar (Ident ())
+data ActorId = Fresh Int String | Alias Int | ActorTPVar (Ident ())
  deriving (Show, Eq, Ord, Data, Typeable)
 
 infix 5 `unifies`, `unify`
@@ -25,7 +25,7 @@
 -- Precondition: No ActorTPVars
 unifies :: ActorId -> ActorId -> Bool
 -- If we have the exact (fresh) ids, we can tell exactly
-unifies (Fresh x) (Fresh y) = x == y
+unifies (Fresh x _) (Fresh y _) = x == y
 unifies _ _ =  True
 -- 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
@@ -47,8 +47,8 @@
 reprs (Alias x xs) = x:xs
 -}
 getId :: ActorId -> Int
-getId (Fresh x) = x
-getId (Alias x) = x
+getId (Fresh x _) = x
+getId (Alias x  ) = x
 
 {-
 reprName :: ActorId -> Name
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
@@ -7,5 +7,7 @@
 data Constraint = LRT TcPolicyRec TcPolicy TcPolicy
   deriving Show
 
-solve :: [Constraint] -> TcCont r ()
+type ConstraintWMsg = (Constraint, String)
+
+solve :: [ConstraintWMsg] -> TcCont r ()
 solve cs = liftIO $ mapM_ print cs -- DEBUG
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
@@ -44,7 +44,7 @@
                 SubstM tau maxID = groundSubst m d 
                 (TcClause ruleHead ruleBody) = d
                 -- include facts to database that all concrete values are actors:
-                allAreActors = map (\x -> TcAtom (Name () [Ident () actorAtomString]) [TcActor (Fresh x)]) [0..maxID]
+                allAreActors = map (\x -> TcAtom (Name () [Ident () actorAtomString]) [TcActor (Fresh x $ "#"++show x)]) [0..maxID]
 
 -- For joins and meets, we want to try all the candidates.
 -- We have that 
@@ -176,7 +176,7 @@
   where rh = aliasToFreshAtom ruleHead               
         rb = map aliasToFreshAtom ruleBody
         aliasToFreshAtom (TcAtom name actors) = TcAtom name (map aliasToFreshActor actors)
-	aliasToFreshActor (TcActor (Alias i)) = TcActor (Fresh i)
+	aliasToFreshActor (TcActor (Alias i)) = TcActor (Fresh i $ "#"++show i)
         aliasToFreshActor x = x
 
 -- Returns the highest integer found as actorID
@@ -185,8 +185,8 @@
   where h = getHeighestActorId ruleHead
         b = foldl (\t atom -> max (getHeighestActorId atom) t) 0 ruleBody
         getHeighestActorId (TcAtom name actors) = foldl (\t actor -> max (acc actor) t ) 0 actors
-        acc (TcActor (Fresh i)) = i
-        acc _                   = 0
+        acc (TcActor (Fresh i _)) = i
+        acc _                     = 0
 
 -- Returns an extended substitution mapping all variables in TcAtom
 -- to fresh constants not occurring in the first two arguments
@@ -198,7 +198,7 @@
 freshSubstActor sub@(SubstM mapping maxId) (TcVar id) = 
   case lookupSubst id mapping of
   Just _  -> sub -- already mapped to a constant
-  Nothing -> SubstM (add mapping id (TcActor (Fresh (maxId + 1)))) (maxId + 1)
+  Nothing -> SubstM (add mapping id (TcActor (Fresh (maxId + 1) $ "#"++show (maxId + 1)))) (maxId + 1)
 freshSubstActor sub                        _          = sub
 
 
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
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 module Language.Java.Paragon.TypeCheck.Monad 
     (
      check, checkM, ignore, orElse, maybeM,
@@ -10,7 +11,7 @@
      lookupFieldT,
      lookupMethod, lookupMethodT,
      lookupConstr, 
-     lookupLockArity, 
+     lookupLock, 
      lookupExn, registerExn, registerExns,
 
      extendLockEnv,
@@ -29,12 +30,14 @@
      activateExns, deactivateExn,
      getExnState, mergeActiveExnStates, useExnState,
 
+     getCurrentPC,
+
      getCurrentLockState, applyLockMods,
      openLock, closeLock,
 
      newMetaPolVar,
 
-     constraint, constraint_, constraintLS,
+     constraint, constraintPC, constraintLS,
      exnConsistent,
 
      extendTypeMapP, extendTypeMapT, lookupPkgTypeMap,
@@ -47,7 +50,8 @@
      getReadPolicy, getWritePolicy, getLockPolicy,
      getParamPolicy, getReturnPolicy,
 
-     fromSrcType, (<:),
+     --fromSrcType, 
+                       (<:),
 
      evalPolicy, evalPolicyExp,
      evalLock, evalActor,
@@ -63,6 +67,7 @@
 
 import Language.Java.Paragon.Syntax
 import Language.Java.Paragon.Pretty
+import Language.Java.Paragon.Verbosity
 
 --import Language.Java.Paragon.TypeCheck.Monad.TcBase
 import Language.Java.Paragon.TypeCheck.Monad.TcCont
@@ -86,9 +91,11 @@
 import Data.IORef
 import Data.List (union, intersperse)
 
-debug str = liftIO $ putStrLn $ "DEBUG: " ++ str
+debug str = liftIO $ finePrint $ "DEBUG: " ++ str
+-- debug _ = return ()
 debugTc = liftCont . debug
 
+
 --------------------------------------------
 --                                        --
 --      Monad-independent helpers         --
@@ -188,13 +195,16 @@
                   _  -> do
                     -- There's more, so the variable is
                     -- being dereferenced
-                    let mTyTm = lookupTypeOfT ty tm
-                    case mTyTm of
-                      Just tyTm -> return (Just tyTm, ty, p, is)
-                      Nothing -> fail $ "Trying to dereference variable "
-                                      ++ prettyPrint i ++
-                                      " but its type " ++ prettyPrint ty ++
-                                      " is not a (known) object type"
+                    let eTyTm = lookupTypeOfT ty tm
+                    case eTyTm of
+                      Right tyTm -> return (Just tyTm, ty, p, is)
+                      Left Nothing -> 
+                          fail $ "Trying to dereference variable "
+                                   ++ prettyPrint i ++
+                                   " but its type " ++ prettyPrint ty ++
+                                   " is not a (known) object type"
+                      Left (Just err) -> fail err
+
   case mNewTm of
     Nothing    -> return (ty, pol) -- We're done
     Just newTm -> aux newTm ty pol rest -- Keep traversing the chain
@@ -210,11 +220,12 @@
                    _ -> do -- There's more, so the field is being dereferenced
                      baseTm <- liftCont getTypeMap
                      case lookupTypeOfT typ baseTm of
-                       Just tyTm -> return $ (Just tyTm, typ, p)
-                       Nothing -> fail $ "Trying to dereference variable "
-                                      ++ prettyPrint i ++
-                                      " but its type " ++ prettyPrint typ ++
-                                      " is not a (known) object type"
+                       Right tyTm -> return $ (Just tyTm, typ, p)
+                       Left Nothing -> fail $ "Trying to dereference variable "
+                                                   ++ prettyPrint i ++
+                                                   " but its type " ++ prettyPrint typ ++
+                                                   " is not a (known) object type"
+                       Left (Just err) -> fail err
                Nothing -> 
                    case Map.lookup i (locks tm) of
                      Just (LSig pol ar) -> do
@@ -248,19 +259,21 @@
       <- do varMap <- vars <$> getEnv
             case Map.lookup i varMap of
               Just (VSig ty p _ _) -> do
-                let mTyTm = lookupTypeOfT ty tm
-                case mTyTm of
+                -- debugTc $ "Type found: " ++ prettyPrint ty
+                let eTyTm = lookupTypeOfT ty tm
+                case eTyTm of
                   -- We found the variable, and it
                   -- has an object type
-                  Just tyTm -> return (Just ty, tyTm, p, is, False)
+                  Right tyTm -> return (Just ty, tyTm, p, is, False)
                   -- We found the variable, but its
                   -- type is not derefereceable, or
                   -- we don't know about it at all
-                  Nothing -> fail $ "Trying to dereference variable " 
-                                      ++ prettyPrint nam ++
-                                      " but its type "
-                                      ++ prettyPrint ty ++
-                                      " is not a (known) object type"
+                  Left Nothing -> fail $ "Trying to dereference variable " 
+                                          ++ prettyPrint (Name () (init n)) ++
+                                          " but its type "
+                                          ++ prettyPrint ty ++
+                                          " is not a (known) object type"
+                  Left (Just err) -> fail err
               Nothing -> return (Nothing,tm,bottom,n,True)
   aux mTy newTm allowPkgT pol rest ts
 
@@ -296,12 +309,12 @@
                  -- field exists, so find its related typemap
                  baseTm <- liftCont getTypeMap
                  case lookupTypeOfT typ baseTm of
-                   Just newTm -> return $ (Just typ, newTm, pol, False)
-                   Nothing    -> fail $ "Trying to dereference field "
-                                      ++ prettyPrint i ++
-                                      maybe "" (\ty -> " of class " ++ prettyPrint ty) mTy
-                                      ++ " but its type " ++ prettyPrint typ ++
-                                      " is not a (known) object type"
+                   Right newTm  -> return $ (Just typ, newTm, pol, False)
+                   Left Nothing -> fail $ "Trying to dereference field "
+                                           ++ prettyPrint i ++
+                                           maybe "" (\ty -> " of class " ++ prettyPrint ty) mTy
+                                           ++ " but its type " ++ prettyPrint typ ++
+                                           " is not a (known) object type"
                Nothing -> 
                    if allowPkgT then
                     case Map.lookup i (pkgsAndTypes tm) of
@@ -336,10 +349,11 @@
 lookupFieldT :: TcType -> Ident () -> Tc r VarFieldSig
 lookupFieldT typ i = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
-  mATm <- lookupTypeOfT typ <$> liftCont getTypeMap
-  case mATm of
-    Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ
-    Just aTm -> 
+  eATm <- lookupTypeOfT typ <$> liftCont getTypeMap
+  case eATm of
+    Left (Just err) -> fail err 
+    Left Nothing    -> fail $ "Unknown reference type: " ++ prettyPrint typ
+    Right aTm -> 
       case Map.lookup i (fields aTm) of
         Just vti -> return vti
         Nothing -> fail $ "Class " ++ prettyPrint typ
@@ -348,10 +362,11 @@
 lookupMethodT :: TcType -> Ident () -> [TcType] -> Tc r ([TypeParam ()], MethodSig)
 lookupMethodT typ i pts = do
   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ
-  mATm <- lookupTypeOfT typ <$> liftCont getTypeMap
-  case mATm of
-    Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ
-    Just aTm -> 
+  eATm <- lookupTypeOfT typ <$> liftCont getTypeMap
+  case eATm of
+    Left (Just err) -> fail err 
+    Left Nothing    -> fail $ "Unknown reference type: " ++ prettyPrint typ
+    Right aTm -> 
       case Map.lookup (i,pts) (methods aTm) of
         Just pmti -> return pmti
         Nothing -> fail $ "Class " ++ prettyPrint typ
@@ -359,22 +374,24 @@
 
 lookupConstr :: TcClassType -> [TcType] -> Tc r ([TypeParam ()], ConstrSig)
 lookupConstr ctyp pts = do
-  mATm <- lookupTypeOfT (clsTypeToType ctyp) <$> liftCont getTypeMap
-  case mATm of
-    Nothing -> fail $ "Unknown class type: " ++ prettyPrint ctyp
-    Just aTm -> 
+  eATm <- lookupTypeOfT (clsTypeToType ctyp) <$> liftCont getTypeMap
+  case eATm of
+    Left (Just err) -> fail err 
+    Left Nothing    -> fail $ "Unknown class type: " ++ prettyPrint ctyp
+    Right aTm -> 
       case Map.lookup pts (constrs aTm) of
         Just pcti -> return pcti
         Nothing -> fail $ "Class " ++ prettyPrint ctyp
                         ++ " does not have a constructor matching argument types "
                         ++ "(" ++ concat (intersperse ", " (map prettyPrint pts)) ++ ")"
 
-lookupLockArity :: Name () -> Tc r Int
-lookupLockArity n = do
+lookupLock :: Name () -> Tc r LockSig
+lookupLock n = do
   tm <- liftCont getTypeMap
+  -- debugTc $ show tm
   case lookupNamed locks n tm of
     Nothing -> fail $ "Unknown lock: " ++ prettyPrint n
-    Just lsig -> return $ lArity lsig
+    Just lsig -> return lsig
 
 lookupExn :: TcType -> Tc r (TcPolicy, TcPolicy)
 lookupExn tyX = do
@@ -398,32 +415,38 @@
 extendLockEnv locks = withEnv $ \env -> 
                         env { lockstate = lockstate env `union` locks }
 
-getBranchPC :: Entity -> Tc r TcPolicy
+getBranchPC :: Entity -> Tc r [(TcPolicy, String)]
 getBranchPC e = do env <- getEnv
                    -- debugTc $ "Env: " ++ show env
                    return $ branchPC (Just e) env
 
-getBranchPC_ :: Tc r TcPolicy
+getBranchPC_ :: Tc r [(TcPolicy, String)]
 getBranchPC_ = do env <- getEnv
                   return $ branchPC Nothing env
 
-extendBranchPC :: TcPolicy -> Tc r a -> Tc r a
-extendBranchPC = withEnv . joinBranchPC
+extendBranchPC :: TcPolicy -> String -> Tc r a -> Tc r a
+extendBranchPC p str = withEnv $ joinBranchPC p str
 
 addBranchPCList :: [Ident ()] -> Tc r a -> Tc r a
 addBranchPCList is =
     withEnv $ \env ->
         let (bm, def) = branchPCE env
-            newBm = foldl (\m i -> Map.insert (VarEntity (Name () [i])) bottom m) bm is
+            newBm = foldl (\m i -> Map.insert (VarEntity (Name () [i])) [] m) bm is
         in env { branchPCE = (newBm, def) }
 
-addBranchPC :: Entity -> TcPolicy -> Tc r a -> Tc r a
-addBranchPC ent pol = 
+addBranchPC :: Entity -> Tc r a -> Tc r a
+addBranchPC ent = 
     withEnv $ \env -> 
         let (bm, def) = branchPCE env
-            newBm = Map.insert ent pol bm
+            newBm = Map.insert ent [] bm
         in env { branchPCE = (newBm, def) }
 
+getCurrentPC :: Entity -> Tc r TcPolicy
+getCurrentPC ent = do
+  bpcs <- fst . unzip <$> getBranchPC ent
+  epcs <- fst . unzip <$> getExnPC
+  return $ foldl join bottom (bpcs ++ epcs)
+
 {-- Tying the knot for member policies
 setFieldPol :: Ident -> TcPolicy -> Tc r ()
 setFieldPol i pF = do
@@ -477,7 +500,7 @@
 
 newActorId :: Ident () -> Tc r ActorId
 newActorId i = do 
-  aid <- liftCont freshActorId
+  aid <- liftCont $ freshActorId (prettyPrint i)
   newActorIdWith i aid
   return aid
 
@@ -488,8 +511,10 @@
   return aid
 
 
-freshActorId, aliasActorId :: TcCont r ActorId
-freshActorId = (liftIO . newFresh) =<< getUniqRef
+freshActorId :: String -> TcCont r ActorId
+freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef
+
+aliasActorId :: TcCont r ActorId
 aliasActorId = (liftIO . newAlias) =<< getUniqRef
   
 
@@ -503,7 +528,7 @@
 
 -- Exception tracking
 
-getExnPC :: Tc r TcPolicy
+getExnPC :: Tc r [(TcPolicy, String)]
 getExnPC = exnPC <$> getState
 
 throwExn :: ExnType -> TcPolicy -> Tc r ()
@@ -583,19 +608,20 @@
 --       Working with constraints         --
 --------------------------------------------
 
-constraint :: [TcLock] -> TcPolicy -> TcPolicy -> Tc r ()
-constraint ls p1 p2 = do -- addConstraint $ LRT ls p1 p2
+constraint :: [TcLock] -> TcPolicy -> TcPolicy -> String -> Tc r ()
+constraint ls p1 p2 str = do -- addConstraint $ LRT ls p1 p2
   g <- getGlobalLockProps
   case lrt (g `recmeet` rls) p1 p2 of
     Left b -> do
-      --debugTc $ "constraint: p1: " ++ show p1
-      --debugTc $ "constraint: p2: " ++ show p2
-      check b $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)
+--      debugTc $ "constraint: p1: " ++ show p1
+--      debugTc $ "constraint: p2: " ++ show p2
+      check b str {-
+                $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)
                  "\n* p = " ++ prettyPrint p1 ++
                  "\n* q = " ++ prettyPrint p2 ++
                  "\nin the presence of lock state {" ++
-                   concat (intersperse ", " (map prettyPrint ls)) ++ "}"
-    Right c -> addConstraint c
+                   concat (intersperse ", " (map prettyPrint ls)) ++ "}" -}
+    Right c -> addConstraint c str
   where rls = locksToRec ls
 
 getGlobalLockProps :: Tc r TcPolicyRec
@@ -604,24 +630,48 @@
 locksToRec :: [TcLock] -> TcPolicyRec
 locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls))
 
-constraint_, constraintLS :: TcPolicy -> TcPolicy -> Tc r ()
-constraint_ = constraint []
-
-constraintLS p1 p2 = do
+constraintLS :: TcPolicy -> TcPolicy -> String -> Tc r ()
+constraintLS p1 p2 str = do
   l <- getCurrentLockState
-  constraint l p1 p2
+  withErrCtxtTc ("In the context of lock state: " ++ prettyPrint l ++ "\n") $
+    constraint l p1 p2 str
 
-exnConsistent :: TcType -> ExnSig -> Tc r ()
-exnConsistent exnTy (ExnSig rX wX _) = do
+constraintPC :: [(TcPolicy, String)] -> TcPolicy -> (TcPolicy -> String -> String) -> Tc r ()
+constraintPC bpcs pW msgf = mapM_ (uncurry $ constraintPC_ pW msgf) bpcs
+    where constraintPC_ :: TcPolicy -> (TcPolicy -> String -> String) 
+                        -> TcPolicy -> String -> Tc r ()
+          -- Don't take lock state into account
+          constraintPC_ pW msgf pPC src = constraint [] pPC pW (msgf pPC src)
+  
+
+
+exnConsistent :: Either (Name ()) (ClassType ()) -> TcType -> ExnSig -> Tc r ()
+exnConsistent caller exnTy (ExnSig rX wX _) = do
     exnMap <- exnsE <$> getEnv
     --debugTc $ "Using exnMap: " ++ show exnMap
+    let (callerName, callerSort) = 
+            case caller of
+              Left n   -> (prettyPrint n , "method"     )
+              Right ct -> (prettyPrint ct, "constructor")
     case Map.lookup exnTy exnMap of
       Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy)
       Just (rE, wE) -> do
-        constraint_ wX wE
-        constraint_ rE rX
+        constraint [] wX wE $
+                    "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?
+                    "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 " ++ 
+                    prettyPrint rE
 
 
+
 --------------------------------------------
 --       Working with typemaps            --
 --------------------------------------------
@@ -653,9 +703,10 @@
 
 lookupPkgTypeMap :: [Ident ()] -> TcCont r TypeMap
 lookupPkgTypeMap is = do
-  mTm <- lookupTypeOfN (Name () is) <$> getTypeMap
-  maybe (fail $ "Unknown package: " ++ prettyPrint (Name () is))
-    return mTm
+  eTm <- lookupTypeOfN (Name () is) <$> getTypeMap
+  case eTm of
+    Right tm -> return tm
+    Left _   -> fail $ "Unknown package: " ++ prettyPrint (Name () is)
 
 -------------------------------------------------------------------
 -- Evaluating types
@@ -677,18 +728,64 @@
 evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct
 
 evalSrcClsType :: ClassType () -> TcCont r TcClassType
-evalSrcClsType (ClassType _ iArgs) = 
-    TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs
+evalSrcClsType ct@(ClassType _ iArgs) = do
+  debug $ "Evaluating class type: " ++ show ct
+  baseTm <- getTypeMap
+  debug $ "Current type map: " ++ show baseTm
+  TcClassT <$> aux baseTm [] iArgs
+
+      where aux :: TypeMap                            -- Typemap of outer type (or top-level)
+                -> [(Ident (), [TcTypeArg])]          -- Accumulated type (reversed)
+                -> [(Ident (), [TypeArgument ()])]    -- Type to traverse
+                -> TcCont r [(Ident (), [TcTypeArg])] -- Result (re-reversed)
+            aux _ accTy [] = return $ reverse accTy
+            aux tm accTy ((i,tas):rest) = do
+                 debug $ "Looking up type: " ++ show i
+                 debug $ "Types field: " ++ show (types tm)
+                 (newTm, tArgs) <- 
+                     case Map.lookup i (types tm) of
+                       Just (pars, tsig) -> do
+                         debug $ "Type found"
+                         tArgs <- mapM (uncurry evalSrcTypeArg) (zip pars tas)
+                         debug "Type arguments evaluated"
+                         return (instantiate (zip pars tArgs) (tMembers tsig), tArgs)
+                       Nothing -> case Map.lookup i (packages tm) of
+                                    Just tm -> do check (null tas) $ 
+                                                            "Packages cannot have type arguments"
+                                                  return (tm, [])
+                                    Nothing -> fail $ "Unknown type: " ++ prettyPrint i
+                 debug $ "Rest of type to evaluate: " ++ show rest
+                 aux newTm ((i,tArgs):accTy) rest
+
+--    TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs
       
-evalSrcTypeArg :: TypeArgument () -> TcCont r TcTypeArg
-evalSrcTypeArg (ActualArg _ a) = evalSrcNWTypeArg a
-evalSrcTypeArg _ = fail "evalSrcTypeArg: Wildcards not yet supported"
+evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcCont r TcTypeArg
+evalSrcTypeArg tp (ActualArg _ a) = evalSrcNWTypeArg tp a
+evalSrcTypeArg _ _ = fail "evalSrcTypeArg: Wildcards not yet supported"
 
-evalSrcNWTypeArg :: NonWildTypeArgument () -> TcCont r TcTypeArg
+evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcCont r TcTypeArg
+-- Types may be names or types -- TODO: Check bounds
+evalSrcNWTypeArg tp@(TypeParam {}) (ActualName _ (Name _ is)) = do
+    TcActualType . TcClsRefT <$> evalSrcClsType (ClassType () $ map (,[]) is)
+evalSrcNWTypeArg (TypeParam {}) (ActualType _ rt) = TcActualType <$> evalSrcRefType rt
+-- 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
+-- Lock states must be locks
+evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls
+
+evalSrcNWTypeArg tp nwta = 
+    fail $ "Trying to instantiate type parameter " ++ prettyPrint tp ++
+           " with incompatible type argument " ++ prettyPrint nwta
+
+{-
 evalSrcNWTypeArg (ActualType   _ rt) = TcActualType <$> evalSrcRefType rt
 evalSrcNWTypeArg (ActualPolicy _ p)  = TcActualPolicy <$> evalPolicy p
 evalSrcNWTypeArg (ActualActor  _ n)  = TcActualActor <$> evalActorId n
 evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls
+-}
 
 evalPolicy :: Exp () -> TcCont r TcPolicy
 evalPolicy e = case e of
@@ -762,7 +859,7 @@
     Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n
 getActor (ActorTypeVar _ i) = return $ ActorTPVar i
 
--- From source
+{-- From source
 
 fromSrcType :: TypeMap -> Type () -> TcType
 fromSrcType tm (PrimType _ pt) = TcPrimT pt
@@ -826,6 +923,7 @@
 fromSrcAtom :: TypeMap -> Atom () -> TcAtom
 fromSrcAtom tm (Atom _ n as) = TcAtom n $ map (fromSrcActor tm) as
 
+-}
 
 -------------------------------------------------------------------------------------      
 getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcCont r TcPolicy
diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs
--- a/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs
@@ -27,9 +27,9 @@
 -- and a writer for constraints
 
 newtype Tc r a =
-    Tc (TcEnv -> TcState -> TcCont r (a, TcState, [Constraint]))
+    Tc (TcEnv -> TcState -> TcCont r (a, TcState, [ConstraintWMsg]))
 
-runTc :: TcEnv -> TcState -> Tc r a -> TcCont r (a, [Constraint])
+runTc :: TcEnv -> TcState -> Tc r a -> TcCont r (a, [ConstraintWMsg])
 runTc env state (Tc f) = do
   (a,_,cs) <- f env state
   return (a, cs)
@@ -93,6 +93,11 @@
                   a <- tcba
                   return (a, s, [])
 
+withErrCtxtTc :: String -> Tc r a -> Tc r a
+withErrCtxtTc str (Tc f) = Tc $ \e s -> withErrCtxt str (f e s)
+                             
+
+
 -- Running in parallel
 infix 1 |||
 (|||) :: Tc r a -> Tc r b -> Tc r (a,b)
@@ -135,6 +140,6 @@
 
 -- Constraints
 
-addConstraint :: Constraint -> Tc r ()
-addConstraint c = Tc (\_ s -> return ((), s, [c]))
+addConstraint :: Constraint -> String -> Tc r ()
+addConstraint c str = Tc (\_ s -> return ((), s, [(c,str)]))
 
diff --git a/src/Language/Java/Paragon/TypeCheck/TcEnv.hs b/src/Language/Java/Paragon/TypeCheck/TcEnv.hs
--- a/src/Language/Java/Paragon/TypeCheck/TcEnv.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TcEnv.hs
@@ -2,6 +2,7 @@
 module Language.Java.Paragon.TypeCheck.TcEnv where
 
 import Language.Java.Paragon.Syntax
+import Language.Java.Paragon.Pretty
 
 import Language.Java.Paragon.TypeCheck.Actors
 import Language.Java.Paragon.TypeCheck.Policy
@@ -19,6 +20,8 @@
 import Data.Generics (Data(..),Typeable(..))
 #endif
 
+import Debug.Trace
+
 type Map = Map.Map
 
 data TypeMap = TypeMap {
@@ -70,20 +73,21 @@
       lockstate :: [TcLock],
       returnI   :: Maybe (TcType, TcPolicy),
       exnsE     :: Map TcType (TcPolicy, TcPolicy),
-      branchPCE :: (Map Entity TcPolicy, TcPolicy)
+      branchPCE :: (Map Entity [(TcPolicy, String)], [(TcPolicy, String)])
     }
   deriving (Show, Data, Typeable)
 
 -- Env to use when typechecking expressions not inside method
 -- bodies, e.g. in field initializers and policy modifiers
-simpleEnv :: TcPolicy -> TcEnv
-simpleEnv brPol = TcEnv {
-                    vars = Map.empty,
-                    lockstate = [],
-                    returnI = Nothing, -- error "No returns in simple env",
-                    exnsE = Map.empty,
-                    branchPCE = (Map.empty, brPol)
-                  }
+simpleEnv :: TcPolicy -> String -> TcEnv
+simpleEnv brPol str = 
+    TcEnv {
+      vars = Map.empty,
+      lockstate = [],
+      returnI = Nothing, -- error "No returns in simple env",
+      exnsE = Map.empty,
+      branchPCE = (Map.empty, [(brPol,str)])
+    }
 
 data Entity = VarEntity (Name ())
             | ThisFieldEntity (Ident ())
@@ -174,10 +178,10 @@
           instT rt = rt
 
           instA :: ActorId -> ActorId
-{-          instA av@(ActorTPVar i) =
+          instA av@(ActorTPVar i) =
               case lookup i as of
                 Just a -> a
-                Nothing -> av -}
+                Nothing -> av
           instA a = a
 
           instP :: TcPolicy -> TcPolicy
@@ -208,66 +212,79 @@
 --    Working with the branchPC     --
 --------------------------------------
 
-branchPC :: Maybe Entity -> TcEnv -> TcPolicy
+branchPC :: Maybe Entity -> TcEnv -> [(TcPolicy, String)]
 branchPC men (TcEnv { branchPCE = (bm, def) }) = 
     flip (maybe def) men $ \en ->
         maybe def id (Map.lookup en bm)
 
-joinBranchPC :: TcPolicy -> TcEnv -> TcEnv
-joinBranchPC p env = let (bm, def) = branchPCE env
-                      in env { branchPCE = (Map.map (`join` p) bm, def `join` p) }
+joinBranchPC :: TcPolicy -> String -> TcEnv -> TcEnv
+joinBranchPC p str env = let (bm, def) = branchPCE env
+                         in env { branchPCE = (Map.map ((p, str):) bm, (p,str):def) }
 
 --------------------------------------
 --    Working with the lookups      --
 --------------------------------------
 
 lookupNamed :: (TypeMap -> Map (Ident ()) a) -> Name () -> TypeMap -> Maybe a
-lookupNamed recf (Name _ is) tm =
-   let mActualTm = lookupTypeOfN (Name () $ init is) tm
-   in maybe Nothing (Map.lookup (last is) . recf) mActualTm
+lookupNamed recf nam@(Name _ is) tm =
+   case lookupTypeOfN (Name () $ init is) tm of
+     Right actualTm -> Map.lookup (last is) (recf actualTm)
+     Left err -> Nothing
 
 lookupNamedMethod :: Name () -> [TcType] -> TypeMap -> Maybe ([TypeParam ()],MethodSig)
 lookupNamedMethod (Name _ is) ts tm = 
-    let mActualTm = lookupTypeOfN (Name () $ init is) tm
-    in maybe Nothing (Map.lookup (last is, ts) . methods) mActualTm
+    case lookupTypeOfN (Name () $ init is) tm of
+      Right actualTm -> Map.lookup (last is, ts) (methods actualTm)
+      Left err -> Nothing
 
 pkgsAndTypes :: TypeMap -> Map (Ident ()) TypeMap
 pkgsAndTypes tm = Map.union (packages tm)
                     -- disregard type parameters
                     (Map.map (tMembers . snd) $ types tm)
 
-lookupTypeOfN :: Name () -> TypeMap -> Maybe TypeMap
-lookupTypeOfN (Name _ is) tm = aux is (Just tm) tm
-    where aux :: [Ident ()] -> Maybe TypeMap -> TypeMap -> Maybe TypeMap
-          aux _ Nothing _ = Nothing
-          aux [] mtm _ = mtm
-          aux (i:is) (Just tm) baseTm =
+lookupTypeOfN :: Name () -> TypeMap -> Either (Maybe String) TypeMap
+lookupTypeOfN nam@(Name _ is) tm = aux is (Right tm) tm
+    where aux :: [Ident ()] 
+              -> Either (Maybe String) TypeMap 
+              -> TypeMap 
+              -> Either (Maybe String) TypeMap
+          aux _ err@(Left _) _ = err
+          aux [] etm _ = etm
+          aux (i:is) (Right tm) baseTm =
             let mNewTm = 
                  case Map.lookup i (fields tm) of
                    Just (VSig typ _ _ _) -> lookupTypeOfT typ baseTm
                    Nothing -> case Map.lookup i (pkgsAndTypes tm) of
-                                Just aTm -> Just aTm
-                                Nothing -> Nothing -- error "lookupTypeOfN: No such name"
+                                Just aTm -> Right aTm
+                                Nothing -> Left Nothing -- $ "Unknown name: " ++ prettyPrint nam
             in aux is mNewTm baseTm
 
-lookupTypeOfT :: TcType -> TypeMap -> Maybe TypeMap
+lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) TypeMap
 lookupTypeOfT (TcRefT refT) = lookupTypeOfT' refT
-lookupTypeOfT t = const Nothing -- error $ "lookupTypeOfT: Unexpected type: " ++ show t
+lookupTypeOfT t = const $ Left Nothing
 
-lookupTypeOfT' :: TcRefType -> TypeMap -> Maybe TypeMap
-lookupTypeOfT' (TcClsRefT (TcClassT iargs)) tm = aux iargs (Just tm)
-    where aux :: [(Ident (), [TcTypeArg])] -> Maybe TypeMap -> Maybe TypeMap
-          aux _ Nothing = Nothing
-          aux [] mtm = mtm
-          aux ((i, args):iargs) (Just tm) =
-              let mNewTm =
+lookupTypeOfT' :: TcRefType -> TypeMap -> Either (Maybe String) TypeMap
+lookupTypeOfT' (TcClsRefT (TcClassT iargs)) tm = aux iargs (Right tm)
+    where aux :: [(Ident (), [TcTypeArg])] 
+              -> Either (Maybe String) TypeMap 
+              -> Either (Maybe String) TypeMap
+          aux _ err@(Left _) = err
+          aux [] etm = etm
+          aux ((i, args):iargs) (Right tm) = -- traceShow args $
+              let eNewTm =
                    case Map.lookup i (types tm) of
-                     Just (pars, tsig) -> Just $ instantiate (zip pars args) (tMembers tsig)
+                     Just (pars, tsig) -> 
+                         if length pars == length args
+                         then Right $ instantiate (zip pars args) (tMembers tsig)
+                         else Left $ Just $ 
+                                  "Wrong number of type arguments in class type.\n" ++
+                                  "Type " ++ prettyPrint i ++ " expects " ++ show (length pars) ++
+                                  " arguments but has been given " ++ show (length args)
                      Nothing -> 
                          case Map.lookup i (packages tm) of
-                           Just tm -> Just tm
-                           Nothing -> Nothing -- error $ "lookupTypeOfT: No such type: " ++ show i
-              in aux iargs mNewTm
+                           Just tm -> Right tm
+                           Nothing -> Left Nothing -- $ "Unknown type : " ++ prettyPrint i
+              in aux iargs eNewTm
 
-lookupTypeOfT' (TcArrayT ty pol) _ = Just $ hardCodedArrayTM ty pol
+lookupTypeOfT' (TcArrayT ty pol) _ = Right $ hardCodedArrayTM ty pol
 -- TODO: Insert array support
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
@@ -38,7 +38,8 @@
 --    Checking expressions       --
 -----------------------------------
 
-debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str
+--debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str
+debugTc _ = return ()
 
 tcExp :: Exp () -> Tc r (TcType, TcPolicy)
 
@@ -76,28 +77,42 @@
   return (ty, pol)
   
 -- Rule VARASS/FIELDASS
-tcExp (Assign _ lhs op rhs) = do
-
-  (tyV, pV, mtyO, mpO, mEnt, mN) <- 
+tcExp ex@(Assign _ lhs op rhs) = do
+  debugTc $ prettyPrint ex
+  (tyV, pV, mtyO, mEnt, mN) <- 
     case lhs of
       NameLhs _ n ->  do
           let (mo,f) = splitName n -- TODO: This is bogus      
           case mo of
             Nothing -> do -- VARASS
                 (tyV, pV) <- lookupVar f
-                return (tyV, pV, Nothing, Nothing, Just (varE n), Just n)
+                return (tyV, pV, Nothing, Just (varE n), Just n)
             Just o -> do -- FIELDASS
                 (tyO,pO) <- lookupVar o
                 let (Name _ [i]) = f
                 (VSig tyF pF _ _) <- lookupFieldT tyO i
-                return (tyF, pF, Just tyO, Just pO, Just (varE n), Just n)
+                constraint [] pO pF $ 
+                     "Cannot update field " ++ prettyPrint i ++ " of object " ++
+                     prettyPrint o ++ 
+                     ": policy of field must be no less restrictive than that of the " ++
+                     "object when updating\n" ++
+                     "Object policy: " ++ prettyPrint pO ++ "\n" ++
+                     "Field policy: " ++ prettyPrint pF
+                return (tyF, pF, Just tyO, Just (varE n), Just n)
       FieldLhs _ (PrimaryFieldAccess _ e fi) -> do
             (tyE, pE) <- tcExp e
             (VSig tyF pF _ _) <- lookupFieldT tyE fi
             let eEnt = case e of
                          This _ -> Just $ thisFE fi
                          _ -> Nothing
-            return (tyF, pF, Just tyE, Just pE, eEnt, Nothing)
+            constraint [] pE pF $
+                 "Cannot update field " ++ prettyPrint fi ++ 
+                 " of object resulting from expression " ++ prettyPrint e ++ 
+                 ": policy of field must be no less restrictive than that of the " ++
+                 "object when updating\n" ++
+                 "Object policy: " ++ prettyPrint pE ++ "\n" ++
+                 "Field policy: " ++ prettyPrint pF
+            return (tyF, pF, Just tyE, eEnt, Nothing)
       ArrayLhs _ (ArrayIndex _ arrE iE) -> do
             (tyA, pA) <- tcExp arrE
             case tyA of
@@ -106,8 +121,22 @@
                 check (isIntConvertible tyI) $
                      "Non-integral expression of type " ++ prettyPrint tyI
                        ++ " used as array index expression"
-                constraintLS pI pA
-                return (tyElem, pElem, Just tyA, Just pA, Nothing, Nothing)
+                constraintLS pI pA $
+                             "When assigning into an array, the policy on the index " ++
+                             "expression may be no more restrictive than the policy of " ++
+                             "the array itself\n" ++
+                             "Array: " ++ prettyPrint arrE ++ "\n" ++
+                             "  has policy " ++ prettyPrint pA ++ "\n" ++
+                             "Index: " ++ prettyPrint iE ++ "\n" ++
+                             "  has policy " ++ prettyPrint pI
+                constraint [] pA 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 tyA, Nothing, Nothing)
 
               _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
                            ++ " of type " ++ prettyPrint tyA
@@ -122,17 +151,27 @@
   checkM (liftCont $ tyRhs <: tyV) $ 
              "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV
   -- Check: E[branchPC](n) <= pV
-  bpc <- maybe getBranchPC_ getBranchPC mEnt
-
-  -- debugTc $ "BPC: " ++ prettyPrint bpc
-  constraint_ bpc pV
+  bpcs <- maybe getBranchPC_ getBranchPC mEnt
+  constraintPC bpcs pV $ \p src ->
+      "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check: exnPC(S) <= pV
-  epc <- getExnPC
-  constraint_ epc pV
+  epcs <- getExnPC
+  constraintPC epcs pV $ \p src -> 
+      "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check: pRhs <= pV modulo L
-  constraintLS pRhs pV
+  constraintLS pRhs pV $
+      "Cannot assign result of expression " ++ prettyPrint rhs ++
+      " with policy " ++ prettyPrint pRhs ++
+      " to location " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV
   -- Check: pO <= pV, if pO exists
-  maybeM mpO (\pO -> constraint_ pO pV)
+--  maybeM mpO (\pO -> constraint [] pO pV $
+--           "When changing the state of an object, the policy of the changed field may not " ++
+--             "be less restrictive than the policy of the object\n" ++
+--             "
 
   -- Update actor tracker if applicable
   maybeM (mActorId tyRhs) $ \aid -> do
@@ -156,25 +195,48 @@
   -- END DEBUG
   (tysArgs, psArgs) <- unzip <$> mapM tcExp args
   (tps,genCti) <- lookupConstr tyT tysArgs
-  tArgs <- liftCont $ mapM evalSrcTypeArg tas
+  -- TODO: Check that the arguments in tyT
+  --       match those expected by the type
+  -- TODO: Type argument inference
+  check (length tps == length tas) $
+        "Wrong number of type arguments in instance creation expression.\n" ++
+        "Constructor expects " ++ show (length tps) ++ 
+        " arguments but has been given " ++ show (length tas)
+  tArgs <- liftCont $ mapM (uncurry evalSrcTypeArg) (zip tps tas)
  -- tm <- liftCont getTypeMap
   let cti = instantiate (zip tps tArgs) genCti
   let (CSig psPars pW lExp lMods exns) = cti
 
   -- Check lockstates
   l <- getCurrentLockState
-  check (null (lExp \\ l)) $ "Lockstate too weak"
+  check (null (lExp \\ l)) $ 
+            "Lockstate too weak when calling constructor " ++ prettyPrint ct ++ ":\n" ++ 
+            "Required lock state: " ++ prettyPrint lExp ++ "\n" ++
+            "Current lock state: " ++ prettyPrint l
   -- Check argument constraints
-  mapM_ (uncurry (constraint l)) (zip psArgs psPars)
+  mapM_ (\(arg,argP,parP) -> 
+             constraintLS argP parP $
+                 "Constructor applied to argument with too restrictive policy:\n" ++ 
+                 "Constructor expression: " ++ prettyPrint e ++ "\n" ++
+                 "Argument: " ++ prettyPrint arg ++
+                 "  with policy: " ++ prettyPrint argP ++
+                 "Declared policy bound: " ++ prettyPrint parP
+        ) (zip3 args psArgs psPars)
   -- Check E[branchPC](*) <= pW
-  bpc <- getBranchPC_
-  constraint_ bpc pW
+  bpcs <- getBranchPC_
+  constraintPC bpcs pW $ \p src ->
+       "Constructor " ++ prettyPrint ct ++ " with declared write effect " ++ prettyPrint pW ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check exnPC(S) <= pW
   epc <- getExnPC
-  constraint_ epc pW
+  constraintPC epc pW $ \p src ->
+      "Constructor " ++ prettyPrint ct ++ " 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) exns
+  mapM (uncurry $ exnConsistent (Right ct)) exns
 
   -- Fix outgoing state
   let exns' = map (first ExnType) exns
@@ -188,7 +250,7 @@
 tcExp (Cond _ c e1 e2) = do
   (tyC, pC) <- tcExp c
   checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"
-  extendBranchPC pC $ do
+  extendBranchPC pC ("conditional expression dependent on expression " ++ prettyPrint c) $ do
     ((ty1, p1), (ty2, p2)) <- 
         (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2
     check (ty1 == ty2) $ "Types of branches don't match"
@@ -292,7 +354,11 @@
               (tyE,pE) <- tcExp e
               check (isIntConvertible tyE) $ nonIntErr tyE
               -- Each dimexpr must satisfy the policy of the outer dim
-              constraintLS pE pPrev
+              constraintLS pE pPrev $
+                           "Array dimension expression has too restrictive policy:\n" ++
+                           "Expression: " ++ prettyPrint e ++ "\n" ++
+                           "  with policy: " ++ prettyPrint pE ++ "\n" ++
+                           "Declared policy bound: " ++ prettyPrint pPrev
               pNext <- evalMaybePol mp
               checkDimExprs (pPrev:acc) emps pNext
 
@@ -322,8 +388,8 @@
       check (isIntConvertible tyI) $
             "Non-integral expression of type " ++ prettyPrint tyI
             ++ " used as array index expression"
-      constraintLS pI pA
-      return (tyElem, pElem `join` pA)
+--      constraintLS pI pA $ " " -- Not true: pI just adds to the outgoing level
+      return (tyElem, pElem `join` pA `join` pI)
 
     _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE
                 ++ " of type " ++ prettyPrint tyA
@@ -337,7 +403,12 @@
 tcArrayInit :: TcType -> [TcPolicy] -> ArrayInit () -> Tc r ()
 tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do
   ps <- mapM (tcVarInit baseType pols) inits
-  mapM_ (\p -> constraintLS p pol1) ps
+  mapM_ (\(p,e) -> constraintLS p pol1 $
+                    "Expression in array initializer has too restrictive policy:\n" ++
+                    "Expression: " ++ prettyPrint e ++
+                    "  with policy: " ++ prettyPrint p ++
+                    "Declared policy bound: " ++ prettyPrint pol1
+        ) (zip ps inits)
 tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions"
 
 tcVarInit :: TcType -> [TcPolicy] -> VarInit () -> Tc r TcPolicy
@@ -382,43 +453,63 @@
 
 tcMethodInv :: MethodInvocation () -> Tc r (TcType, TcPolicy)
 tcMethodInv mi = do
-  --debugTc $ "tcMethodInv: " ++ show mi
+  debugTc $ "tcMethodInv: " ++ prettyPrint mi
   mSigORlSig <-
       case mi of 
         MethodCall _ n args -> do
             (tysArgs, psArgs) <- unzip <$> mapM tcExp args
             eML <- lookupMethod n tysArgs
+            debugTc $ show eML
             case eML of
-              Left (pPath,_tps,mti) -> return $ Left (mti, psArgs, pPath)
+              Left (pPath,_tps,mti) -> return $ Left (n,mti,args, psArgs, pPath)
               Right (pPath,lsig) -> return $ Right (n,lsig, pPath, tysArgs, psArgs)
         PrimaryMethodCall _ e tas i args -> do
             (tyE, pE) <- tcExp e
             (tysArgs, psArgs) <- unzip <$> mapM tcExp args
             (tps,genMti) <- lookupMethodT tyE i tysArgs
-            tArgs <- liftCont $ mapM (evalSrcTypeArg . ActualArg ()) tas
+            tArgs <- liftCont $ mapM (uncurry evalSrcTypeArg) $ 
+                                     zip tps (map (ActualArg ()) tas)
             let mti = instantiate (zip tps tArgs) genMti
-            return $ Left (mti, psArgs, pE)
+            return $ Left (Name () [i], mti, args, psArgs, pE)
         _ -> fail $ "tcMethodInv: Unsupported method call"
 
   case mSigORlSig of
     -- This is a method call
-    Left (mti, psArgs, pE) -> do
+    Left (n, mti, args, psArgs, pE) -> do
        let (MSig tyR pR psPars pW lExp lMods exns) = mti
-
+--       debugTc $ "Method call"
        -- Check lockstates
        l <- getCurrentLockState
-       check (null (lExp \\ l)) $ "Lockstate too weak: " ++ "(" ++ show lExp ++ ", " ++ show l ++ ")"
+       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
-       mapM_ (uncurry (constraint l)) (zip psArgs psPars)
+       mapM_ (\(arg,argP,parP) -> 
+                  constraintLS argP parP $
+                      "Method applied to argument with too restrictive policy:\n" ++ 
+                      "Method invocation: " ++ prettyPrint mi ++ "\n" ++
+                      "Argument: " ++ prettyPrint arg ++
+                      "  with policy: " ++ prettyPrint argP ++
+                      "Declared policy bound: " ++ prettyPrint parP
+             ) (zip3 args psArgs psPars)
+--      mapM_ (uncurry (constraint l)) (zip psArgs psPars)
+--       debugTc $ "Arguments checked"
        -- Check E[branchPC](*) <= pW
-       bpc <- getBranchPC_
-       constraint_ bpc pW
+       bpcs <- getBranchPC_
+       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
-       constraint_ epc 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) exns
+       mapM (uncurry $ exnConsistent (Left n)) exns
 
        -- Fix outgoing state
        let exns' = map (first ExnType) exns
@@ -466,7 +557,7 @@
 
 tcAtom :: Atom () -> Tc r TcAtom
 tcAtom (Atom _ n as) = do
-  ar <- lookupLockArity n
+  (LSig _ ar) <- lookupLock n
   check (length as == ar) $ "Arity mismatch in policy"
   tcAs <- mapM tcActor as
   return (TcAtom n tcAs)
diff --git a/src/Language/Java/Paragon/TypeCheck/TcState.hs b/src/Language/Java/Paragon/TypeCheck/TcState.hs
--- a/src/Language/Java/Paragon/TypeCheck/TcState.hs
+++ b/src/Language/Java/Paragon/TypeCheck/TcState.hs
@@ -1,6 +1,8 @@
 module Language.Java.Paragon.TypeCheck.TcState where
 
 import Language.Java.Paragon.Syntax
+import Language.Java.Paragon.Pretty
+import Text.PrettyPrint (text)
 
 import Language.Java.Paragon.TypeCheck.Policy
 import Language.Java.Paragon.TypeCheck.Actors
@@ -105,5 +107,13 @@
   return (ExnPoint st w)
 
 -- This should probably be pre-computed each time the map is updated instead
-exnPC :: TcState -> TcPolicy
-exnPC s = foldl join bottom $ map epWrite $ Map.elems $ exnS s
+exnPC :: TcState -> [(TcPolicy, String)]
+exnPC s = map (\(tyX,ptX) -> (epWrite ptX, errorSrc tyX)) $ Map.assocs $ exnS s
+
+errorSrc :: ExnType -> String
+errorSrc et = "area of influence of " ++
+    case et of
+      ExnBreak -> "a break statement"
+      ExnContinue -> "a continue statement"
+      ExnReturn -> "a return statement"
+      ExnType tX -> "exception " ++ prettyPrint tX
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
@@ -36,7 +36,7 @@
 tcStmt (IfThenElse _ c s1 s2) = do
   (tyC, pC) <- tcExp c
   checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"
-  extendBranchPC pC $ do
+  extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do
     ignore $ (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2
 
 -- Rule IFTHEN
@@ -47,9 +47,9 @@
   s <- getState                  -- Starting state S
   (tyC, pC) <- tcExp c
   check (isBoolConvertible tyC) $ "Cannot convert type to boolean"
-  extendBranchPC pC $
-    addBranchPC breakE bottom $
-    addBranchPC continueE bottom $ 
+  extendBranchPC pC ("loop over condition " ++ prettyPrint c) $
+    addBranchPC breakE $
+    addBranchPC continueE $ 
      do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls))
         -- First iteration of body
         tcStmt sBody
@@ -81,10 +81,11 @@
     check (isBoolConvertible tyC) $ 
               "Test in basic for loop must have a bool-convertible type. \n" ++
               "Found type: " ++ prettyPrint tyC
-    extendBranchPC pC $
-      addBranchPC breakE bottom $
-      addBranchPC continueE bottom $ do
-     do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls))
+    maybe id (\test -> extendBranchPC pC 
+                       ("for loop dependent on condition " ++ prettyPrint test)) mTest $
+      addBranchPC breakE $
+      addBranchPC continueE $ do
+        maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls))
         -- First iteration of body
         tcStmt body
         _ <- maybe (return undefined) (mapM tcExp) mUp
@@ -112,17 +113,13 @@
 
 -- Rule BREAK
 tcStmt (Break _ Nothing) = do
-  bpc <- getBranchPC breakE
-  epc <- getExnPC
-  s <- getState
-  throwExn ExnBreak (bpc `join` epc)
+  pc <- getCurrentPC breakE
+  throwExn ExnBreak pc
 
 -- Rule CONTINUE
 tcStmt (Continue _ Nothing) = do
-  bpc <- getBranchPC continueE
-  epc <- getExnPC
-  s <- getState
-  throwExn ExnContinue (bpc `join` epc)
+  pc <- getCurrentPC continueE
+  throwExn ExnContinue pc
 
 -- Rule RETURNVOID
 tcStmt (Return _ Nothing) = do
@@ -131,10 +128,8 @@
   check (pR == top)   $ "Internal error: tcStmt: " 
                           ++ "void return with non-top return policy should never happen"
 
-  bpc <- getBranchPC returnE
-  epc <- getExnPC
-  s <- getState
-  throwExn ExnReturn (bpc `join` epc)
+  pc <- getCurrentPC returnE
+  throwExn ExnReturn pc
 
 -- Rule RETURN
 tcStmt (Return _ (Just e)) = do
@@ -145,15 +140,23 @@
          "Expecting type: " ++ prettyPrint tyR
   
   -- Check pE <=[L] pR
-  l <- getCurrentLockState
-  constraint l pE pR
+  constraintLS pE pR $
+               "Returned value has too restrictive policy:\n" ++
+               "Return expression: " ++ prettyPrint e ++ "\n" ++
+               "  with policy: " ++ prettyPrint pE ++ "\n" ++
+               "Declared policy bound: " ++ prettyPrint pR               
   -- Check E[branchPC](return) <= pR
-  bpc <- getBranchPC returnE
-  constraint_ bpc pR
+  bpcs <- getBranchPC returnE
+  constraintPC bpcs pR $ \p src ->
+      "Returning from method, visible at policy " ++ prettyPrint pR ++
+      ", not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check exnPC(S) <= pR
   epc <- getExnPC
-  constraint_ epc pR
-
+  constraintPC epc pR $ \p src ->
+      "Returning from method, visible at policy " ++ prettyPrint pR ++
+      ", not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   throwExn ExnReturn pR
 
 -- Rule THROW
@@ -163,14 +166,23 @@
   (rX, wX) <- lookupExn tyX
   -- Check E[branchPC](X) <= E[exns](X)[write]
   bpc <- getBranchPC (exnE tyX)
-  constraint_ bpc wX
+  constraintPC bpc wX $ \p src ->
+      "Exception with write effect " ++ prettyPrint wX ++ 
+      " may not be thrown in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check exnPC(S) <= E[exns](X)[write]
   epc <- getExnPC
-  constraint_ epc wX
+  constraintPC epc wX $ \p src ->
+      "Exception with write effect " ++ prettyPrint wX ++ 
+      " may not be thrown in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check pX <=[L] E[exns](X)[read]
-  l <- getCurrentLockState
-  constraint l pX rX
-
+  constraintLS pX rX $
+               "Thrown value has too restrictive policy:\n" ++
+               "Expression thrown: " ++ prettyPrint eX ++ "\n" ++
+               "  of type: " ++ prettyPrint tyX ++ "\n" ++
+               "  with policy: " ++ prettyPrint pX ++ "\n" ++
+               "Declared exception policy: " ++ prettyPrint rX
   throwExn (ExnType tyX) wX
 
 -- Rule TRYCATCH
@@ -179,9 +191,9 @@
   tyP <- liftCont $ evalSrcType t
   -- TODO check tyP <: "Throwable"
   pR <- liftCont $ getReadPolicy ms -- getParamPolicy i ms
-  pW <- newMetaPolVar             -- \pi, where \pi is fresh
-  addBranchPC (exnE tyP) bottom $ -- E' = E[branchPC{tyP +-> bottom},
-    registerExn tyP pR pW $ do    --        exns{tyP +-> (pR, \pi)}]
+  pW <- newMetaPolVar               -- \pi, where \pi is fresh
+  addBranchPC (exnE tyP) $          -- E' = E[branchPC{tyP +-> bottom},
+    registerExn tyP pR pW $ do      --        exns{tyP +-> (pR, \pi)}]
       tcBlock block
       extendVarEnv i (VSig tyP pR False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}]
         msX <- getExnState (ExnType tyP)
@@ -216,29 +228,37 @@
 -- Rule OPEN
 -- TODO change the list of actor names to a list of expressions (parser, AST, here)
 tcStmt (Open _ (Lock _ n as)) = do
-  arL <- lookupLockArity n
-  (_,pL) <- lookupVar n
+  (LSig pL arL) <- lookupLock n
+  -- (_,pL) <- lookupVar n
   check (length as == arL) $ 
             "Lock " ++ prettyPrint n ++ " expects " ++ show arL 
                     ++ " arguments but has been given " ++ show (length as)
   -- Check pI <=[L] pL
-  l <- getCurrentLockState
   psAs <- map snd <$> mapM lookupActorName as
-  mapM_ (flip (constraint l) pL) psAs
+  mapM_ (\(a,pA) -> constraintLS pA pL $ 
+                      "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+                      " cannot be opened for actor " ++ prettyPrint a ++
+                      " with policy " ++ prettyPrint pA
+        ) (zip as psAs)
   -- Check E[branchPC](L) <= pL
   bpc <- getBranchPC (lockE n)
-  constraint_ bpc pL
+  constraintPC bpc pL $ \p src ->
+      "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check exnPC(S) <= pL
   epc <- getExnPC
-  constraint_ epc pL
-
+  constraintPC epc pL $ \p src ->
+      "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   aids <- mapM tcActorName as
   openLock (TcLock n aids)
 
 -- Rule CLOSE
 tcStmt (Close _ (Lock _ n as)) = do
-  arL <- lookupLockArity n
-  (_,pL) <- lookupVar n
+  (LSig pL arL) <- lookupLock n
+--  (_,pL) <- lookupVar n
 --  LTI arL pL <- lookupLock n
   check (length as == arL) $ 
             "Lock " ++ prettyPrint n ++ " expects " ++ show arL 
@@ -246,23 +266,31 @@
   -- Check pI <=[L] pL
   l <- getCurrentLockState
   psAs <- map snd <$> mapM lookupActorName as
-  mapM_ (flip (constraint l) pL) psAs
+  mapM_ (\(arg,argP) -> constraintLS argP pL $
+                      "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+                      " cannot be closed for actor " ++ prettyPrint arg ++
+                      " with policy " ++ prettyPrint argP
+        ) (zip as psAs)
   -- Check E[branchPC](L) <= pL
   bpc <- getBranchPC (lockE n)
-  constraint_ bpc pL
+  constraintPC bpc pL $ \p src ->
+      "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   -- Check exnPC(S) <= pL
   epc <- getExnPC
-  constraint_ epc pL
-
+  constraintPC epc pL $ \p src ->
+      "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+      " not allowed in " ++ src ++
+      " with write effect bound " ++ prettyPrint p
   aids <- mapM tcActorName as
   closeLock (TcLock n aids)
 
 -- Rule OPENIN
 tcStmt (OpenBlock _ (Lock _ n as) block) = do
-  arL <- lookupLockArity n
-  (_,pL) <- lookupVar n
+  LSig pL arL <- lookupLock n
+  -- (_,pL) <- lookupVar n
   --debugTc $ "pL: " ++ prettyPrint n ++ ": " ++ show pL
---  LTI arL pL <- lookupLock n
   check (length as == arL) $ 
             "Lock " ++ prettyPrint n ++ " expects " ++ show arL 
                     ++ " arguments but has been given " ++ show (length as)
@@ -270,7 +298,11 @@
   l <- getCurrentLockState
   psAs <- map snd <$> mapM lookupActorName as
   --debugTc $ "psAs: " ++ show psAs
-  mapM_ (flip (constraint l) pL) psAs
+  mapM_ (\(arg,argP) -> constraintLS argP pL $
+                      "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++
+                      " cannot be opened for actor " ++ prettyPrint arg ++
+                      " with policy " ++ prettyPrint argP
+        ) (zip as psAs)
 
   aids <- mapM tcActorName as
   extendLockEnv [TcLock n aids] $
@@ -325,7 +357,7 @@
            then actorIdT <$> newActorId i
            else return tyV
   extendVarEnv i (VSig tyV' pV False fin) $ do
-  addBranchPC (varE (Name () [i])) bottom $ do
+  addBranchPC (varE (Name () [i])) $ do
     tcLocalVars pV tyV fin vds cont    
 
 -- Rule LOCALVARINIT (Exp)
@@ -333,14 +365,17 @@
   (tyE, pE) <- tcExp e
   checkM (liftCont $ tyE <: tyV) $ 
              "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV
-  constraintLS pE pV
+  constraintLS pE pV $
+      "Cannot assign result of expression " ++ prettyPrint e ++
+      " with policy " ++ prettyPrint pE ++
+      " to variable " ++ prettyPrint i ++ " with policy " ++ prettyPrint pV               
   tyV' <- case mActorId tyE of
             Nothing -> return tyV
             Just aid -> do
               newActorIdWith i aid
               return $ actorIdT aid
   extendVarEnv i (VSig tyV' pV False fin) $ do
-  addBranchPC (varE (Name () [i])) bottom $ do
+  addBranchPC (varE (Name () [i])) $ do
     tcLocalVars pV tyV fin vds cont
 
 -- Rule LOCALVARINIT (Array)
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
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP, DeriveDataTypeable, TupleSections, FlexibleInstances #-}
 module Language.Java.Paragon.TypeCheck.Types where
 
 import Language.Java.Paragon.Syntax
@@ -79,6 +79,9 @@
 qualClsType :: [Ident ()] -> TcType
 qualClsType = clsTypeWArg . map (\i -> (i, []))
 
+nameToClsType :: Name () -> TcClassType
+nameToClsType (Name _ is) = TcClassT $ map (\i -> (i,[])) is
+
 stringT :: TcType
 stringT = clsType (Ident () "String")
 
@@ -120,6 +123,12 @@
 isRefType (TcRefT _) = True
 isRefType _ = False
 
+mNameRefType :: TcRefType -> Maybe (Name ())
+mNameRefType (TcClsRefT (TcClassT iargs)) =
+    let (is, as) = unzip iargs
+    in if all null as then Just (Name () is) else Nothing
+mNameRefType _ = Nothing
+
 isNullType (TcRefT (TcClsRefT TcNullT)) = True
 isNullType _ = False
 
@@ -154,7 +163,39 @@
 -------------------------------------------
 -- Type operations
 
+widenConvert :: PrimType () -> [PrimType ()]
+widenConvert pt = case pt of
+   FloatT  _ -> map ($()) [DoubleT]
+   LongT   _ -> map ($()) [DoubleT, FloatT]
+   IntT    _ -> map ($()) [DoubleT, FloatT, LongT]
+   ShortT  _ -> map ($()) [DoubleT, FloatT, LongT, IntT]
+   CharT   _ -> map ($()) [DoubleT, FloatT, LongT, IntT]
+   ByteT   _ -> map ($()) [DoubleT, FloatT, LongT, IntT, ShortT]
+   _         -> []
 
+narrowConvert :: PrimType () -> [PrimType ()]
+narrowConvert pt = case pt of
+   ShortT  _ -> map ($()) [ByteT, CharT]
+   CharT   _ -> map ($()) [ByteT, ShortT]
+   IntT    _ -> map ($()) [ByteT, ShortT, CharT]
+   LongT   _ -> map ($()) [ByteT, ShortT, CharT, IntT]
+   FloatT  _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT]
+   DoubleT _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT, FloatT]
+   _         -> []
+
+widenNarrowConvert :: PrimType () -> [PrimType ()]
+widenNarrowConvert (ByteT _) = [CharT ()]
+widenNarrowConvert _ = []
+
+
+boxConvert :: TcType -> Maybe (TcType)
+boxConvert (TcPrimT pt) = case pt of
+   BooleanT () -> Just $ TcRefT $ TcClsRefT $ TcClassT $ 
+                    map (\s -> (Ident () s,[])) ["java", "lang", "Boolean"  ]
+   _ -> Nothing
+   
+
+
 unboxConvert :: TcType -> Maybe (PrimType ())
 unboxConvert (TcPrimT t) = Just t
 unboxConvert (TcRefT (TcClsRefT (TcClassT is))) =
@@ -168,6 +209,7 @@
       ["java", "lang", "Float"    ] -> Just $ FloatT   ()
       ["java", "lang", "Double"   ] -> Just $ DoubleT  ()
       _ -> Nothing
+unboxConvert _ = Nothing
 
 isNumConvertible :: TcType -> Bool
 isNumConvertible t =
@@ -184,6 +226,7 @@
 isBoolConvertible :: TcType -> Bool
 isBoolConvertible t = unboxConvert t == Just (BooleanT ())
 
+
 unaryNumPromote :: TcType -> Maybe (PrimType ())
 unaryNumPromote t =
     case unboxConvert t of
@@ -208,6 +251,8 @@
 binaryNumPromote_ :: TcType -> TcType -> TcType
 binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2
 
+
+
 ---------------------------------------------
 -- Pretty printing
 
@@ -269,7 +314,7 @@
   pretty (TcVar i) = char '\'' <> pretty i
 
 instance Pretty ActorId where
-  pretty (Fresh k) = text ('#':show k)
+  pretty (Fresh k s) = text s <> text ('#':show k)
   pretty (Alias k) = text ('@':show k)
   pretty (ActorTPVar i) = pretty i
 
@@ -278,6 +323,8 @@
     opt (not $ null aids) (parens (hcat (punctuate (char ',') $ map pretty aids)))
   pretty (TcLockVar i) = pretty i
 
+instance Pretty [TcLock] where
+  pretty ls = brackets $ hcat (punctuate (char ',') $ map pretty ls)
 
 
 ppTypeParams :: Pretty a => [a] -> Doc
diff --git a/src/Language/Java/Paragon/TypeCheck/Uniq.hs b/src/Language/Java/Paragon/TypeCheck/Uniq.hs
--- a/src/Language/Java/Paragon/TypeCheck/Uniq.hs
+++ b/src/Language/Java/Paragon/TypeCheck/Uniq.hs
@@ -20,7 +20,7 @@
 newAlias u = do uniq <- getUniq u
                 return $ Alias uniq
 
-newFresh :: Uniq -> IO ActorId
-newFresh u = do uniq <- getUniq u
-                return $ Fresh uniq
+newFresh :: Uniq -> String -> IO ActorId
+newFresh u str = do uniq <- getUniq u
+                    return $ Fresh uniq str