Revive External Core typechecker
[ghc-hetmet.git] / utils / ext-core / Check.hs
index dedc0f4..29fb71f 100644 (file)
@@ -1,12 +1,19 @@
-module Check where
+{-# OPTIONS -Wall -fno-warn-name-shadowing #-}
+module Check(
+  checkModule, envsModule,
+  checkExpr, checkType, 
+  primCoercionError, 
+  Menv, Venv, Tvenv, Envs(..),
+  CheckRes(..), splitTy, substl) where
 
 import Maybe
 import Control.Monad.Reader
 
 import Core
-import Printer
+import Printer()
 import List
 import Env
+import PrimEnv
 
 {- Checking is done in a simple error monad.  In addition to
    allowing errors to be captured, this makes it easy to guarantee
@@ -25,7 +32,7 @@ getGlobalEnv = ask >>= (return . snd)
 
 instance Monad CheckRes where
   OkC a >>= k = k a
-  FailC s >>= k = fail s
+  FailC s >>= _ = fail s
   return = OkC
   fail = FailC
 
@@ -40,19 +47,31 @@ requireM cond s =
 
 {- Environments. -}
 type Tvenv = Env Tvar Kind                    -- type variables  (local only)
-type Tcenv = Env Tcon Kind                    -- type constructors
+type Tcenv = Env Tcon KindOrCoercion          -- type constructors
 type Tsenv = Env Tcon ([Tvar],Ty)             -- type synonyms
 type Cenv = Env Dcon Ty                      -- data constructors
 type Venv = Env Var Ty                               -- values
 type Menv = Env AnMname Envs                 -- modules
 data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
+  deriving Show
 
-{- Extend an environment, checking for illegal shadowing of identifiers. -}
-extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
-extendM env (k,d) = 
+{- Extend an environment, checking for illegal shadowing of identifiers (for term
+   variables -- shadowing type variables is allowed.) -}
+data EnvType = Tv | NotTv
+  deriving Eq
+
+extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
+extendM envType env (k,d) = 
    case elookup env k of
-     Just _ -> fail ("multiply-defined identifier: " ++ show k)
-     Nothing -> return (eextend env (k,d))
+     Just _ | envType == NotTv -> fail ("multiply-defined identifier: " 
+                                      ++ show k)
+     _ -> return (eextend env (k,d))
+
+extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
+extendVenv = extendM NotTv
+
+extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
+extendTvenv = extendM Tv
 
 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
 lookupM env k =   
@@ -62,34 +81,72 @@ lookupM env k =
             
 {- Main entry point. -}
 checkModule :: Menv -> Module -> CheckRes Menv
-checkModule globalEnv mod@(Module mn tdefs vdefgs) = 
+checkModule globalEnv (Module mn tdefs vdefgs) = 
   runReaderT 
     (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
-        (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
+        (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
                               (eempty,eempty) 
                               vdefgs
         return (eextend globalEnv 
             (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})))
     (mn, globalEnv)   
 
+-- Like checkModule, but doesn't typecheck the code, instead just
+-- returning declared types for top-level defns.
+-- This is necessary in order to handle circular dependencies, but it's sort
+-- of unpleasant.
+envsModule :: Menv -> Module -> Menv
+envsModule globalEnv (Module mn tdefs vdefgs) = 
+   let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs
+       e_venv               = foldr vdefgTypes eempty vdefgs in
+     eextend globalEnv (mn, 
+             (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
+        where vdefgTypes :: Vdefg -> Venv -> Venv
+              vdefgTypes (Nonrec (Vdef (v,t,_))) e =
+                             add [(v,t)] e
+              vdefgTypes (Rec vds) e = 
+                             add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
+              add :: [(Qual Var,Ty)] -> Venv -> Venv
+              add pairs e = foldr addOne e pairs
+              addOne :: (Qual Var, Ty) -> Venv -> Venv
+              addOne ((Nothing,_),_) e = e
+              addOne ((Just _,v),t) e  = eextend e (v,t)
+
 checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
 checkTdef0 (tcenv,tsenv) tdef = ch tdef
       where 
        ch (Data (m,c) tbs _) = 
            do mn <- getMname
                requireModulesEq m mn "data type declaration" tdef False
-              tcenv' <- extendM tcenv (c,k)
+              tcenv' <- extendM NotTv tcenv (c, Kind k)
               return (tcenv',tsenv)
            where k = foldr Karrow Klifted (map snd tbs)
-        -- TODO
-       ch (Newtype (m,c) tbs axiom rhs) = 
+       ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = 
            do mn <- getMname
                requireModulesEq m mn "newtype declaration" tdef False
-              tcenv' <- extendM tcenv (c,k)
+              tcenv' <- extendM NotTv tcenv (c, Kind k)
+               -- add newtype axiom to env
+               tcenv'' <- extendM NotTv tcenv' 
+                  (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
               tsenv' <- case rhs of
                           Nothing -> return tsenv
-                          Just rep -> extendM tsenv (c,(map fst tbs,rep))
-              return (tcenv', tsenv')
+                          Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
+              return (tcenv'', tsenv')
+           where k = foldr Karrow Klifted (map snd tbs)
+
+processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
+processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
+      where 
+       ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
+           where k = foldr Karrow Klifted (map snd tbs)
+       ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = 
+           let tcenv' = eextend tcenv (c, Kind k)
+                -- add newtype axiom to env
+                tcenv'' = eextend tcenv' 
+                  (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
+               tsenv' = maybe tsenv 
+                  (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
+               (tcenv'', tsenv')
            where k = foldr Karrow Klifted (map snd tbs)
     
 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
@@ -97,12 +154,12 @@ checkTdef tcenv cenv = ch
        where 
         ch (Data (_,c) utbs cdefs) = 
            do cbinds <- mapM checkCdef cdefs
-              foldM extendM cenv cbinds
+              foldM (extendM NotTv) cenv cbinds
            where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
                    do mn <- getMname
                        requireModulesEq m mn "constructor declaration" cdef 
                          False 
-                      tvenv <- foldM extendM eempty tbs 
+                      tvenv <- foldM (extendM Tv) eempty tbs 
                       ks <- mapM (checkTy (tcenv,tvenv)) ts
                       mapM_ (\k -> require (baseKind k)
                                            ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
@@ -113,26 +170,57 @@ checkTdef tcenv cenv = ch
                                  (foldr tArrow
                                          (foldl Tapp (Tcon (Just mn,c))
                                                 (map (Tvar . fst) utbs)) ts) tbs
-         -- TODO
-        ch (tdef@(Newtype c tbs axiom (Just t))) =  
-           do tvenv <- foldM extendM eempty tbs
+         ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) =  
+           do tvenv <- foldM (extendM Tv) eempty tbs
               k <- checkTy (tcenv,tvenv) t
-              require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef) 
+               -- Makes sure GHC is eta-expanding things properly
+               require (length tbs == length coTbs) $
+                 ("Arity mismatch between newtycon and newtype coercion: "
+                  ++ show tdef)
+               require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
+               axiomTvenv <- foldM (extendM Tv) eempty coTbs
+               kLhs <- checkTy (tcenv,axiomTvenv) coLhs
+               kRhs <- checkTy (tcenv,axiomTvenv) coRhs
+               require (kLhs `eqKind` kRhs) 
+                  ("Kind mismatch in newtype axiom types: " ++ show tdef 
+                    ++ " kinds: " ++
+                   (show kLhs) ++ " and " ++ (show kRhs))
               return cenv
-        ch (tdef@(Newtype c tbs axiom Nothing)) =
+        ch (Newtype _ _ _ Nothing) =
            {- should only occur for recursive Newtypes -}
            return cenv
 
+processCdef :: Cenv -> Tdef -> Cenv
+processCdef cenv = ch
+  where
+    ch (Data (_,c) utbs cdefs) = do 
+       let cbinds = map checkCdef cdefs
+       foldl eextend cenv cbinds
+     where checkCdef (Constr (mn,dcon) etbs ts) =
+             (dcon,t mn) 
+            where tbs = utbs ++ etbs
+                  t mn = foldr Tforall 
+                         (foldr tArrow
+                           (foldl Tapp (Tcon (mn,c))
+                               (map (Tvar . fst) utbs)) ts) tbs
+    ch _ = cenv
+
 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv)
 mkTypeEnvs tdefs = do
   (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
   cenv <- foldM (checkTdef tcenv) eempty tdefs
   return (tcenv, tsenv, cenv)
 
+mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
+mkTypeEnvsNoChecking tdefs = 
+  let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
+      cenv           = foldl processCdef eempty tdefs in
+    (tcenv, tsenv, cenv)
+
 requireModulesEq :: Show a => Mname -> AnMname -> String -> a 
                           -> Bool -> CheckResult ()
 requireModulesEq (Just mn) m msg t _      = require (mn == m) (mkErrMsg msg t)
-requireModulesEq Nothing m msg t emptyOk  = require emptyOk (mkErrMsg msg t)
+requireModulesEq Nothing _ msg t emptyOk  = require emptyOk (mkErrMsg msg t)
 
 mkErrMsg :: Show a => String -> a -> String
 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t    
@@ -142,10 +230,10 @@ checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv)
 checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
       case vdefg of
        Rec vdefs ->
-           do e_venv' <- foldM extendM e_venv e_vts
-              l_venv' <- foldM extendM l_venv l_vts
+           do e_venv' <- foldM extendVenv e_venv e_vts
+              l_venv' <- foldM extendVenv l_venv l_vts
               let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
-              mapM_ (\ (vdef@(Vdef ((m,v),t,e))) -> 
+              mapM_ (\ (vdef@(Vdef ((m,_),t,e))) -> 
                            do mn <- getMname
                                requireModulesEq m mn "value definition" vdef True
                               k <- checkTy (tcenv,tvenv) t
@@ -160,33 +248,58 @@ checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
                  l_vts  = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
        Nonrec (vdef@(Vdef ((m,v),t,e))) ->
            do mn <- getMname
-               requireModulesEq m mn "value definition" vdef True
+               -- TODO: document this weirdness
+               let isZcMain = vdefIsMainWrapper mn m 
+               unless isZcMain $
+                    requireModulesEq m mn "value definition" vdef True
               k <- checkTy (tcenv,tvenv) t 
               require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
-              require ((not top_level) || (not (k `eqKind` Kunlifted))) ("top-level unlifted kind in:\n" ++ show vdef) 
+              require ((not top_level) || (not (k `eqKind` Kunlifted))) 
+                 ("top-level unlifted kind in:\n" ++ show vdef) 
               t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
               requireM (equalTy tsenv t t') 
-                       ("declared type doesn't match expression type in:\n" ++ show vdef  ++ "\n"  ++
+                       ("declared type doesn't match expression type in:\n" 
+                         ++ show vdef  ++ "\n"  ++
                         "declared type: " ++ show t ++ "\n" ++
                         "expression type: " ++ show t') 
               if isNothing m then
-                 do l_venv' <- extendM l_venv (v,t)
+                 do l_venv' <- extendVenv l_venv (v,t)
                     return (e_venv,l_venv')
                else
-                do e_venv' <- extendM e_venv (v,t)
+                              -- awful, but avoids name shadowing --
+                              -- otherwise we'd have two bindings for "main"
+                do e_venv' <- if isZcMain 
+                                 then return e_venv 
+                                 else extendVenv e_venv (v,t)
                     return (e_venv',l_venv)
     
+vdefIsMainWrapper :: AnMname -> Mname -> Bool
+vdefIsMainWrapper enclosing defining = 
+   enclosing == mainMname && defining == wrapperMainMname
+
 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv 
                -> Exp -> Ty
-checkExpr mn menv tdefs venv tvenv e = case (runReaderT (do
+checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
   (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
-  checkExp (tcenv, tsenv, tvenv, cenv, venv, eempty) e) 
-                            (mn, menv)) of
-    OkC t -> t
-    FailC s -> reportError s
+  -- Since the preprocessor calls checkExpr after code has been
+  -- typechecked, we expect to find the external env in the Menv.
+  case (elookup menv mn) of
+     Just thisEnv ->
+       checkExp (tcenv, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e 
+     Nothing -> reportError e ("checkExpr: Environment for " ++ 
+                  show mn ++ " not found")) (mn,menv) of
+         OkC t -> t
+         FailC s -> reportError e s
+
+checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
+checkType mn menv tdefs tvenv t = case runReaderT (do
+  (tcenv, _, _) <- mkTypeEnvs tdefs
+  checkTy (tcenv, tvenv) t) (mn, menv) of
+      OkC k -> k
+      FailC s -> reportError tvenv s
 
 checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
-checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch 
+checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
       where 
        ch e0 = 
          case e0 of
@@ -221,7 +334,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                   _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
                               "operator type: " ++ show t1)
            Lam (Tb tb) e ->
-             do tvenv' <- extendM tvenv tb 
+             do tvenv' <- extendTvenv tvenv tb 
                 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e 
                 return (Tforall tb t)
            Lam (Vb (vb@(_,vt))) e ->
@@ -229,7 +342,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                 require (baseKind k)   
                         ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
                          "kind: " ++ show k) 
-                l_venv' <- extendM l_venv vb
+                l_venv' <- extendVenv l_venv vb
                 t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
                 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0) 
                 return (tArrow vt t)
@@ -264,8 +377,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                          ok []                 _  = fail ("missing default alternative in literal case:\n" ++ show e0)
                      in ok as [l] 
                   [Adefault _] -> return ()
-                  [] -> fail ("no alternatives in case:\n" ++ show e0) 
-                l_venv' <- extendM l_venv (v,t)
+                  _ -> fail ("no alternatives in case:\n" ++ show e0) 
+                l_venv' <- extendVenv l_venv (v,t)
                 t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts  
                 bs <- mapM (equalTy tsenv t) ts
                 require (and bs)
@@ -276,11 +389,18 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                    " match case return type in:\n" ++ show e0 ++ "\n" ++
                    "alt type: " ++ show t ++ " return type: " ++ show resultTy)
                 return t
-           Cast e t -> 
-             do ch e 
-                checkTy (tcenv,tvenv) t 
-                return t
-           Note s e -> 
+           c@(Cast e t) -> 
+             do eTy <- ch e 
+                k <- checkTy (tcenv,tvenv) t
+                 case k of
+                    (Keq fromTy toTy) -> do
+                        require (eTy == fromTy) ("Type mismatch in cast: c = "
+                             ++ show c ++ " and " ++ show eTy
+                             ++ " and " ++ show fromTy)
+                        return toTy
+                    _ -> fail ("Cast with non-equality kind: " ++ show e 
+                               ++ " and " ++ show t ++ " has kind " ++ show k)
+           Note _ e -> 
              ch e
            External _ t -> 
              do checkTy (tcenv,eempty) t {- external types must be closed -}
@@ -308,7 +428,7 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
                         ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
                          "kinds declared in data constructor: " ++ show eks ++
                          "kinds declared in case alternative: " ++ show eks') 
-                tvenv' <- foldM extendM tvenv etbs
+                tvenv' <- foldM extendTvenv tvenv etbs
                 {- check term variables -}
                 let vts = map snd vbs
                 mapM_ (\vt -> require ((not . isUtupleTy) vt)
@@ -329,7 +449,7 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
                          ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
                           "pattern constructor type: " ++ show ct_res ++ "\n" ++
                           "scrutinee type: " ++ show t0) 
-                l_venv' <- foldM extendM l_venv vbs
+                l_venv' <- foldM extendVenv l_venv vbs
                 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e 
                 checkTy (tcenv,tvenv) t  {- check that existentials don't escape in result type -}
                 return t
@@ -344,25 +464,93 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
              checkExp env e
     
 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
-checkTy (tcenv,tvenv) = ch
+checkTy es@(tcenv,tvenv) t = ch t
      where
        ch (Tvar tv) = lookupM tvenv tv
-       ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc
+       ch (Tcon qtc) = do
+         kOrC <- qlookupM tcenv_ tcenv eempty qtc
+         case kOrC of
+            Kind k -> return k
+            Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
+            Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
        ch (t@(Tapp t1 t2)) = 
-          do k1 <- ch t1
-             k2 <- ch t2
-             case k1 of
-                Karrow k11 k12 ->
-                  do require (k2 `subKindOf` k11) 
-                            ("kinds don't match in type application: " ++ show t ++ "\n" ++
-                             "operator kind: " ++ show k11 ++ "\n" ++
-                             "operand kind: " ++ show k2)              
-                     return k12
-                _ -> fail ("applied type has non-arrow kind: " ++ show t)
+             case splitTyConApp_maybe t of
+               Just (tc, tys) -> do
+                 tcK <- qlookupM tcenv_ tcenv eempty tc 
+                 case tcK of
+                   Kind _ -> checkTapp t1 t2
+                   Coercion (DefinedCoercion tbs (from,to)) -> do
+                     -- makes sure coercion is fully applied
+                     require (length tys == length tbs) $
+                        ("Arity mismatch in coercion app: " ++ show t)
+                     let (tvs, tks) = unzip tbs
+                     argKs <- mapM (checkTy es) tys
+                     require (all (uncurry eqKind) (zip tks argKs))
+                        ("Kind mismatch in coercion app: " ++ show tks 
+                         ++ " and " ++ show argKs ++ " t = " ++ show t)
+                     return $ Keq (substl tvs tys from) (substl tvs tys to)
+               Nothing -> checkTapp t1 t2
+            where checkTapp t1 t2 = do 
+                   k1 <- ch t1
+                   k2 <- ch t2
+                   case k1 of
+                     Karrow k11 k12 ->
+                           case k2 of
+                               Keq eqTy1 eqTy2 -> do
+                                 -- Distribute the type operator over the
+                                 -- coercion
+                                 subK1 <- checkTy es eqTy1
+                                 subK2 <- checkTy es eqTy2
+                                 require (subK2 `subKindOf` k11 && 
+                                          subK1 `subKindOf` k11) $
+                                    kindError
+                                 return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2)
+                              _               -> do
+                                   require (k2 `subKindOf` k11) kindError
+                                   return k12
+                            where kindError = 
+                                    "kinds don't match in type application: "
+                                    ++ show t ++ "\n" ++
+                                   "operator kind: " ++ show k11 ++ "\n" ++
+                                   "operand kind: " ++ show k2 
+                     _ -> fail ("applied type has non-arrow kind: " ++ show t)
+                           
        ch (Tforall tb t) = 
-           do tvenv' <- extendM tvenv tb 
-              checkTy (tcenv,tvenv') t
-    
+           do tvenv' <- extendTvenv tvenv tb 
+              k <- checkTy (tcenv,tvenv') t
+               return $ case k of
+                 -- distribute the forall
+                 Keq t1 t2 -> Keq (Tforall tb t1) (Tforall tb t2)
+                 _         -> k
+       ch (TransCoercion t1 t2) = do
+            k1 <- checkTy es t1
+            k2 <- checkTy es t2
+            case (k1, k2) of
+              (Keq ty1 ty2, Keq ty3 ty4) | ty2 == ty3 ->
+                  return $ Keq ty1 ty4
+              _ -> fail ("Bad kinds in trans. coercion: " ++
+                           show k1 ++ " " ++ show k2)
+       ch (SymCoercion t1) = do
+            k <- checkTy es t1
+            case k of
+               Keq ty1 ty2 -> return $ Keq ty2 ty1
+               _           -> fail ("Bad kind in sym. coercion: "
+                            ++ show k)
+       ch (UnsafeCoercion t1 t2) = do
+            checkTy es t1
+            checkTy es t2
+            return $ Keq t1 t2
+       ch (LeftCoercion t1) = do
+            k <- checkTy es t1
+            case k of
+              Keq (Tapp u _) (Tapp w _) -> return $ Keq u w
+              _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+       ch (RightCoercion t1) = do
+            k <- checkTy es t1
+            case k of
+              Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x
+              _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+
 {- Type equality modulo newtype synonyms. -}
 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
 equalTy tsenv t1 t2 = 
@@ -377,10 +565,28 @@ equalTy tsenv t1 t2 =
            expand (Tforall tb t) = 
              do t' <- expand t
                 return (Tforall tb t')
+            expand (TransCoercion t1 t2) = do
+               exp1 <- expand t1
+               exp2 <- expand t2
+               return $ TransCoercion exp1 exp2
+            expand (SymCoercion t) = do
+               exp <- expand t
+               return $ SymCoercion exp
+            expand (UnsafeCoercion t1 t2) = do
+               exp1 <- expand t1
+               exp2 <- expand t2
+               return $ UnsafeCoercion exp1 exp2
+            expand (LeftCoercion t1) = do
+               exp1 <- expand t1
+               return $ LeftCoercion exp1
+            expand (RightCoercion t1) = do
+               exp1 <- expand t1
+               return $ RightCoercion exp1
            expapp (t@(Tcon (m,tc))) ts = 
              do env <- mlookupM tsenv_ tsenv eempty m
                 case elookup env tc of 
-                   Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs)
+                   Just (formals,rhs) | (length formals) == (length ts) ->
+                         return (substl formals ts rhs)
                    _ -> return (foldl Tapp t ts)
            expapp (Tapp t1 t2) ts = 
              do t2' <- expand t2
@@ -388,12 +594,11 @@ equalTy tsenv t1 t2 =
            expapp t ts = 
              do t' <- expand t
                 return (foldl Tapp t' ts)
-    
 
-mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname 
+mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
           -> CheckResult (Env a b)
 mlookupM _ _ local_env    Nothing            = return local_env
-mlookupM selector external_env _ (Just m) = do
+mlookupM selector external_env local_env (Just m) = do
   mn <- getMname
   if m == mn
      then return external_env
@@ -401,34 +606,33 @@ mlookupM selector external_env _ (Just m) = do
        globalEnv <- getGlobalEnv
        case elookup globalEnv m of
          Just env' -> return (selector env')
-         Nothing -> fail ("Check: undefined module name: " ++ show m)
+         Nothing -> fail ("Check: undefined module name: "
+                      ++ show m ++ show (edomain local_env))
 
-qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b 
+qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
                   -> Qual a -> CheckResult b
-qlookupM selector external_env local_env (m,k) =   
+qlookupM selector external_env local_env (m,k) =
       do env <- mlookupM selector external_env local_env m
-        lookupM env k
-
+         lookupM env k
 
 checkLit :: Lit -> CheckResult Ty
 checkLit (Literal lit t) =
   case lit of
-      -- TODO: restore commented-out stuff.
     Lint _ -> 
-         do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh]) 
-                    ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+         do require (t `elem` intLitTypes)
+                    ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
             return t
     Lrational _ ->
-         do {- require (elem t [tFloatzh,tDoublezh]) 
-                    ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+         do require (t `elem` ratLitTypes)
+                    ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
             return t
     Lchar _ -> 
-         do {- require (t == tCharzh) 
-                    ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)  -}
+         do require (t `elem` charLitTypes)
+                    ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
             return t   
     Lstring _ ->
-         do {- require (t == tAddrzh) 
-                    ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)  -}
+         do require (t `elem` stringLitTypes)
+                    ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
             return t
 
 {- Utilities -}
@@ -460,6 +664,11 @@ substl tvs ts t = f (zip tvs ts) t
            Tforall (t',k) (f ((t,Tvar t'):env) t1)
          else 
           Tforall (t,k) (f (filter ((/=t).fst) env) t1)
+       TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
+       SymCoercion t1 -> SymCoercion (f env t1)
+       UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
+       LeftCoercion t1 -> LeftCoercion (f env t1)
+       RightCoercion t1 -> RightCoercion (f env t1)
      where free = foldr union [] (map (freeTvars.snd) env)
            t' = freshTvar free 
    
@@ -469,10 +678,21 @@ freeTvars (Tcon _) = []
 freeTvars (Tvar v) = [v]
 freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1) 
+freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
+freeTvars (SymCoercion t) = freeTvars t
+freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
+freeTvars (LeftCoercion t) = freeTvars t
+freeTvars (RightCoercion t) = freeTvars t
 
 {- Return any tvar *not* in the argument list. -}
 freshTvar :: [Tvar] -> Tvar
 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
 
+primCoercionError :: Show a => a -> b
+primCoercionError s = error $ "Bad coercion application: " ++ show s
+
 -- todo
-reportError s = error $ ("Core parser error: checkExpr failed with " ++ s)
+reportError :: Show a => a -> String -> b
+reportError e s = error $ ("Core type error: checkExpr failed with "
+                   ++ s ++ " and " ++ show e)
+