diff --git a/paragon.cabal b/paragon.cabal
--- a/paragon.cabal
+++ b/paragon.cabal
@@ -1,5 +1,5 @@
 Name:                   paragon
-Version:                0.1.4
+Version:                0.1.5
 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
@@ -10,6 +10,8 @@
 --import Language.Java.Paragon.TypeCheck.Locks
 --import Language.Java.Paragon.TypeCheck.Policy
 --import qualified Language.Java.Paragon.TypeCheck.Types as TP
+import Language.Java.Paragon.Verbosity
+
 import System.FilePath
 import System.Environment
 import System.Directory
@@ -17,13 +19,40 @@
 import qualified Data.Map as DM
 import Data.Maybe
 
+import System.Console.GetOpt
+
 -------------------------------------------------------------------------------------
 main :: IO ()
 main = do
-  [f] <- getArgs
-  compile f
+  (flags, files) <- compilerOpts =<< getArgs
+  when (Version `elem` flags) $ putStrLn versionString
+  mapM_ setVerbosity $ [ k | Verbose k <- flags ]
+  when (not (null files)) $
+    compile flags (head files) -- TODO: Enable multiple files
 
+-- This probably needs to live somewhere else
+data Flag = Verbose Int | Version
+  deriving (Show, Eq)
 
+versionString :: String
+versionString = "Paragon Compiler version: 0.1.5"
+
+options :: [OptDescr Flag]
+options =
+    [ Option ['v'] ["verbose"] 
+                 (OptArg (Verbose . maybe 3 read) "n") 
+                 "Control verbosity (n is 0--4, normal verbosity level is 1, -v alone is equivalent to -v3"
+    , Option ['V','?'] ["version"] 
+                 (NoArg Version)       "Show version number"
+    ]
+
+compilerOpts :: [String] -> IO ([Flag], [String])
+compilerOpts argv =
+    case getOpt RequireOrder options argv of
+      (o,n,[]) -> return (o,n)
+      (_,_,errs) -> ioError (userError (concat errs ++ usageInfo header options))
+          where header = "Usage: parac [OPTION...] files..."
+
 -------------------------------------------------------------------------------------
 --type ErrM = Either String
 
@@ -36,21 +65,16 @@
 debugPrint = putStrLn
 --debugPrint = return ()
 
-compile :: String -> IO ()
-compile filePath = do
+compile :: [Flag] -> String -> IO ()
+compile flags filePath = do
   let (directory,fileName) = splitFileName filePath --relative or absolute path?
   fc <- readFile filePath
   ast <- liftE $ parser compilationUnit fc
-  debugPrint "Parsing complete!"
+  verbosePrint 2 "Parsing complete!"
   ast2 <- typeCheck directory ast
-  debugPrint "Type checking complete!"
+  verbosePrint 2 "Type checking complete!"
   genFiles filePath  ast2
-  debugPrint "File generation complete!"
-    
-
--- import this from TypeCheck.hs
---typeCheck :: CompilationUnit -> IO CompilationUnit
---typeCheck = undefined
+  verbosePrint 2 "File generation complete!"
 
 genFiles :: FilePath -> CompilationUnit -> IO ()
 genFiles filePath ast  = let astC      = compileTransform ast
@@ -64,346 +88,3 @@
                              pi        = prettyPrint astPi
                          in writeFile javaPath java
                             >> writeFile piPath pi    
