X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FCheck.hs;h=af3bb3c55969d1bb866b4c7b4b4df9e43addae22;hp=dedc0f41088ab458a8202d80cfb7445c699d9146;hb=e4417dcd4679da9c6b18c02ff667199c572bed89;hpb=6e93da5e0a775b2bfb9c9f2bd31a36cc828521cb

diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
index dedc0f4..af3bb3c 100644
--- a/utils/ext-core/Check.hs
+++ b/utils/ext-core/Check.hs
@@ -1,12 +1,21 @@
-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
+-- just for printing warnings
+import System.IO.Unsafe
 
 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 +34,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 +49,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,15 +83,37 @@ 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)   
+         -- avoid name shadowing
+    (mn, eremove globalEnv mn)
+
+-- 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
@@ -78,31 +121,62 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef
 	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) coVar tbs 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'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
 	       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 tc@(_,c) coercion tbs rhs) = 
+	    let tcenv' = eextend tcenv (c, Kind k)
+                -- add newtype axiom to env
+                tcenv'' = case rhs of
+                            Just rep ->
+                              eextend tcenv' 
+                               (snd coercion, Coercion $ DefinedCoercion tbs
+                                (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep))
+                            Nothing -> tcenv'
+	        tsenv' = maybe tsenv 
+                  (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
+               (tcenv'', tsenv')
 	    where k = foldr Karrow Klifted (map snd tbs)
+
+envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Maybe Ty 
+  -> CheckResult Tcenv
+envPlusNewtype tcenv tyCon coVar tbs rhs =
+  case rhs of
+    Nothing -> return tcenv
+    Just rep -> extendM NotTv tcenv 
+                  (snd coVar, Coercion $ DefinedCoercion tbs
+                            (foldl Tapp (Tcon tyCon) 
+                                       (map Tvar (fst (unzip tbs))),
+                                       rep))
     
 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
 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,82 +187,126 @@ 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
-	       k <- checkTy (tcenv,tvenv) t
-	       require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef) 
+         ch (tdef@(Newtype tc _ tbs (Just t))) =  
+	    do tvenv <- foldM (extendM Tv) eempty tbs
+	       kRhs <- checkTy (tcenv,tvenv) t
+               require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
+               kLhs <- checkTy (tcenv,tvenv) 
+                         (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
+               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    
 
 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) 
                -> Vdefg -> CheckResult (Venv,Venv)
-checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
+checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
+      mn <- getMname
       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', l_venv') <- makeEnv mn vdefs
 	       let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