-{-
-compile2 :: String -> IO ()
-compile2 filePath = do
-  fc <- readFile filePath
-  let east = parser compilationUnit fc
-  case east of
-    Left errs -> print errs
-    Right ast -> do
-      print ast --DEBUG
-      let (directory,fileName) = splitFileName filePath --relative or absolute path?
-      ienv <- createIEnv directory ast
-      putStrLn "IEnv created"
-      mds <- checkTMsigs ienv ast
-      let tmsenv = createTMSEnv ienv mds 
-      putStrLn "Typemethod sigs added"
-      fds <- checkTFs tmsenv ast
-      let tmenv = createTMEnv tmsenv fds
-      putStrLn "Field and method sigs added"
-      tms <- checkTMs tmenv ast
-      let tenv = createTEnv tmenv tms
-      putStrLn "Typemethod bodies added"
-      memds <- checkSigs tenv ast
-      let env = createEnv tenv memds
-      checkBodies env ast 
-
-
--------------------------------------------------------------------------------------
-defaultImportDecls :: [ImportDecl]
-defaultImportDecls = [ ImportDecl False (Name [Ident "paragon"]) True
-                      ,ImportDecl False (Name [Ident "paragon", Ident "util"]) True
-                      ,ImportDecl False (Name [Ident "paragon", Ident "io"]) True]
--------------------------------------------------------------------------------------
-createIEnv :: DirectoryPath -> CompilationUnit -> IO IEnv
-createIEnv currentDir (CompilationUnit _ imps [td])  
-  =  foldM (\env imp -> setIEnvOfImport imp env currentDir) (emptyTM (TP.clsType $ tdIdent td)) imps  
--------------------------------------------------------------------------------------        
------ import Java.*;
-setIEnvOfImport :: ImportDecl -> IEnv -> DirectoryPath -> IO IEnv
-setIEnvOfImport (ImportDecl False (Name idents) True) fileEnv currentDirectory =  
-  do  
-    let relative    = pathOf idents
-    let absoluteDir = currentDirectory ++ [pathSeparator] ++ relative ++ [pathSeparator]
-    names <- getDirectoryContents absoluteDir
-    let classPathsAndName  =  [ (absoluteDir ++ name, takeBaseName name)
-                              | name <- names 
-                              , takeExtension name == ".pi"]
-    let packageNames = idents
-    foldM (\fileEnv' (classPath,className) ->  setIEnvOfCompilationUnit packageNames className fileEnv' classPath) 
-      fileEnv classPathsAndName
-------------------------------
------ import Java.typename;   
-setIEnvOfImport (ImportDecl False (Name idents) False) fileEnv currentDirectory = 
-  do   
-    let relative          = pathOf idents
-    let absoluteFile      = currentDirectory ++ [pathSeparator] ++ relative ++ ".pi"
-    let (Ident className) = last idents
-    let packageNames      =  init idents    
-    setIEnvOfCompilationUnit packageNames className fileEnv absoluteFile  
--------------------------------------------------------------------------------------  
-setIEnvOfCompilationUnit :: [Ident] -> String -> IEnv -> String -> IO IEnv           
-setIEnvOfCompilationUnit [] className env classPath
-  = fetchCompilationUnit className env classPath
-setIEnvOfCompilationUnit (packageName:packageNames) className env classPath
-  = do
-    let oldNestedTypeMap = case DM.lookup packageName (types env) of
-          Just (_,mp) -> mp 
-          _ -> (emptyTM undefined)  -- what is "this" of package ?!!
-    newTypeMap <- setIEnvOfCompilationUnit packageNames className oldNestedTypeMap classPath
-    return env{ types= DM.insert packageName ([],newTypeMap) (types env) }       
-   
--------------------------------------------------------------------------------------
-tdIdent :: TypeDecl -> Ident
-tdIdent (ClassTypeDecl (ClassDecl _ i _ _ _ _)) = i
-tdIdent (InterfaceTypeDecl (InterfaceDecl _ i _ _ _)) = i 
--------------------------------------------------------------------------------------
-getInterface :: String -> IO InterfaceDecl
-getInterface piPath = do
-  fc <- readFile piPath
-  let east = parser compilationUnit fc
-  case east of
-    Left errs -> error $ show errs 
-    Right (CompilationUnit _ _ [(InterfaceTypeDecl interface)]) -> 
-      -- assume there is only one type in each pi file and that is interface
-      return interface
-    _ -> error "\nThere should be only one interface type per Pi file!\n"
--------------------------------------------------------------------------------------      
-getReadPolicy :: [Modifier] -> Policy
-getReadPolicy mods = [pol |(Reads pol) <- mods ]!!0 -- Read Policy? what if no read policy?
--------------------------------------------------------------------------------------
-fetchFieldDecls :: [MemberDecl] -> DM.Map Ident (VTypeInfo Exp Policy Lock)
-fetchFieldDecls memberDecls 
-  = foldl
-    (\m1 (FieldDecl fmods ftype fvardecls)-> 
-      (foldl 
-       (\m2 (VarDecl (VarId fid)  _) -> 
-         DM.insert fid 
-         VTI {
-          varType = (TP.fromSrcType ftype)
-          ,varPol = getReadPolicy fmods 
-          ,varStatic = (Static `elem`  fmods)   
-          ,varFinal = (Final `elem`  fmods)
-          }
-         m2
-       )
-       m1
-       fvardecls
-      )
-    )         
-   (DM.empty) 
-   [f|f@(FieldDecl _ _ _) <- memberDecls] 
--------------------------------------------------------------------------------------
-fetchMethodDecls:: [MemberDecl] -> DM.Map (Ident, [TP.TcTypeExp]) (MTypeInfo Exp Policy Lock)   
-fetchMethodDecls memberDecls
-  = foldl 
-    (\m (MethodDecl mmods mtparams mmaybet mident mformparams mexceptionspecs _)-> 
-      DM.insert 
-      (mident,[TP.fromSrcType pType|(FormalParam _ pType _ _)<-mformparams])  
-      MTI {
-        mRetType = if (isNothing mmaybet) then TP.TcVoidT else TP.fromSrcType$ fromJust mmaybet  
-        , mRetPol = getReadPolicy mmods   
-        , mPars = [getReadPolicy pModifiers
-                  |(FormalParam pModifiers pType pBool pVarDeclId) <- mformparams]
-        , mWrites =  [p| (Writes p) <-mmods ]!!0
-        , mExpects = concat [l| (Expects l) <-mmods ] 
-        , mLMods = ( concat [l| (Closes l) <-mmods], concat [l|(Opens l)<-mmods]) 
-        , mExns =  map (\ (ExceptionSpec emods eExceptionType) -> 
-                         (TP.fromSrcType (RefType eExceptionType), ExnSig {
-                                   exnReads =  getReadPolicy emods
-                                   ,exnWrites = [p| (Writes p) <-emods ]!!0 
-                                   ,exnMods = ( concat [l| (Closes l) <-emods], concat [l|(Opens l)<-emods]) 
-                                   })) 
-                   mexceptionspecs 
-        }
-      m
-    ) 
-    (DM.empty) 
-    [m|m@(MethodDecl mmods _ _ _ _ _ _)<-memberDecls]
--------------------------------------------------------------------------------------
-fetchConstructorDecls :: [MemberDecl]-> DM.Map [TP.TcTypeExp] (CTypeInfo Exp Policy Lock)
-fetchConstructorDecls memberDecls
-  = foldl
-    (\m (ConstructorDecl cmods ctparams cident cformparams cexceptionspecs _)->                       
-      DM.insert 
-      ([TP.fromSrcType pType|(FormalParam _ pType _ _)<-cformparams])
-      CTI {
-        cPars = [getReadPolicy pModifiers|(FormalParam pModifiers pType pBool pVarDeclId)<-cformparams]  
-        ,cWrites = [ p| (Writes p) <-cmods ]!!0
-        ,cExpects = concat [l| (Expects l) <-cmods ]  
-        ,cLMods = (concat [l|(Closes l)<-cmods],concat [l|(Opens l)<-cmods])
-        ,cExns = map (\ (ExceptionSpec emods eExceptionType) -> ( 
-                         (TP.fromSrcType (RefType eExceptionType)) ,ExnSig {
-                                               exnReads =  getReadPolicy emods
-                                               ,exnWrites = [p| (Writes p) <-emods ]!!0 
-                                               ,exnMods = ( concat [l| (Closes l) <-emods], concat [l|(Opens l)<-emods]) 
-                                               })) 
-                 cexceptionspecs
-        }
-      m
-    ) 
-    (DM.empty) 
-    [c|c@(ConstructorDecl _ _ _ _ _ _ )<-memberDecls]
--------------------------------------------------------------------------------------
-fetchLockDecls :: [MemberDecl] -> DM.Map Ident (LTypeInfo Policy)    
-fetchLockDecls memberDecls 
-  = foldl
-    (\m (LockDecl lmods lident lmaybeidents maybelockproperties)-> 
-      DM.insert 
-      lident  
-      LTI {
-        arity = length lmaybeidents 
-        ,lockPol = getReadPolicy  lmods
-        }
-      m
-    ) 
-    (DM.empty) 
-    [l|l@(LockDecl _ _ _ _)<-memberDecls]
--------------------------------------------------------------------------------------    
-fetchPolicyDecls :: [MemberDecl] -> DM.Map Ident Policy
-fetchPolicyDecls memberDecls
-  = foldl
-    (\m (PolicyDecl pmods pident ppolicy)-> DM.insert pident (getReadPolicy pmods) m) 
-    (DM.empty) 
-    [p|p@(PolicyDecl _ _ _)<-memberDecls]
--------------------------------------------------------------------------------------    
-fetchTypemethods :: [MemberDecl] -> DM.Map Ident ([Ident], Block)    
-fetchTypemethods memberDecls
- = foldl
-   (\m (MethodDecl tmmods tmtparams tmmaybet tmident tmformparams _ (MethodBody(Just tmblock)) )-> 
-     DM.insert 
-     tmident 
-     (
-       map (\(FormalParam _ _ _ (VarId vident) ) -> vident) tmformparams  
-                           ,tmblock)         
-     m
-   ) 
-   (DM.empty) 
-   [tm|tm@(MethodDecl tmmods _ _ _ _ _ _ )<-memberDecls
-      ,Typemethod `elem`tmmods]
--------------------------------------------------------------------------------------    
-fetchActors :: [MemberDecl] -> DM.Map Ident Exp
-fetchActors memberDecls
-  = foldl
-    (\m (FieldDecl amods _ vardecls)-> 
-      (foldl
-       (\m' (VarDecl (VarId aid) init) ->
-         let aexp = case init of
-               Just (InitExp a) -> a
-               Nothing -> newActor
-         in DM.insert aid aexp m'
-       )
-       m
-       vardecls
-      )
-    ) 
-    (DM.empty) 
-    [p|p@(FieldDecl _ (PrimType ActorT) _)<-memberDecls] 
--------------------------------------------------------------------------------------        
-fetchCompilationUnit :: String -> IEnv -> String -> IO IEnv
-fetchCompilationUnit compilationUnitName env piPath = do
-  (InterfaceDecl _ id@(Ident compilationUnitName) params _supers (InterfaceBody memberDecls)) <- getInterface piPath 
-  -- Assume there is only one type in each pi file 
-  -- with the specified name
-  -- Assume the superclasses dont matter now
-  let newTypeMap= TypeMap {
-        this= error "Non-local use of 'this'."
-        ,fields = fetchFieldDecls       memberDecls
-        ,methods = fetchMethodDecls     memberDecls
-        ,constrs= fetchConstructorDecls memberDecls          
-        ,locks= fetchLockDecls          memberDecls
-        ,policies= fetchPolicyDecls     memberDecls
-        ,actors= fetchActors            memberDecls
-        ,typemethods= fetchTypemethods  memberDecls         
-        ,types = DM.empty -- inner classes / inner interfaces
-        }
-  return env{ 
-    types = (DM.insert id (params,newTypeMap) (types env)) 
-    }
--------------------------------------------------------------------------------------        
-newActor :: Exp
-newActor = ExpName (Name [Ident "$newActor"])
--------------------------------------------------------------------------------------
--- [ d1 , d2 , x ] -> d1/d2/x  , x can be folder or file (.class)
-pathOf :: [Ident] -> String
-pathOf ((Ident name1):idents) = foldl (\p (Ident str) -> p ++ [pathSeparator]
-                                                         ++ str  ) name1 idents           
--------------------------------------------------------------------------------------
-expand :: TypeMap a b c -> Map Ident (Name, TypeMap a b c)
-expand env = DM.fromList(concat(map (expand' []) (DM.toList(types env))))
- 
-expand' :: [Ident] -> (Ident,([TypeParam],TypeMap a b c)) -> [(Ident,(Name, TypeMap a b c))]
-expand' ns (i,(_,env))
-  | null $ DM.toList (types env) = [(i ,(Name (ns++[i]),env) )]     
-  | True                      =  concat(map (expand' (ns++[i])) (DM.toList(types env)))  
- 
--------------------------------------------------------------------------------------
-type IEnv = TypeMapExp
-type TMSEnv = TypeMapExp
-type TMEnv = TypeMapExp
-type TEnv = TypeMapExp
-type Env = TypeMapExp
-type DirectoryPath = String
-type ClassPath = String
--------------------------------------------------------------------------------------
-createTMSEnv :: IEnv -> [MemberDecl] -> TMSEnv
-createTMSEnv = undefined
--------------------------------------------------------------------------------------
-createTMEnv :: TMSEnv -> [MemberDecl] -> TMEnv
-createTMEnv = undefined
--------------------------------------------------------------------------------------
-createTEnv :: TMEnv -> [MemberDecl] -> TEnv
-createTEnv = undefined
--------------------------------------------------------------------------------------
-createEnv :: TEnv -> [MemberDecl] -> Env
-createEnv = undefined
--------------------------------------------------------------------------------------
--- Dummies:
-checkTMsigs = undefined
-checkTFs = undefined
-checkTMs = undefined
-checkSigs = undefined
-checkBodies = undefined
--------------------------------------------------------------------------------------
-testImportDecl = ImportDecl False (Name [Ident "paragon",Ident "util"]) True
--------------------------------------------------------------------------------------}
---assume there is no static imports
-{-
------ import static Java.typename.member;   
-createIEnv' (ImportDecl True (Name idents) False) ienv currentDirectory = 
-  do   
-    let relative           = pathOf $ init idents
-    let absoluteFile       = currentDirectory ++ [pathSeparator] ++ relative ++ ".pi"
-    let (Ident memberName) = last idents
-    let (Ident className)  = last $ init idents
-    fetchStaticMember memberName className ienv absoluteFile 
-
------ import static Java.typename.*;      
-createIEnv' (ImportDecl True (Name idents) True) ienv currentDirectory =   
-  do   
-    let relative          = pathOf idents
-    let absoluteFile      = currentDirectory ++ [pathSeparator] ++ relative ++ ".pi"
-    let (Ident className) = last idents
-    fetchStaticCompilationUnit className ienv absoluteFile
--}
-
--- Assume we don't have any static import
-{-
--- import package1.class1.member1
-fetchStaticCompilationUnit :: String -> IEnv -> String -> IO IEnv
-fetchStaticCompilationUnit compilationUnitName env piPath = do
-  (InterfaceDecl mods id@(Ident compilationUnitName) params refs body) <- getInterface piPath 
-                                                       -- Assume there is only one type in each pi file 
-                                                       -- with the specified name
-  let mp = types env
-  let newTypeMap= TypeMap { 
-        this= undefined
-        ,fields = undefined
-        ,methods = undefined
-        ,constrs= (DM.empty)          
-        ,locks=undefined        
-        ,policies=undefined
-        ,typemethods=undefined          
-        ,types = (DM.empty)
-        }
-  return env{ types = (DM.insert (Name [id]) newTypeMap mp) } --error here because the idnet is not a name
-
-fetchStaticMember :: String -> String -> IEnv -> String -> IO IEnv
-fetchStaticMember memberName compilationUnitName env piPath = do
-  (InterfaceDecl mods id@(Ident compilationUnitName) params refs body) <- getInterface piPath 
-                                                       -- Assume there is only one type in each pi file 
-                                                       -- with the specified name
-  let mp = types env
-  let newTypeMap= TypeMap { 
-        this= undefined
-        ,fields = undefined
-        ,methods = undefined
-        ,constrs=undefined           
-        ,locks=undefined        
-        ,policies=undefined
-        ,typemethods=undefined          
-        ,types = (DM.empty)
-        }
-  return env{ types = (DM.insert (Name [id]) newTypeMap mp) } --error here because the idnet is not a name
--}
diff --git a/src/Language/Java/Paragon/TypeCheck.hs b/src/Language/Java/Paragon/TypeCheck.hs
--- a/src/Language/Java/Paragon/TypeCheck.hs
+++ b/src/Language/Java/Paragon/TypeCheck.hs
@@ -166,7 +166,7 @@
 withEnvFromClass :: FilePath -> String -> TcCont r a -> TcCont r a
 withEnvFromClass fp className tcba = do
   --debug $ "Checking imported class: " ++ className
-  ClassDecl _ id@(Ident cuName) tps _super _impls (ClassBody ds) <- getClass fp
+  ClassDecl ms id@(Ident cuName) tps _super _impls (ClassBody ds) <- getClass fp
   check (className == cuName) $ "File name " ++ className ++ " does not match class name " ++ cuName
   let mDs = map (\(MemberDecl d) -> d) ds
   fetchActors mDs $                  -- actor ids,
@@ -175,8 +175,9 @@
     fetchSignatures mDs $ do         -- and signatures of fields, methods, constructors and locks
       tm <- getTypeMap
       let typeTm = tm { packages = Map.empty, types = Map.empty }
+          typeSig = TSig True (Final `elem` ms) [] [] typeTm -- TODO: Insert actual values
       withTypeMap clearToTypes $
-        extendTypeMapT (Ident cuName) tps typeTm $ do
+        extendTypeMapT (Ident cuName) tps typeSig $ do
           tm <- getTypeMap
           --debug $ "TypeMap after adding " ++ className ++ ":\n" ++ show tm
           tcba
@@ -464,13 +465,15 @@
     withTypeMap $ \tm ->
         -- We insert an empty typemap at first,
         -- since we are only using this when checking signatures
-        tm { types = Map.insert i (tps,emptyTM) (types tm) }
+        let thisSig = TSig True False [] [] emptyTM
+        in tm { types = Map.insert i (tps,thisSig) (types tm) }
 
 withThisTypeSigs :: Ident -> [TypeParam] -> TcCont r a -> TcCont r a
 withThisTypeSigs i tps tcba = do
   tm <- getTypeMap
   let thisTm = tm { types = Map.empty, packages = Map.empty }
-  extendTypeMapT i tps thisTm $
+      thisSig = TSig True False [] [] thisTm -- TODO: Include proper values
+  extendTypeMapT i tps thisSig $
     tcba
 
 withTypeParam :: TypeParam -> TcCont r a -> TcCont r a
@@ -826,7 +829,7 @@
                         (--liftBase (debug "inside runTC") >> 
                                   tcExp polExp)
   check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?"
-  check (ty <: policyT) $ "Wrong type for policy expression: " ++ prettyPrint ty
+  checkM (ty <: policyT) $ "Wrong type for policy expression: " ++ prettyPrint ty
   -- check that _pol is bottom shouldn't be necessary
 
 
@@ -864,7 +867,7 @@
     Just (InitExp e) -> do
       (_,cs) <- runTc (simpleEnv lim) st $ do
                   (ty, pol) <- tcExp e
-                  check (ty <: matchTy) $ "typeCheckVarDecl: type mismatch"
+                  checkM (liftCont $ ty <: matchTy) $ "typeCheckVarDecl: type mismatch"
                   constraint_ pol matchPol
       solve cs
 
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,6 +1,6 @@
 module Language.Java.Paragon.TypeCheck.Monad 
     (
-     check, ignore, orElse, maybeM,
+     check, checkM, ignore, orElse, maybeM,
      withFold, withFoldMap,
 
      getThisType, getReturn,
@@ -45,7 +45,7 @@
      getReadPolicy, getWritePolicy, getLockPolicy,
      getParamPolicy, getReturnPolicy,
 
-     fromSrcType,
+     fromSrcType, (<:),
 
      evalPolicy, evalPolicyExp,
      evalLock, evalActor,
@@ -96,6 +96,9 @@
 check :: Monad m => Bool -> String -> m ()
 check b err = if b then return () else fail err
 
+checkM :: Monad m => m Bool -> String -> m ()
+checkM mb err = mb >>= flip check err
+
 ignore :: Monad m => m a -> m ()
 ignore = (>> return ())
 
@@ -533,10 +536,10 @@
                           newTm = go is leafTm eTm
                       in tm { packages = Map.insert i newTm mTm }
 
-extendTypeMapT :: Ident -> [TypeParam] -> TypeMap -> TcCont r a -> TcCont r a
-extendTypeMapT i tps leafTm =
+extendTypeMapT :: Ident -> [TypeParam] -> TypeSig -> TcCont r a -> TcCont r a
+extendTypeMapT i tps tSig =
     withTypeMap $ \tm -> 
-        tm { types = Map.insert i (tps, leafTm) (types tm) }
+        tm { types = Map.insert i (tps, tSig) (types tm) }
 
 
 lookupPkgTypeMap :: [Ident] -> TcCont r TypeMap
@@ -741,6 +744,40 @@
 ofPol = TcRigidVar
 
 
+------------------------------------------------------------
+-- Subtyping
+
+(<:) :: TcType -> TcType -> TcCont r Bool
+-- Short-cut for the most common case.
+t1 <: t2 | t1 == t2 = return True
+-- Sub-typing for primitive types.
+TcPrimT pt1 <: TcPrimT pt2 = return $ pt1 <<: pt2
+t1 <: t2 | isPolicyType t1 && t2 == policyT = return True
+         | isLockType t1 && t2 == booleanT = return True
+         | isActorType t1 && t2 == actorT = return True
+-- Sub-typing for reference types.
+-- - Null.
+TcRefT (TcClsRefT TcNullT) <: TcRefT _ = return True
+_ <: _ = return False
+
+
+(<<:) :: PrimType -> PrimType -> Bool
+ByteT <<: ShortT = True
+t <<: IntT    = t `elem` [ShortT, ByteT, CharT]
+t <<: LongT   = t == IntT   || t <<: IntT
+t <<: FloatT  = t == LongT  || t <<: LongT
+t <<: DoubleT = t == FloatT || t <<: FloatT
+_ <<: _ = False
+      
+
+{-
+   | t1 == nullT && isRefType t2 = True
+   | isLockType t1 && t2 == booleanT = True
+   -- Should surely be more cases here
+   | isPolicyType t1 && t2 == policyT = True
+   -- When we add proper subtyping, it must also be in Tc
+   | otherwise = False
+-}
 
 
 
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
@@ -33,7 +33,7 @@
       -- typemethod eval info
       typemethods :: Map Ident ([Ident], Block),
       -- types and packages
-      types       :: Map Ident ([TypeParam], TypeMap),
+      types       :: Map Ident ([TypeParam], TypeSig),
       packages    :: Map Ident TypeMap
     }
   deriving (Show, Data, Typeable)
@@ -137,6 +137,15 @@
   deriving (Show, Data, Typeable)
 
 
+data TypeSig = TSig {
+      tIsClass    :: Bool,
+      tIsFinal    :: Bool,
+      tSupers     :: [TcType],
+      tImpls      :: [TcType],
+      tMembers    :: TypeMap
+    }
+  deriving (Show, Data, Typeable)
+
 --------------------------------------
 --   Type argument instantiation    --
 --------------------------------------
@@ -214,7 +223,7 @@
 pkgsAndTypes :: TypeMap -> Map Ident TypeMap
 pkgsAndTypes tm = Map.union (packages tm)
                     -- disregard type parameters
-                    (Map.map snd $ types tm)
+                    (Map.map (tMembers . snd) $ types tm)
 
 lookupTypeOfN :: Name -> TypeMap -> TypeMap
 lookupTypeOfN (Name is) tm = aux is tm tm
@@ -236,7 +245,7 @@
           aux ((i, args):iargs) tm =
               let newTm =
                    case Map.lookup i (types tm) of
-                     Just (pars, genTm) -> instantiate (zip pars args) genTm
+                     Just (pars, tsig) -> instantiate (zip pars args) (tMembers tsig)
                      Nothing -> 
                          case Map.lookup i (packages tm) of
                            Just tm -> tm
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
@@ -96,7 +96,8 @@
   (tyRhs, pRhs) <- tcExp rhs
 
   -- Check all the necessary constraints:
-  check (tyRhs <: tyV) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV
+  checkM (liftCont $ tyRhs <: tyV) $ 
+             "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV
   -- Check: E[branchPC](n) <= pV
   bpc <- maybe getBranchPC_ getBranchPC mEnt
 
@@ -164,7 +165,7 @@
 -- Rule COND
 tcExp (Cond c e1 e2) = do
   (tyC, pC) <- tcExp c
-  check (tyC <: booleanT) $ "Cannot convert type to boolean"
+  checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"
   extendBranchPC pC $ do
     ((ty1, p1), (ty2, p2)) <- 
         (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2
@@ -229,7 +230,7 @@
 tcExp (Cast t e) = do
   (tyE, pE) <- tcExp e
   tyC <- liftCont $ evalSrcType t
-  check (tyE <: tyC) $ "Wrong type at cast"
+  checkM (liftCont $ tyE <: tyC) $ "Wrong type at cast"
   return (tyC, pE)
 
 tcExp (FieldAccess fa) = tcFieldAccess fa
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
@@ -35,7 +35,7 @@
 -- Rule IF
 tcStmt (IfThenElse c s1 s2) = do
   (tyC, pC) <- tcExp c
-  check (tyC <: booleanT) $ "Cannot convert type to boolean"
+  checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"
   extendBranchPC pC $ do
     ignore $ (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2
 
@@ -46,7 +46,7 @@
 tcStmt (While c sBody) = do
   s <- getState                  -- Starting state S
   (tyC, pC) <- tcExp c
-  check (tyC <: booleanT) $ "Cannot convert type to boolean"
+  checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"
   extendBranchPC pC $
     addBranchPC breakE bottom $
     addBranchPC continueE bottom $ 
@@ -103,7 +103,7 @@
 tcStmt (Return (Just e)) = do
   (tyR, pR) <- getReturn
   (tyE, pE) <- tcExp e
-  check (tyE <: tyR) $ "Returned value has wrong type: " ++ prettyPrint tyE
+  checkM (liftCont $ tyE <: tyR) $ "Returned value has wrong type: " ++ prettyPrint tyE
   
   -- Check pE <=[L] pR
   l <- getCurrentLockState
@@ -257,7 +257,8 @@
 tcBlockStmts (LocalVars ms t [VarDecl (VarId i) (Just (InitExp e))] : bss) = do
   (tyE, pE) <- tcExp e
   tyV <- liftCont $ evalSrcType t
-  check (tyE <: tyV) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV
+  checkM (liftCont $ tyE <: tyV) $ 
+             "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV
   pV <- localVarPol ms
   tyV' <- case mActorId tyE of
             Nothing -> return tyV
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
@@ -143,16 +143,6 @@
 -------------------------------------------
 -- Type operations
 
-(<:) :: TcType -> TcType -> Bool
-t1 <: t2 
-   | t1 == t2 = True
-   | t1 == nullT && isRefType t2 = True
-   | isLockType t1 && t2 == booleanT = True
-   -- Should surely be more cases here
-   | isPolicyType t1 && t2 == policyT = True
-   -- When we add proper subtyping, it must also be in Tc
-   | otherwise = False
-
 
 unboxConvert :: TcType -> Maybe PrimType
 unboxConvert (TcPrimT t) = Just t