-	       mapM_ (\ (vdef@(Vdef ((m,v),t,e))) -> 
-			    do mn <- getMname
-                               requireModulesEq m mn "value definition" vdef True
-			       k <- checkTy (tcenv,tvenv) t
-			       require (k `eqKind` Klifted) ("unlifted kind in:\n" ++ show vdef)
-			       t' <- checkExp env' e
-			       requireM (equalTy tsenv t t') 
-					("declared type doesn't match expression type in:\n"  ++ show vdef ++ "\n" ++  
-					 "declared type: " ++ show t ++ "\n" ++
-					 "expression type: " ++ show t')) vdefs
-	       return (e_venv',l_venv')
-	    where e_vts  = [ (v,t) | Vdef ((Just _,v),t,_) <- vdefs ]
-	          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
-	       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) 
-	       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: " ++ show t ++ "\n" ++
-			 "expression type: " ++ show t') 
-	       if isNothing m then
-                 do l_venv' <- extendM l_venv (v,t)
-                    return (e_venv,l_venv')
-	        else
-		 do e_venv' <- extendM e_venv (v,t)
-                    return (e_venv',l_venv)
+               mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) 
+                        ("unlifted kind in:\n" ++ show vdef)) env') 
+                     vdefs
+               return (e_venv', l_venv')
+	Nonrec vdef ->
+	    do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv)
+               checkVdef (\ vdef k -> do
+                     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)) env' vdef
+               makeEnv mn [vdef]
+
+  where makeEnv mn vdefs = do
+             ev <- foldM extendVenv e_venv e_vts
+             lv <- foldM extendVenv l_venv l_vts
+             return (ev, lv)
+           where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
+                                     not (vdefIsMainWrapper mn (Just m))]
+                 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
+        checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
+          mn <- getMname
+          let isZcMain = vdefIsMainWrapper mn m
+          unless isZcMain $
+             requireModulesEq m mn "value definition" vdef True
+	  k <- checkTy (tcenv,tvenv) t
+	  checkKind vdef k
+	  t' <- checkExp env e
+	  requireM (equalTy tsenv t t') 
+		   ("declared type doesn't match expression type in:\n"  
+                    ++ show vdef ++ "\n" ++  
+		    "declared type: " ++ show t ++ "\n" ++
+		    "expression type: " ++ show t')
     
+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 = 
+	ch e0 =
 	  case e0 of
 	    Var qv -> 
 	      qlookupM venv_ e_venv l_venv qv
@@ -221,7 +339,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 +347,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 +382,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 +394,14 @@ 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 
+		 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
+                 require (eTy == fromTy) ("Type mismatch in cast: c = "
+                             ++ show c ++ "\nand eTy = " ++ show eTy
+                             ++ "\n and " ++ show fromTy)
+                 return toTy
+	    Note _ e -> 
 	      ch e
 	    External _ t -> 
 	      do checkTy (tcenv,eempty) t {- external types must be closed -}
@@ -308,7 +429,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 +450,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 +465,146 @@ 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) = ch
      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
+                     let kPairs = zip argKs tks
+                     let kindsOk = all (uncurry eqKind) kPairs
+                     if not kindsOk &&
+                        all (uncurry subKindOf) kPairs
+                       -- GHC occasionally generates code like:
+                       -- :Co:TTypeable2 (->)
+                       -- where in this case, :Co:TTypeable2 expects an
+                       -- argument of kind (*->(*->*)) and (->) has kind
+                       -- (?->(?->*)). I'm not sure whether or not it's
+                       -- sound to apply an arbitrary coercion to an
+                       -- argument that's a subkind of what it expects.
+                       then warn $ "Applying coercion " ++ show tc ++
+                               " to arguments of kind " ++ show argKs
+                               ++ " when it expects: " ++ show tks
+                       else require kindsOk
+                        ("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 -> 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 
+               checkTy (tcenv,tvenv') t
+       ch (TransCoercion t1 t2) = do
+            (ty1,ty2) <- checkTyCo es t1
+            (ty3,ty4) <- checkTyCo es t2
+            require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
+                        show ty2 ++ " and " ++ show ty3)
+            return $ Keq ty1 ty4
+       ch (SymCoercion t1) = do
+            (ty1,ty2) <- checkTyCo es t1
+            return $ Keq ty2 ty1
+       ch (UnsafeCoercion t1 t2) = do
+            checkTy es t1
+            checkTy es t2
+            return $ Keq t1 t2
+       ch (LeftCoercion t1) = do
+            k <- checkTyCo es t1
+            case k of
+              ((Tapp u _), (Tapp w _)) -> return $ Keq u w
+              _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+       ch (RightCoercion t1) = do
+            k <- checkTyCo es t1
+            case k of
+              ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
+              _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+       ch (InstCoercion ty arg) = do
+            forallK <- checkTyCo es ty
+            case forallK of
+              ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
+                 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
+                                            ++ show ty)
+                 argK <- checkTy es arg
+                 require (argK `eqKind` k1) ("Kind mismatch in type being "
+                           ++ "instantiated: " ++ show arg)
+                 let newLhs = substl [v1] [arg] b1
+                 let newRhs = substl [v2] [arg] b2
+                 return $ Keq newLhs newRhs
+              _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
+
+checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
+checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = 
+  (case splitTyConApp_maybe t of
+    Just (tc, tys) -> do
+       tcK <- qlookupM tcenv_ tcenv eempty tc
+       case tcK of
+ -- todo: avoid duplicating this code
+ -- blah, this almost calls for a different syntactic form
+ -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
+         Coercion (DefinedCoercion tbs (from, to)) -> do
+           require (length tys == length tbs) $ 
+            ("Arity mismatch in coercion app: " ++ show t)
+           let (tvs, tks) = unzip tbs
+           argKs <- mapM (checkTy es) tys
+           let kPairs = zip argKs tks
+           let kindsOk = all (uncurry eqKind) kPairs
+           if not kindsOk &&
+                        all (uncurry subKindOf) kPairs
+                       -- see comments in checkTy about this
+                       then warn $ "Applying coercion " ++ show tc ++
+                               " to arguments of kind " ++ show argKs
+                               ++ " when it expects: " ++ show tks
+                       else require kindsOk
+                        ("Kind mismatch in coercion app: " ++ show tks 
+                         ++ " and " ++ show argKs ++ " t = " ++ show t)
+           return (substl tvs tys from, substl tvs tys to)
+         _ -> checkTapp t1 t2
+    _ -> checkTapp t1 t2)
+       where checkTapp t1 t2 = do
+               (lhsRator, rhsRator) <- checkTyCo es t1
+               (lhs, rhs) <- checkTyCo es t2
+               -- Comp rule from paper
+               checkTy es (Tapp lhsRator lhs)
+               checkTy es (Tapp rhsRator rhs)
+               return (Tapp lhsRator lhs, Tapp rhsRator rhs)
+checkTyCo (tcenv, tvenv) (Tforall tb t) = do
+  tvenv' <- extendTvenv tvenv tb
+  (t1,t2) <- checkTyCo (tcenv, tvenv') t
+  return (Tforall tb t1, Tforall tb t2)
+checkTyCo es t = do
+  k <- checkTy es t
+  case k of
+    Keq t1 t2 -> return (t1, t2)
+    -- otherwise, expand by the "refl" rule
+    _          -> return (t, t)
+
 {- Type equality modulo newtype synonyms. -}
 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
 equalTy tsenv t1 t2 = 
@@ -377,10 +619,32 @@ 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
+            expand (InstCoercion t1 t2) = do
+               exp1 <- expand t1
+               exp2 <- expand t2
+               return $ InstCoercion exp1 exp2
 	    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 +652,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 +664,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 +722,12 @@ 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)
+       InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
      where free = foldr union [] (map (freeTvars.snd) env)
            t' = freshTvar free 
    
@@ -467,12 +735,26 @@ substl tvs ts t = f (zip tvs ts) t
 freeTvars :: Ty -> [Tvar]
 freeTvars (Tcon _) = []
 freeTvars (Tvar v) = [v]
-freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
+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
+freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
 
 {- 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)
+
+warn :: String -> CheckResult ()
+warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return ()
\ No newline at end of file