From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Mon, 14 Apr 2008 02:46:48 +0000 (+0000)
Subject: Revive External Core typechecker
X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=420a27dc9fb7de5fc6c96fe078ddd4dc87222d44

Revive External Core typechecker

The typechecker works again! Yay!

Details upon request.
---

diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
index dedc0f4..29fb71f 100644
--- a/utils/ext-core/Check.hs
+++ b/utils/ext-core/Check.hs
@@ -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)
+
diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs
index 46e8185..ce2a11d 100644
--- a/utils/ext-core/Core.hs
+++ b/utils/ext-core/Core.hs
@@ -1,5 +1,7 @@
 module Core where
 
+import Encoding
+
 import List (elemIndex)
 
 data Module 
@@ -13,7 +15,7 @@ data Cdef
   = Constr (Qual Dcon) [Tbind] [Ty]
 
 -- Newtype coercion
-type Axiom = (Qual Tcon, Kind)
+type Axiom = (Qual Tcon, [Tbind], (Ty,Ty))
 
 data Vdefg 
   = Rec [Vdef]
@@ -51,6 +53,15 @@ data Ty
   | Tcon (Qual Tcon)
   | Tapp Ty Ty
   | Tforall Tbind Ty 
+-- Wired-in coercions:
+-- These are primitive tycons in GHC, but in ext-core,
+-- we make them explicit, to make the typechecker
+-- somewhat more clear. 
+  | TransCoercion Ty Ty
+  | SymCoercion Ty
+  | UnsafeCoercion Ty Ty
+  | LeftCoercion Ty
+  | RightCoercion Ty
 
 data Kind 
   = Klifted
@@ -59,6 +70,25 @@ data Kind
   | Karrow Kind Kind
   | Keq Ty Ty
 
+-- A CoercionKind isn't really a Kind at all, but rather,
+-- corresponds to an arbitrary user-declared axiom.
+-- A tycon whose CoercionKind is (DefinedCoercion <tbs> (from, to))
+-- represents a tycon with arity (length tbs), whose kind is
+-- (from :=: to) (modulo substituting type arguments.
+-- It's not a Kind because a coercion must always be fully applied:
+-- whenever we see a tycon that has such a CoercionKind, it must
+-- be fully applied if it's to be assigned an actual Kind.
+-- So, a CoercionKind *only* appears in the environment (mapping
+-- newtype axioms onto CoercionKinds).
+-- Was that clear??
+data CoercionKind = 
+   DefinedCoercion [Tbind] (Ty,Ty)
+
+-- The type constructor environment maps names that are
+-- either type constructors or coercion names onto either
+-- kinds or coercion kinds.
+data KindOrCoercion = Kind Kind | Coercion CoercionKind
+  
 data Lit = Literal CoreLit Ty
   deriving Eq   -- with nearlyEqualTy 
 
@@ -74,8 +104,8 @@ data CoreLit = Lint Integer
 -- module namespace, either when printing out
 -- Core or (probably preferably) in a 
 -- preprocessor.
--- The empty module name (as in an unqualified name)
--- is represented as Nothing.
+-- We represent the empty module name (as in an unqualified name)
+-- with Nothing.
 
 type Mname = Maybe AnMname
 type AnMname = (Pname, [Id], Id)
@@ -104,8 +134,18 @@ eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
 eqKind _ _ = False -- no Keq kind is ever equal to any other...
                    -- maybe ok for now?
 
---- tjc: I haven't looked at the rest of this file. ---
 
+splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
+splitTyConApp_maybe (Tvar _) = Nothing
+splitTyConApp_maybe (Tcon t) = Just (t,[])
+splitTyConApp_maybe (Tapp rator rand) = 
+   case (splitTyConApp_maybe rator) of
+      Just (r,rs) -> Just (r,rs++[rand])
+      Nothing     -> case rator of
+                       Tcon tc -> Just (tc,[rand])
+                       _       -> Nothing
+splitTyConApp_maybe t@(Tforall _ _) = Nothing
+           
 {- Doesn't expand out fully applied newtype synonyms
    (for which an environment is needed). -}
 nearlyEqualTy t1 t2 =  eqTy [] [] t1 t2 
@@ -125,6 +165,8 @@ instance Eq Ty where (==) = nearlyEqualTy
 
 subKindOf :: Kind -> Kind -> Bool
 _ `subKindOf` Kopen = True
+(Karrow a1 r1) `subKindOf` (Karrow a2 r2) = 
+  a2 `subKindOf` a1 && (r1 `subKindOf` r2)
 k1 `subKindOf` k2 = k1 `eqKind` k2  -- doesn't worry about higher kinds
 
 baseKind :: Kind -> Bool
@@ -134,17 +176,21 @@ baseKind _ = True
 isPrimVar (Just mn,_) = mn == primMname
 isPrimVar _ = False
 
-primMname = mkBaseMname "Prim"
+primMname = mkPrimMname "Prim"
 errMname  = mkBaseMname "Err"
-mkBaseMname :: Id -> AnMname
+mkBaseMname,mkPrimMname :: Id -> AnMname
 mkBaseMname mn = (basePkg, ghcPrefix, mn)
+mkPrimMname mn = (primPkg, ghcPrefix, mn)
 basePkg = "base"
 mainPkg = "main"
+primPkg = zEncodeString "ghc-prim"
 ghcPrefix = ["GHC"]
 mainPrefix = []
 baseMname = mkBaseMname "Base"
+boolMname = mkPrimMname "Bool"
 mainVar = qual mainMname "main"
 mainMname = (mainPkg, mainPrefix, "Main")
+wrapperMainMname = Just (mainPkg, mainPrefix, "ZCMain")
 
 tcArrow :: Qual Tcon
 tcArrow = (Just primMname, "ZLzmzgZR")
@@ -158,8 +204,6 @@ ktArrow = Karrow Kopen (Karrow Kopen Klifted)
 
 {- Unboxed tuples -}
 
--- tjc: not sure whether anything that follows is right
-
 maxUtuple :: Int
 maxUtuple = 100
 
@@ -178,7 +222,9 @@ isUtupleTy (Tcon tc) = tc `elem` [tcUtuple n | n <- [1..maxUtuple]]
 isUtupleTy _ = False
 
 dcUtuple :: Int -> Qual Dcon
-dcUtuple n = (Just primMname,"ZdwZ" ++ (show n) ++ "H")
+-- TODO: Seems like Z2H etc. appears in ext-core files,
+-- not $wZ2H etc. Is this right?
+dcUtuple n = (Just primMname,"Z" ++ (show n) ++ "H")
 
 isUtupleDc :: Qual Dcon -> Bool
 isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
diff --git a/utils/ext-core/Driver.hs b/utils/ext-core/Driver.hs
index b9d5556..684f31f 100644
--- a/utils/ext-core/Driver.hs
+++ b/utils/ext-core/Driver.hs
@@ -4,10 +4,15 @@
    Note that, if compiled under GHC, this requires a very large heap to run!
 -}
 
+import Control.Exception
+import Data.List
+import Maybe
 import Monad
-import System.Environment
+import Prelude hiding (catch)
 import System.Cmd
+import System.Environment
 import System.Exit
+import System.FilePath
 
 import Core
 import Printer
@@ -20,9 +25,13 @@ import Interp
 
 -- You may need to change this.
 baseDir = "../../libraries/"
---------                   
+-- change to True to typecheck library files as well as reading type signatures
+typecheckLibs = False 
+
+-- You shouldn't *need* to change anything below this line...                  
+libDir = map (baseDir ++)
 
--- Code for checking that the external and GHC printers print the same results
+-- Code to check that the external and GHC printers print the same results
 testFlag = "-t"
 
 validateResults :: FilePath -> FilePath -> IO ()
@@ -34,71 +43,135 @@ validateResults origFile genFile = do
     _             -> "Error diffing files: " ++ origFile ++ " " ++ genFile
 ------------------------------------------------------------------------------
 
-process :: Bool -> (Check.Menv,[Module]) -> String -> IO (Check.Menv,[Module])
-process doTest (senv,modules) f = 
-       do putStrLn ("Processing " ++ f)
+process :: Bool -> (Check.Menv,[Module]) -> FilePath 
+             -> IO (Check.Menv,[Module])
+process doTest (senv,modules) f = catch
+      (do putStrLn ("Processing " ++ f)
           resultOrErr <- parseCore f
 	  case resultOrErr of
-	    Right m -> do 
+	    Right m@(Module mn _ _) -> do 
                         putStrLn "Parse succeeded"
                         let outF = f ++ ".parsed"
 			writeFile outF (show m) 
                         when doTest $ (validateResults f outF)
 			case checkModule senv m of
 			  OkC senv' -> 
-			    do putStrLn "Check succeeded"
+			    do putStrLn $ "Check succeeded for " ++ show mn 
 			       let m' = prepModule senv' m
-                               {- writeFile (f ++ ".prepped") (show m') -}
-			       case checkModule senv m' of
+                               let (dir,fname) = splitFileName f
+                               let preppedFile = dir </> (fname ++ ".prepped") 
+                               writeFile preppedFile (show m') 
+			       case checkModule senv' m' of
                                  OkC senv'' ->
 				   do putStrLn "Recheck succeeded"
                                       return (senv'',modules ++ [m'])
 				 FailC s -> 
 				   do putStrLn ("Recheck failed: " ++ s)
 				      error "quit"
-			  FailC s -> 
-			    do putStrLn ("Check failed: " ++ s)
-			       error "quit"
-            Left err -> do putStrLn ("Parse failed: " ++ show err)
-                           error "quit"
+			  FailC s -> error ("Typechecking failed: " ++ s)
+            Left err -> error ("Parsing failed: " ++ show err)) handler
+   where handler e = do
+           putStrLn ("WARNING: we caught an exception " ++ show e 
+                     ++ " while processing " ++ f)
+           return (senv, modules)
 
 main = do args <- getArgs
-          let (doTest, fname) = 
+          let (doTest, fnames) = 
                  case args of
-                   (f:fn:_) | f == testFlag -> (True,fn)
-                   (fn:_)                   -> (False,fn)
+                   (f:rest) | f == testFlag -> (True,rest)
+                   rest@(_:_)                   -> (False,rest)
                    _                        -> error $ 
                                               "usage: ./Driver [filename]"
-          mapM_ (process doTest (initialEnv,[])) (libs ++ [fname])
-          (_,modules) <- foldM (process doTest) (initialEnv,[]) (libs ++ [fname])
-	  let result = evalProgram modules
-	  putStrLn ("Result = " ++ show result)
-	  putStrLn "All done"
-            where  libs = map (baseDir ++) ["./ghc-prim/GHC/Generics.hcr",
-                           "./ghc-prim/GHC/PrimopWrappers.hcr",
+          -- Note that we scan over the libraries twice:
+          -- first to gather together all type sigs, then to typecheck them
+          -- (the latter of which doesn't necessarily have to be done every time.)
+          -- This is a hack to avoid dealing with circular dependencies.
+
+          -- notice: scan over libraries *and* input modules first, not just libs
+          topEnv <- mkInitialEnv (map normalise libs `union` map normalise fnames)
+          doOneProgram doTest topEnv fnames
+            where  doOneProgram doTest topEnv fns = do
+                      putStrLn $ "========== Program " ++ (show fns) ++ " ================"
+                      let numToDo = length (typecheckLibraries fns)
+                      (_,modules) <- foldM (process doTest) (topEnv,[]) (typecheckLibraries fns)
+                      let succeeded = length modules
+                      putStrLn ("Finished typechecking. Successfully checked " ++ show succeeded
+                         ++ " out of " ++ show numToDo ++ " modules.")
+                      -- TODO: uncomment once interpreter works
+                      --let result = evalProgram modules
+                      --putStrLn ("Result = " ++ show result)
+                      putStrLn "All done\n============================================="
+
+                   typecheckLibraries = if typecheckLibs then (libs ++) else id
+                   -- Just my guess as to what's needed from the base libs.
+                   -- May well be missing some libraries and have some that
+                   -- aren't commonly used.
+                   -- However, the following is enough to check all of nofib.
+                   -- This points to how nice it would be to have explicit import lists in ext-core.
+                   libs = (libDir ["./ghc-prim/GHC/Generics.hcr",
                            "./ghc-prim/GHC/Bool.hcr",
                            "./ghc-prim/GHC/IntWord64.hcr",
                            "./base/GHC/Base.hcr",
+                           "./base/Data/Tuple.hcr",
+                           "./base/Data/Maybe.hcr",
+                           "./integer-gmp/GHC/Integer.hcr",
                            "./base/GHC/List.hcr",
                            "./base/GHC/Enum.hcr",
+                           "./base/Data/Ord.hcr",
+                           "./base/Data/String.hcr",
+                           "./base/Data/Either.hcr",
                            "./base/GHC/Show.hcr",
                            "./base/GHC/Num.hcr",
                            "./base/GHC/ST.hcr",
-                           "./base/GHC/Real.hcr",
                            "./base/GHC/STRef.hcr",
                            "./base/GHC/Arr.hcr",
-                           "./base/GHC/Float.hcr",
-                           "./base/GHC/Read.hcr",
-                           "./base/GHC/Ptr.hcr",
-                           "./base/GHC/Word.hcr",
+                           "./base/GHC/Real.hcr",
+                           "./base/Control/Monad.hcr",
                            "./base/GHC/Int.hcr",
                            "./base/GHC/Unicode.hcr",
-                           "./base/GHC/IOBase.hcr",
+                           "./base/Text/ParserCombinators/ReadP.hcr",
+                           "./base/Text/Read/Lex.hcr",
+                           "./base/Text/ParserCombinators/ReadPrec.hcr",
+                           "./base/GHC/Read.hcr",
+                           "./base/GHC/Word.hcr",
+                           "./base/Data/HashTable.hcr",
+                           "./base/Unsafe/Coerce.hcr",
+                           "./base/Foreign/Storable.hcr",
+                           "./base/Foreign/C/Types.hcr",
+                           "./base/GHC/IOBase.hcr",                           
+                           "./base/GHC/ForeignPtr.hcr",
+                           "./base/Data/Typeable.hcr",
+                           "./base/Data/Dynamic.hcr",
                            "./base/GHC/Err.hcr",
+                           "./base/Data/List.hcr",
+                           "./base/Data/Char.hcr",
+                           "./base/GHC/Pack.hcr",
+                           "./base/GHC/Storable.hcr",
+                           "./base/System/IO/Error.hcr",
+                           "./base/Foreign/Ptr.hcr",
+                           "./base/Foreign/Marshal/Error.hcr",
+                           "./base/Foreign/ForeignPtr.hcr",
+                           "./base/Foreign/Marshal/Alloc.hcr",
+                           "./base/Foreign/Marshal/Utils.hcr",
+                           "./base/Foreign/Marshal/Array.hcr",
+                           "./base/Foreign/C/String.hcr",
+                           "./base/Foreign/C/Error.hcr",
+                           "./base/Foreign/C.hcr",
+                           "./base/System/IO/Unsafe.hcr",
+                           "./base/Foreign/Marshal.hcr",
+                           "./base/Foreign/StablePtr.hcr",
+                           "./base/Foreign.hcr",
+                           "./base/System/Posix/Types.hcr",
+                           "./base/System/Posix/Internals.hcr",
+                           "./base/GHC/Conc.hcr",
+                           "./base/Control/Exception.hcr",
+                           "./base/GHC/TopHandler.hcr",
+                           "./base/Data/Bits.hcr",
+                           "./base/Numeric.hcr",
+                           "./base/GHC/Ptr.hcr",
+                           "./base/GHC/Float.hcr",
                            "./base/GHC/Exception.hcr",
                            "./base/GHC/Stable.hcr",
-                           "./base/GHC/Storable.hcr",
-                           "./base/GHC/Pack.hcr",
                            "./base/GHC/Weak.hcr",
                            "./base/GHC/Handle.hcr",
                            "./base/GHC/IO.hcr",
@@ -106,34 +179,32 @@ main = do args <- getArgs
                            "./base/GHC/Environment.hcr",
                            "./base/GHC/Exts.hcr",
                            "./base/GHC/PArr.hcr",
-                           "./base/GHC/TopHandler.hcr",
-                           "./base/GHC/Desugar.hcr",
-                           "./base/Data/Ord.hcr",
-                           "./base/Data/Maybe.hcr",
-                           "./base/Data/Bits.hcr",
-                           "./base/Data/STRef/Lazy.hcr",
+                           "./base/System/IO.hcr",
+                           "./base/System/Environment.hcr",
                            "./base/Data/Generics/Basics.hcr",
-                           "./base/Data/Generics/Aliases.hcr",
-                           "./base/Data/Generics/Twins.hcr",
-                           "./base/Data/Generics/Instances.hcr",
-                           "./base/Data/Generics/Text.hcr",
-                           "./base/Data/Generics/Schemes.hcr",
-                           "./base/Data/Tuple.hcr",
-                           "./base/Data/String.hcr",
-                           "./base/Data/Either.hcr",
-                           "./base/Data/Char.hcr",
-                           "./base/Data/List.hcr",
-                           "./base/Data/HashTable.hcr",
-                           "./base/Data/Typeable.hcr",
-                           "./base/Data/Dynamic.hcr",
-                           "./base/Data/Function.hcr",
-                           "./base/Data/IORef.hcr",
-                           "./base/Data/Fixed.hcr",
-                           "./base/Data/Monoid.hcr",
-                           "./base/Data/Ratio.hcr",
-                           "./base/Data/STRef.hcr",
-                           "./base/Data/Version.hcr",
                            "./base/Data/Complex.hcr",
-                           "./base/Data/Unique.hcr",
-                           "./base/Data/Foldable.hcr",
-                           "./base/Data/Traversable.hcr"]
\ No newline at end of file
+                           "./array/Data/Array/Base.hcr",
+                           "./base/System/Exit.hcr",
+                           "./base/Data/Ratio.hcr",
+                           "./base/Control/Monad/ST/Lazy.hcr",
+                           "./base/Prelude.hcr",
+                           "./base/Control/Concurrent/MVar.hcr",
+                           "./base/Data/Foldable.hcr"])
+
+mkInitialEnv :: [FilePath] -> IO Menv
+mkInitialEnv libs = foldM mkTypeEnv initialEnv libs
+
+mkTypeEnv :: Menv -> FilePath -> IO Menv
+mkTypeEnv globalEnv fn = catch (do
+  putStrLn $ "mkTypeEnv: reading library " ++ fn
+  resultOrErr <- parseCore fn
+  case resultOrErr of
+    Right mod@(Module mn _ _) -> do
+       let newE = envsModule globalEnv mod
+       return newE 
+    Left  err -> do putStrLn ("Failed to parse library module: " ++ show err)
+                    error "quit") handler
+  where handler e = do
+           putStrLn ("WARNING: mkTypeEnv caught an exception " ++ show e 
+                     ++ " while processing " ++ fn)
+           return globalEnv
diff --git a/utils/ext-core/Env.hs b/utils/ext-core/Env.hs
index 6f6973c..642df00 100644
--- a/utils/ext-core/Env.hs
+++ b/utils/ext-core/Env.hs
@@ -1,6 +1,6 @@
 {- Environments.
-   Uses lists for simplicity and to make the semantics clear.
-   A real implementation should use balanced trees or hash tables.
+  The original version used lists. I changed it to use Data.Map.
+  Sadly it doesn't seem to matter much. --tjc
 -}
 
 module Env (Env,
@@ -9,36 +9,41 @@ module Env (Env,
 	    eextend,
             edomain,
 	    efromlist,
+            etolist,
 	    efilter,
 	    eremove)
 where
 
-import List
+import qualified Data.Map as M
+import Data.List
 
-data Env a b = Env [(a,b)] 
- deriving (Show)
+data Env a b = Env (M.Map a b)
+ deriving Show
 
 eempty :: Env a b 
-eempty = Env []
+eempty = Env M.empty
 
 {- In case of duplicates, returns most recently added entry. -}
-elookup :: (Eq a) => Env a b -> a -> Maybe b
-elookup (Env l) k = lookup k l 
+elookup :: (Eq a, Ord a) => Env a b -> a -> Maybe b
+elookup (Env l) k = M.lookup k l 
 
 {- May hide existing entries. -}
-eextend :: Env a b -> (a,b) -> Env a b
-eextend (Env l) (k,d) = Env ((k,d):l)
+eextend :: Ord a => Env a b -> (a,b) -> Env a b
+eextend (Env l) (k,d) = Env (M.insert k d l)
 
 edomain :: (Eq a) => Env a b -> [a]
-edomain (Env l) = nub (map fst l)
+edomain (Env l) = M.keys l
 
 {- In case of duplicates, first entry hides others. -}
-efromlist :: [(a,b)] -> Env a b
-efromlist l = Env l
+efromlist :: Ord a => [(a,b)] -> Env a b
+efromlist = Env . M.fromList
 
-eremove :: (Eq a)  => Env a b -> a -> Env a b
-eremove (Env l) k = Env (filter ((/= k).fst) l)
+etolist :: Env a b -> [(a,b)]
+etolist (Env l) = M.toList l
 
-efilter :: Env a b -> (a -> Bool) -> Env a b
-efilter (Env l) p = Env (filter (p.fst) l)
+eremove :: (Eq a, Ord a)  => Env a b -> a -> Env a b
+eremove (Env l) k = Env (M.delete k l)
+
+efilter :: Ord a => Env a b -> (a -> Bool) -> Env a b
+efilter (Env l) p = Env (M.filterWithKey (\ k a -> p k) l)
 
diff --git a/utils/ext-core/Interp.hs b/utils/ext-core/Interp.hs
index f5f9857..e730012 100644
--- a/utils/ext-core/Interp.hs
+++ b/utils/ext-core/Interp.hs
@@ -15,7 +15,7 @@ The only major omission is garbage collection.
 Just a sampling of primitive types and operators are included.
 -}
 
-module Interp where
+module Interp ( evalProgram ) where
 
 import Core
 import Printer
diff --git a/utils/ext-core/Makefile b/utils/ext-core/Makefile
index e302387..7015105 100644
--- a/utils/ext-core/Makefile
+++ b/utils/ext-core/Makefile
@@ -1,5 +1,23 @@
-all:	Check.hs Core.hs Driver.hs Env.hs Interp.hs ParsecParser.hs ParseGlue.hs Prep.hs Prims.hs Printer.hs
-	ghc --make -fglasgow-exts -o Driver Driver.hs
+all:	Check.hs Core.hs Driver.hs Env.hs Interp.hs ParsecParser.hs ParseGlue.hs Prep.hs PrimCoercions.hs Prims.hs Printer.hs
+	ghc -O2 --make -fglasgow-exts -o Driver Driver.hs
+
+# Run this when the primops.txt file changes
+prims:  ../../compiler/prelude/primops.txt
+	../genprimopcode/genprimopcode --make-ext-core-source < ../../compiler/prelude/primops.txt > PrimEnv.hs
 
 #Parser.hs: Parser.y
-#	happy -ad -ihappy.debug -o Parser.hs Parser.y
\ No newline at end of file
+#	happy -ad -ihappy.debug -o Parser.hs Parser.y
+
+# The following assumes that you've built all the GHC libs with -fext-core...
+libtest: all
+	./Driver `find ../../libraries -print | grep .hcr$$ | grep -v bootstrapping`
+
+# ...or built all the nofib programs with -fext-core.
+nofibtest: all
+	./Driver `find ../../nofib -print | grep .hcr$$`
+
+clean:
+	rm -f Driver *.hi *.o
+
+reallyclean: clean
+	rm PrimEnv.hs
\ No newline at end of file
diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs
index 8602bdc..b539962 100644
--- a/utils/ext-core/ParsecParser.hs
+++ b/utils/ext-core/ParsecParser.hs
@@ -1,10 +1,14 @@
+{-# OPTIONS -Wall -Werror -fno-warn-missing-signatures #-}
+
 module ParsecParser where
 
 import Core
 import ParseGlue
+import Check
+import PrimCoercions
 
 import Text.ParserCombinators.Parsec
-import Text.ParserCombinators.Parsec.Expr
+--import Text.ParserCombinators.Parsec.Expr
 import qualified Text.ParserCombinators.Parsec.Token as P
 import Text.ParserCombinators.Parsec.Language
 import Data.Ratio
@@ -31,7 +35,9 @@ coreModuleName = do
    return (pkgName, modHierarchy, baseName)
 
 corePackageName :: Parser Pname
-corePackageName = identifier
+-- Package names can be lowercase or uppercase!
+-- TODO: update docs
+corePackageName = identifier <|> upperName
 
 coreHierModuleNames :: Parser ([Id], Id)
 coreHierModuleNames = do
@@ -83,7 +89,7 @@ coreNewtypeDecl = do
 
 coreQualifiedCon :: Parser (Mname, Id)
 coreQualifiedCon = coreQualifiedGen upperName
-
+ 
 coreQualifiedName = coreQualifiedGen identifier
 
 coreQualifiedGen p = do
@@ -110,10 +116,12 @@ coreAxiom :: Parser Axiom
 coreAxiom = parens (do
               coercionName <- coreQualifiedCon
               whiteSpace
+              tbs <- coreTbinds
+              whiteSpace
               symbol "::"
               whiteSpace
-              coercionKind <- coreKind
-              return (coercionName, coercionKind))
+              coercionK <- try equalityKind <|> parens equalityKind
+              return (coercionName, tbs, coercionK))
 
 coreTbinds :: Parser [Tbind]
 coreTbinds = many coreTbind 
@@ -145,7 +153,7 @@ coreCdef = do
   tBinds      <- try $ coreTbindsGen (symbol "@")
   -- This should be equivalent to (many coreAty)
   -- But it isn't. WHY??
-  tys         <- sepBy coreAty whiteSpace
+  tys         <- sepBy coreAtySaturated whiteSpace
   return $ Constr dataConName tBinds tys
 
 coreTRep :: Parser (Maybe Ty)
@@ -168,43 +176,71 @@ coreType = coreForallTy <|> (do
                          stuff -> foldl Tapp (Tcon tcArrow) (hd:stuff))
 
 coreBty :: Parser Ty
-coreBty = arrowThing coreAty coreAty whiteSpace Tapp
-
-arrowThing :: Parser a -> Parser a -> Parser b -> (a -> a -> a) -> Parser a
-arrowThing hdThing restThing sep op = do
-  hd <- hdThing
+coreBty = do
+  hd <- coreAty
                          -- The "try" is necessary:
                          -- otherwise, parsing "T " fails rather
                          -- than returning "T".
-  maybeRest <- option [] (many1 (try (sep >> restThing)))
-  return $ case maybeRest of 
-             [] -> hd
-             stuff -> foldl op hd maybeRest
-
-coreAppTy :: Parser Ty
-coreAppTy = do 
-  bTy <- try coreBty
-  whiteSpace
-  aTy <- try coreAty
-  return $ Tapp bTy aTy
-
-coreAty = try coreTcon <|> try coreTvar <|> parens coreType
-
+  maybeRest <- option [] (many1 (try (whiteSpace >> coreAtySaturated)))
+  return $ (case hd of
+             -- so I'm not sure I like this... it's basically doing
+             -- typechecking (kind-checking?) in the parser.
+             -- However, the type syntax as defined in Core.hs sort of
+             -- forces it.
+             ATy t     -> foldl Tapp t maybeRest
+             Trans k   -> app k 2 maybeRest "trans"
+             Sym k     -> app k 1 maybeRest "sym"
+             Unsafe k  -> app k 2 maybeRest "unsafe"
+             LeftCo k  -> app k 1 maybeRest "left"
+             RightCo k -> app k 1 maybeRest "right")
+                 where app k arity args _ | length args == arity = k args
+                       app _ _ args err = 
+                           primCoercionError (err ++ 
+                             ("Args were: " ++ show args))
+
+coreAtySaturated :: Parser Ty
+coreAtySaturated = do
+   t <- coreAty
+   case t of
+     ATy ty -> return ty
+     _     -> unexpected "coercion ty"
+
+coreAty :: Parser ATyOp
+coreAty = try coreTcon <|> ((try coreTvar <|> parens coreType)
+                             >>= return . ATy)
 coreTvar :: Parser Ty
 coreTvar = try identifier >>= (return . Tvar)
 
-coreTcon :: Parser Ty
+coreTcon :: Parser ATyOp
 -- TODO: Change the grammar
 -- A Tcon can be an uppercase type constructor
 -- or a lowercase (always qualified) coercion variable
-coreTcon = (try coreQualifiedCon <|> coreRequiredQualifiedName) 
-             >>= (return . Tcon)
-
-coreTyApp :: Parser Ty
-coreTyApp = do
-  operTy <- coreType
-  randTy <- coreType
-  return $ Tapp operTy randTy
+coreTcon =  
+         -- Special case is first so that (CoUnsafe .. ..) gets parsed as
+         -- a prim. coercion app and not a Tcon app.
+         -- But the whole thing is so bogus.
+        try (do
+                                    -- the "try"s are crucial; they force
+                                    -- backtracking
+           maybeCoercion <- choice [try symCo, try transCo, try unsafeCo,
+                                    try leftCo, rightCo]
+           return $ case maybeCoercion of
+              TransC  -> Trans (\ [x,y] -> TransCoercion x y)
+              SymC    -> Sym (\ [x] -> SymCoercion x)
+              UnsafeC -> Unsafe (\ [x,y] -> UnsafeCoercion x y)
+              LeftC   -> LeftCo (\ [x] -> LeftCoercion x)
+              RightC  -> RightCo (\ [x] -> RightCoercion x))
+    <|> (coreQualifiedCon >>= (return . ATy . Tcon))
+
+data CoercionTy = TransC | SymC | UnsafeC | LeftC | RightC
+
+symCo, transCo, unsafeCo :: Parser CoercionTy
+-- Would be better not to wire these in quite this way. Sigh
+symCo    = string "^ghczmprim:GHCziPrim.sym"      >> return SymC
+transCo  = string "^ghczmprim:GHCziPrim.trans"    >> return TransC 
+unsafeCo = string "^ghczmprim:GHCziPrim.CoUnsafe" >> return UnsafeC
+leftCo   = string "^ghczmprim:GHCziPrim.left"     >> return LeftC
+rightCo  = string "^ghczmprim:GHCziPrim.right"    >> return RightC
 
 coreFunTy :: Parser Ty
 coreFunTy = do
@@ -228,12 +264,10 @@ coreKind :: Parser Kind
 coreKind = do
   hd <- coreAtomicKind 
   maybeRest <- option [] (many1 (symbol "->" >> coreKind))
-  return $ case maybeRest of
-             [] -> hd
-             stuff -> foldl Karrow hd maybeRest
+  return $ foldl Karrow hd maybeRest
 
 coreAtomicKind = try liftedKind <|> try unliftedKind 
-       <|> try openKind <|> try (parens equalityKind) 
+       <|> try openKind {- <|> try (parens equalityKind) -}
        <|> try (parens coreKind)
 
 liftedKind = do
@@ -252,7 +286,19 @@ equalityKind = do
   ty1 <- coreBty
   symbol ":=:"
   ty2 <- coreBty
-  return $ Keq ty1 ty2
+  return (ty1, ty2)
+
+-- Only used internally within the parser:
+-- represents either a Tcon, or a continuation
+-- for a primitive coercion
+data ATyOp = 
+   ATy Ty
+ | Trans ([Ty] -> Ty)
+ | Sym ([Ty] -> Ty)
+ | Unsafe ([Ty] -> Ty)
+ | LeftCo ([Ty] -> Ty)
+ | RightCo ([Ty] -> Ty)
+
 coreVdefGroups :: Parser [Vdefg]
 coreVdefGroups = option [] (do
   theFirstVdef <- coreVdefg
@@ -290,7 +336,7 @@ coreAtomicExp = do
   return res
 
 coreFullExp = (choice [coreLam, coreLet,
-  coreCase, coreCast, coreNote, coreExternal]) <|> (try coreAppExp)
+  coreCase, coreCast, coreNote, coreExternal, coreLabel]) <|> (try coreAppExp)
 -- The "try" is necessary so that we backtrack
 -- when we see a var (that is not an app)
     <|> coreAtomicExp
@@ -306,7 +352,7 @@ coreAppExp = do
     args <- many1 (whiteSpace >> ((coreAtomicExp >>= (return . Left)) <|>
              -- note this MUST be coreAty, not coreType, because otherwise:
              -- "A @ B c" gets parsed as "A @ (B c)"
-             ((symbol "@" >> coreAty) >>= (return . Right))))
+             ((symbol "@" >> coreAtySaturated) >>= (return . Right))))
     return $ foldl (\ op ->
                      either (App op) (Appt op)) oper args
 
@@ -339,7 +385,7 @@ coreLet = do
   return $ Let vdefg body 
 coreCase = do
   reserved "case"
-  ty <- coreAty
+  ty <- coreAtySaturated
   scrut <- coreAtomicExp
   reserved "of"
   vBind <- parens lambdaBind
@@ -351,21 +397,33 @@ coreCast = do
 -- The parens are CRUCIAL, o/w it's ambiguous
   body <- try (parens coreFullExp)
   whiteSpace
-  ty <- try coreAty
+  ty <- try coreAtySaturated
   return $ Cast body ty
 coreNote = do
   reserved "note"
   s <- stringLiteral
   e <- coreFullExp
   return $ Note s e
-coreExternal = do
+coreExternal = (do
   reserved "external"
   -- TODO: This isn't in the grammar, but GHC
   -- always prints "external ccall". investigate...
   symbol "ccall"
   s <- stringLiteral
-  t <- coreAty
-  return $ External s t
+  t <- coreAtySaturated
+  return $ External s t) <|>
+    -- TODO: I don't really understand what this does
+                (do
+    reserved "dynexternal"
+    symbol "ccall"
+    t <- coreAtySaturated
+    return $ External "[dynamic]" t)
+coreLabel = do
+-- TODO: Totally punting this, but it needs to go in the grammar
+-- or not at all
+  reserved "label"
+  s <- stringLiteral
+  return $ External s tAddrzh
 
 coreLambdaBinds = many1 coreBind
 
diff --git a/utils/ext-core/Prep.hs b/utils/ext-core/Prep.hs
index 4528d54..05250af 100644
--- a/utils/ext-core/Prep.hs
+++ b/utils/ext-core/Prep.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS -Wall -fno-warn-name-shadowing #-}
 {- 
 Preprocess a module to normalize it in the following ways:
 	(1) Saturate all constructor and primop applications. 
@@ -10,14 +11,17 @@ After these preprocessing steps, Core can be interpreted (or given an operationa
 
 module Prep where
 
+import Data.Either
+
 import Prims
 import Core
-import Printer
 import Env
 import Check
 
+import Data.List
+
 primArgTys :: Env Var [Ty]
-primArgTys = efromlist (map f Prims.primVals)
+primArgTys = efromlist (map f (etolist (venv_ primEnv)))
   where f (v,t) = (v,atys)
              where (_,atys,_) = splitTy t
 
@@ -25,6 +29,7 @@ prepModule :: Menv -> Module -> Module
 prepModule globalEnv (Module mn tdefs vdefgs) = 
     Module mn tdefs vdefgs' 
   where
+
     (_,vdefgs') = foldl prepTopVdefg (eempty,[]) vdefgs
 
     prepTopVdefg (venv,vdefgs) vdefg = (venv',vdefgs ++ [vdefg'])
@@ -32,35 +37,36 @@ prepModule globalEnv (Module mn tdefs vdefgs) =
  
     prepVdefg (env@(venv,_)) (Nonrec(Vdef((Nothing,x),t,e))) = 
 	(eextend venv (x,t), Nonrec(Vdef((Nothing,x),t,prepExp env e)))
-    prepVdefg (env@(venv,_))  (Nonrec(Vdef(qx,t,e))) = 
-	(venv, Nonrec(Vdef(qx,t,prepExp env e)))
+    prepVdefg (env@(venv,_))  (Nonrec(Vdef(qx,t,e))) =
+     	(venv, Nonrec(Vdef(qx,t,prepExp env e)))
     prepVdefg (venv,tvenv) (Rec vdefs) = 
-	(venv',Rec [Vdef(qx,t,prepExp (venv',tvenv) e) | Vdef(qx,t,e) <- vdefs])
+	(venv',Rec [ Vdef(qx,t,prepExp (venv',tvenv) e) | Vdef(qx,t,e) <- vdefs])
 	where venv' = foldl eextend venv [(x,t) | Vdef((Nothing,x),t,_) <- vdefs]
 
-    prepExp env (Var qv) = Var qv
-    prepExp env (Dcon qdc) = Dcon qdc
-    prepExp env (Lit l) = Lit l
+    prepExp _ (Var qv) = Var qv
+    prepExp _ (Dcon qdc) = Dcon qdc
+    prepExp _ (Lit l) = Lit l
     prepExp env e@(App _ _) = unwindApp env e []
     prepExp env e@(Appt _ _) = unwindApp env e []
     prepExp (venv,tvenv) (Lam (Vb vb) e) = Lam (Vb vb) (prepExp (eextend venv vb,tvenv) e)
     prepExp (venv,tvenv) (Lam (Tb tb) e) = Lam (Tb tb) (prepExp (venv,eextend tvenv tb) e)
     prepExp env@(venv,tvenv) (Let (Nonrec(Vdef((Nothing,x),t,b))) e) 
-        | kindof tvenv t `eqKind` Kunlifted && suspends b =
+        | (kindOfTy tvenv t `eqKind` Kunlifted && suspends b) = 
             -- There are two places where we call the typechecker, one of them
             -- here.
             -- We need to know the type of the let body in order to construct
             -- a case expression. 
-            let eTy = typeOfExp env e in
-		Case (prepExp env b) (x,t) 
+                                -- need to extend the env with the let-bound var too!
+            let eTy = typeOfExp (eextend venv (x, t), tvenv) e in
+               Case (prepExp env b) (x,t) 
                   eTy
-                  [Adefault (prepExp (eextend venv (x,t),tvenv) e)]
+                  [Adefault (prepExp (eextend venv (x,t),tvenv) e)] 
     prepExp (venv,tvenv) (Let vdefg e) =  Let vdefg' (prepExp (venv',tvenv) e)
 		where (venv',vdefg') = prepVdefg (venv,tvenv) vdefg
     prepExp env@(venv,tvenv) (Case e vb t alts) = Case (prepExp env e) vb t (map (prepAlt (eextend venv vb,tvenv)) alts)
     prepExp env (Cast e t) = Cast (prepExp env e) t
     prepExp env (Note s e) = Note s (prepExp env e)
-    prepExp env (External s t) = External s t
+    prepExp _ (External s t) = External s t
 
     prepAlt (venv,tvenv) (Acon qdc tbs vbs e) = Acon qdc tbs vbs (prepExp (foldl eextend venv vbs,foldl eextend tvenv tbs) e)
     prepAlt env (Alit l e) = Alit l (prepExp env e)
@@ -69,7 +75,7 @@ prepModule globalEnv (Module mn tdefs vdefgs) =
 
     unwindApp env (App e1 e2) as = unwindApp env e1 (Left e2:as)
     unwindApp env (Appt e t) as  = unwindApp env e (Right t:as)
-    unwindApp env (op@(Dcon qdc)) as =
+    unwindApp env (op@(Dcon qdc)) as = 
         etaExpand (drop n atys) (rewindApp env op as)
         where (tbs,atys0,_) = splitTy (qlookup cenv_ eempty qdc)
 	      atys = map (substl (map fst tbs) ts) atys0
@@ -82,25 +88,40 @@ prepModule globalEnv (Module mn tdefs vdefgs) =
     unwindApp env op as = rewindApp env op as
 
 
-    etaExpand ts e = foldl g e [('$':(show i),t) | (i,t) <- zip [1..] ts]
-	  where g e (v,t) = Lam (Vb(v,t)) (App e (Var (unqual v)))
+    etaExpand :: [Ty] -> Exp -> Exp
+    etaExpand ts e = 
+         let args = [('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in
+	   foldr (\ (v,t) e -> Lam (Vb (v,t)) e)
+              (foldl (\ e (v,_) -> App e (Var (unqual v))) e args)
+              args
 
-    rewindApp env e [] = e
-    rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindof tvenv t `eqKind` Kunlifted && suspends e2 =
+    rewindApp _ e [] = e
+    rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindOfTy tvenv t `eqKind` Kunlifted && suspends e2 =
        -- This is the other place where we call the typechecker.
-	Case (prepExp env' e2) (v,t) (typeOfExp env rhs) [Adefault rhs]
-        where rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
-              v = freshVar venv
+        Case newScrut (v,t) (typeOfExp env' rhs) [Adefault rhs]
+        where newScrut = prepExp env e2
+              rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
+                 -- note:
+                 -- e1 gets moved inside rhs. so if we pick a case
+                 -- var name (outside e1) equal to a name bound *inside*
+                 -- e1, the binding *inside* e1 will shadow "v"
+                 -- Which would be name capture!
+                 -- So, we pass the bound vars of e1 to freshVar along with
+                 -- the domain of the current env.
+              v = freshVar (edomain venv `union` (boundVars e1))
               t = typeOfExp env e2
               env' = (eextend venv (v,t),tvenv)
     rewindApp env e1 (Left e2:as) = rewindApp env (App e1 (prepExp env e2)) as
     rewindApp env e (Right t:as) = rewindApp env (Appt e t) as
 
-    freshVar venv = maximum ("":edomain venv) ++ "x" -- one simple way!
+    freshVar vs = maximum ("":vs) ++ "x" -- one simple way!
 
     typeOfExp :: (Venv, Tvenv) -> Exp -> Ty
     typeOfExp = uncurry (checkExpr mn globalEnv tdefs)
 
+    kindOfTy :: Tvenv -> Ty -> Kind
+    kindOfTy tvenv = checkType mn globalEnv tdefs tvenv
+
     {- Return false for those expressions for which Interp.suspendExp builds a thunk. -}
     suspends (Var _) = False
     suspends (Lit _) = False
@@ -112,16 +133,6 @@ prepModule globalEnv (Module mn tdefs vdefgs) =
     suspends (External _ _) = False
     suspends _ = True
 
-    kindof :: Tvenv -> Ty -> Kind
-    kindof tvenv (Tvar tv) = 
-      case elookup tvenv tv of
-	Just k -> k
-        Nothing -> error ("impossible Tyvar " ++ show tv)
-    kindof tvenv (Tcon qtc) = qlookup tcenv_ eempty qtc
-    kindof tvenv (Tapp t1 t2) = k2
-	where Karrow _ k2 = kindof tvenv t1
-    kindof tvenv (Tforall _ t) = kindof tvenv t
-
     mlookup :: (Envs -> Env a b) -> Env a b -> Mname -> Env a b
     mlookup _ local_env Nothing = local_env
     mlookup selector _  (Just m) =   
@@ -135,3 +146,29 @@ prepModule globalEnv (Module mn tdefs vdefgs) =
         Just v -> v
         Nothing -> error ("undefined identifier: " ++ show k)
 
+boundVars :: Exp -> [Id]
+boundVars (Lam (Vb (v,_)) e) = [v] `union` boundVars e
+boundVars (Lam _ e) = boundVars e
+boundVars (Let vds e) = (boundVarsVdefs vds) `union` boundVars e
+boundVars (Case scrut (v,_) _ alts) = 
+   [v] `union` (boundVars scrut) `union` boundVarsAlts alts
+boundVars (Cast e _) = boundVars e
+boundVars (Note _ e) = boundVars e
+boundVars (App e1 e2) = boundVars e1 `union` boundVars e2
+boundVars (Appt e _) = boundVars e
+boundVars _ = []
+
+boundVarsVdefs :: Vdefg -> [Id]
+boundVarsVdefs (Rec vds) = nub (concatMap boundVarsVdef vds)
+boundVarsVdefs (Nonrec vd) = boundVarsVdef vd
+
+boundVarsVdef :: Vdef -> [Id]
+boundVarsVdef (Vdef ((_,v),_,e)) = [v] `union` boundVars e
+
+boundVarsAlts :: [Alt] -> [Var]
+boundVarsAlts as = nub (concatMap boundVarsAlt as)
+
+boundVarsAlt :: Alt -> [Var]
+boundVarsAlt (Acon _ _ vbs e) = (map fst vbs) `union` (boundVars e)
+boundVarsAlt (Alit _ e) = boundVars e
+boundVarsAlt (Adefault e) = boundVars e
\ No newline at end of file
diff --git a/utils/ext-core/PrimCoercions.hs b/utils/ext-core/PrimCoercions.hs
new file mode 100644
index 0000000..7536cb6
--- /dev/null
+++ b/utils/ext-core/PrimCoercions.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS -Wall -fno-warn-missing-signatures #-}
+module PrimCoercions where
+import Core
+
+-- Stuff the parser needs to know about
+
+pv :: a -> Qual a
+pv = qual primMname
+
+pvz :: Id -> Qual Id
+pvz = (qual primMname) . (++ "zh")
+
+{- Coercions -}
+symCoercion, transCoercion, unsafeCoercion :: Qual Tcon
+symCoercion    = pv "sym"
+transCoercion  = pv "trans"
+unsafeCoercion = pv "CoUnsafe"
+leftCoercion   = pv "left"
+rightCoercion   = pv "right"
+
+{- Addrzh -}
+tcAddrzh = pvz "Addr"
+tAddrzh = Tcon tcAddrzh
+ktAddrzh = Kunlifted
diff --git a/utils/ext-core/Prims.hs b/utils/ext-core/Prims.hs
index efcd60e..d061200 100644
--- a/utils/ext-core/Prims.hs
+++ b/utils/ext-core/Prims.hs
@@ -1,21 +1,36 @@
-{- This module really should be auto-generated from the master primops.txt file. 
-   It is roughly correct (but may be slightly incomplete) wrt/ GHC5.02. -}
+{-# OPTIONS -Wall #-}
 
-module Prims where
+{- This module contains a few primitive types that need to be wired in.
+   Most are defined in PrimEnv, which is automatically generated from
+   GHC's primops.txt. -}
+
+module Prims(initialEnv, primEnv) where
 
 import Core
 import Env
 import Check
+import PrimCoercions
+
+import PrimEnv
 
 initialEnv :: Menv
 initialEnv = efromlist [(primMname,primEnv),
 		     (errMname,errorEnv)]
 
 primEnv :: Envs
-primEnv = Envs {tcenv_=efromlist primTcs,
+-- Tediously, we add defs for ByteArray# etc. because these are
+-- declared as ByteArr# (etc.) in primops.txt, and GHC has
+-- ByteArray# etc. wired-in.
+-- At least this is better than when all primops were wired-in here.
+primEnv = Envs {tcenv_=efromlist $ map (\ (t,k) -> (t,Kind k)) $ 
+                  [(snd tcByteArrayzh,ktByteArrayzh), 
+                   (snd tcMutableArrayzh, ktMutableArrayzh),
+                   (snd tcMutableByteArrayzh, ktMutableByteArrayzh)] ++
+                 ([(snd $ tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]] 
+                   ++ ((snd tcArrow,ktArrow):primTcs)),
 		tsenv_=eempty,
 		cenv_=efromlist primDcs,
-		venv_=efromlist primVals}
+		venv_=efromlist (opsState ++ primVals)}
 
 errorEnv :: Envs
 errorEnv = Envs {tcenv_=eempty,
@@ -23,816 +38,70 @@ errorEnv = Envs {tcenv_=eempty,
 		 cenv_=eempty,
 		 venv_=efromlist errorVals}
 
-{- Components of static environment -}
-
-primTcs :: [(Tcon,Kind)]
-primTcs = 
-	map (\ ((m,tc),k) -> (tc,k))
-	([(tcArrow,ktArrow),
-	 (tcAddrzh,ktAddrzh),
-	 (tcCharzh,ktCharzh),
-	 (tcDoublezh,ktDoublezh),
-	 (tcFloatzh,ktFloatzh),
-	 (tcIntzh,ktIntzh),
-	 (tcInt32zh,ktInt32zh),
-	 (tcInt64zh,ktInt64zh),
-	 (tcWordzh,ktWordzh),
-	 (tcWord32zh,ktWord32zh),
-	 (tcWord64zh,ktWord64zh),
-	 (tcRealWorld, ktRealWorld),
-	 (tcStatezh, ktStatezh),
-	 (tcArrayzh,ktArrayzh),
-	 (tcByteArrayzh,ktByteArrayzh),
-	 (tcMutableArrayzh,ktMutableArrayzh),
-	 (tcMutableByteArrayzh,ktMutableByteArrayzh),
-	 (tcMutVarzh,ktMutVarzh),
-	 (tcMVarzh,ktMVarzh),
-	 (tcWeakzh,ktWeakzh),
-	 (tcForeignObjzh, ktForeignObjzh),
-	 (tcStablePtrzh, ktStablePtrzh),
-	 (tcThreadIdzh, ktThreadIdzh),
-	 (tcZCTCCallable, ktZCTCCallable),
-	 (tcZCTCReturnable, ktZCTCReturnable)]
-       ++ [(tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]])
-
 
 primDcs :: [(Dcon,Ty)]
-primDcs = map (\ ((m,c),t) -> (c,t))
+primDcs = map (\ ((_,c),t) -> (c,t))
 	      [(dcUtuple n, dcUtupleTy n) | n <- [1..maxUtuple]]
 
-primVals :: [(Var,Ty)]
-primVals = 
-	opsAddrzh ++
-	opsCharzh ++
-	opsDoublezh ++
-	opsFloatzh ++
-	opsIntzh ++
-	opsInt32zh ++
-	opsInt64zh ++
-	opsIntegerzh ++
-	opsWordzh ++
-	opsWord32zh ++
-	opsWord64zh ++
-	opsSized ++
-	opsArray ++
-	opsMutVarzh ++
-	opsState ++
-	opsExn ++
-	opsMVar ++
-	opsWeak ++
-	opsForeignObjzh ++
-        opsStablePtrzh ++
-	opsConc ++
-	opsMisc
-
-
-dcUtuples :: [(Qual Dcon,Ty)]
-dcUtuples = map ( \n -> (dcUtuple n, typ n)) [1..100]
-     where typ n = foldr ( \tv t -> Tforall (tv,Kopen) t)
-				(foldr ( \tv t -> tArrow (Tvar tv) t)
-					     (tUtuple (map Tvar tvs)) tvs) tvs
-		      where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
-
-pv = qual primMname
-pvz = (qual primMname) . (++ "zh")
-
-{- Addrzh -}
-tcAddrzh = pvz "Addr"
-tAddrzh = Tcon tcAddrzh
-ktAddrzh = Kunlifted
-
-opsAddrzh = [
- ("gtAddrzh",tcompare tAddrzh),
- ("geAddrzh",tcompare tAddrzh), 
- ("eqAddrzh",tcompare tAddrzh),  
- ("neAddrzh",tcompare tAddrzh),
- ("ltAddrzh",tcompare tAddrzh),  
- ("leAddrzh",tcompare tAddrzh),
- ("nullAddrzh", tAddrzh),
- ("plusAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
- ("minusAddrzh", tArrow tAddrzh (tArrow tAddrzh tIntzh)),
- ("remAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh))]
-
-{- Charzh -}
-
-tcCharzh = pvz "Char"
-tCharzh = Tcon tcCharzh
-ktCharzh = Kunlifted
-
-opsCharzh = [
- ("gtCharzh", tcompare tCharzh),
- ("geCharzh", tcompare tCharzh),
- ("eqCharzh", tcompare tCharzh),
- ("neCharzh", tcompare tCharzh),
- ("ltCharzh", tcompare tCharzh),
- ("leCharzh", tcompare tCharzh),
- ("ordzh",    tArrow tCharzh tIntzh)]
-
-
-{- Doublezh -}
-
-tcDoublezh = pvz "Double"
-tDoublezh = Tcon tcDoublezh
-ktDoublezh = Kunlifted
-
-opsDoublezh = [
- ("zgzhzh", tcompare tDoublezh),
- ("zgzezhzh", tcompare tDoublezh),
- ("zezezhzh", tcompare tDoublezh),
- ("zszezhzh", tcompare tDoublezh),
- ("zlzhzh", tcompare tDoublezh),
- ("zlzezhzh", tcompare tDoublezh),
- ("zpzhzh", tdyadic tDoublezh),
- ("zmzhzh", tdyadic tDoublezh),
- ("ztzhzh", tdyadic tDoublezh),
- ("zszhzh", tdyadic tDoublezh),
- ("negateDoublezh", tmonadic tDoublezh),
- ("double2Intzh", tArrow tDoublezh tIntzh),
- ("double2Floatzh", tArrow tDoublezh tFloatzh),
- ("expDoublezh", tmonadic tDoublezh),
- ("logDoublezh", tmonadic tDoublezh),
- ("sqrtDoublezh", tmonadic tDoublezh),
- ("sinDoublezh", tmonadic tDoublezh),
- ("cosDoublezh", tmonadic tDoublezh),
- ("tanDoublezh", tmonadic tDoublezh),
- ("asinDoublezh", tmonadic tDoublezh),
- ("acosDoublezh", tmonadic tDoublezh),
- ("atanDoublezh", tmonadic tDoublezh),
- ("sinhDoublezh", tmonadic tDoublezh),
- ("coshDoublezh", tmonadic tDoublezh),
- ("tanhDoublezh", tmonadic tDoublezh),
- ("ztztzhzh", tdyadic tDoublezh),
- ("decodeDoublezh", tArrow tDoublezh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
-
-
-{- Floatzh -}
-
-tcFloatzh = pvz "Float"
-tFloatzh = Tcon tcFloatzh
-ktFloatzh = Kunlifted
-
-opsFloatzh = [
- ("gtFloatzh", tcompare tFloatzh),
- ("geFloatzh", tcompare tFloatzh),
- ("eqFloatzh", tcompare tFloatzh),
- ("neFloatzh", tcompare tFloatzh),
- ("ltFloatzh", tcompare tFloatzh),
- ("leFloatzh", tcompare tFloatzh),
- ("plusFloatzh", tdyadic tFloatzh),
- ("minusFloatzh", tdyadic tFloatzh),
- ("timesFloatzh", tdyadic tFloatzh),
- ("divideFloatzh", tdyadic tFloatzh),
- ("negateFloatzh", tmonadic tFloatzh),
- ("float2Intzh", tArrow tFloatzh tIntzh),
- ("expFloatzh", tmonadic tFloatzh),
- ("logFloatzh", tmonadic tFloatzh),
- ("sqrtFloatzh", tmonadic tFloatzh),
- ("sinFloatzh", tmonadic tFloatzh),
- ("cosFloatzh", tmonadic tFloatzh),
- ("tanFloatzh", tmonadic tFloatzh),
- ("asinFloatzh", tmonadic tFloatzh),
- ("acosFloatzh", tmonadic tFloatzh),
- ("atanFloatzh", tmonadic tFloatzh),
- ("sinhFloatzh", tmonadic tFloatzh),
- ("coshFloatzh", tmonadic tFloatzh),
- ("tanhFloatzh", tmonadic tFloatzh),
- ("powerFloatzh", tdyadic tFloatzh),
- ("float2Doublezh", tArrow tFloatzh tDoublezh),
- ("decodeFloatzh", tArrow tFloatzh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
-
-
-{- Intzh -}
-
-tcIntzh = pvz "Int"
-tIntzh = Tcon tcIntzh
-ktIntzh = Kunlifted
-
-opsIntzh = [
- ("zpzh", tdyadic tIntzh),
- ("zmzh", tdyadic tIntzh),
- ("ztzh", tdyadic tIntzh),
- ("quotIntzh", tdyadic tIntzh),
- ("remIntzh", tdyadic tIntzh),
- ("gcdIntzh", tdyadic tIntzh),
- ("negateIntzh", tmonadic tIntzh),
- ("addIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("subIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("mulIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("zgzh", tcompare tIntzh),
- ("zgzezh", tcompare tIntzh),
- ("zezezh", tcompare tIntzh),
- ("zszezh", tcompare tIntzh),
- ("zlzh", tcompare tIntzh),
- ("zlzezh", tcompare tIntzh),
- ("chrzh", tArrow tIntzh tCharzh),
- ("int2Wordzh", tArrow tIntzh tWordzh),
- ("int2Floatzh", tArrow tIntzh tFloatzh),
- ("int2Doublezh", tArrow tIntzh tDoublezh),
- ("intToInt32zh", tArrow tIntzh tInt32zh),
- ("int2Integerzh", tArrow tIntzh tIntegerzhRes),
- ("iShiftLzh", tdyadic tIntzh),
- ("iShiftRAzh", tdyadic tIntzh),
- ("iShiftRLh", tdyadic tIntzh)]
-
-
-{- Int32zh -}
-
-tcInt32zh = pvz "Int32"
-tInt32zh = Tcon tcInt32zh
-ktInt32zh = Kunlifted
-
-opsInt32zh = [
- ("int32ToIntzh", tArrow tInt32zh tIntzh),
- ("int32ToIntegerzh", tArrow tInt32zh tIntegerzhRes)]
-
-
-{- Int64zh -}
-
-tcInt64zh = pvz "Int64"
-tInt64zh = Tcon tcInt64zh
-ktInt64zh = Kunlifted
-
-opsInt64zh = [
- ("int64ToIntegerzh", tArrow tInt64zh tIntegerzhRes)]
-
-{- Integerzh -}
-
--- not actuallly a primitive type
-tIntegerzhRes = tUtuple [tIntzh, tByteArrayzh]
-tIntegerzhTo t = tArrow tIntzh (tArrow tByteArrayzh t)
-tdyadicIntegerzh = tIntegerzhTo (tIntegerzhTo tIntegerzhRes)
-
-opsIntegerzh = [
- ("plusIntegerzh", tdyadicIntegerzh),
- ("minusIntegerzh", tdyadicIntegerzh),
- ("timesIntegerzh", tdyadicIntegerzh),
- ("gcdIntegerzh", tdyadicIntegerzh),
- ("gcdIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
- ("divExactIntegerzh", tdyadicIntegerzh),
- ("quotIntegerzh", tdyadicIntegerzh),
- ("remIntegerzh", tdyadicIntegerzh),
- ("cmpIntegerzh", tIntegerzhTo (tIntegerzhTo tIntzh)),
- ("cmpIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
- ("quotRemIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
- ("divModIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
- ("integer2Intzh", tIntegerzhTo tIntzh),
- ("integer2Wordzh", tIntegerzhTo tWordzh),
- ("integerToInt32zh", tIntegerzhTo tInt32zh),
- ("integerToWord32zh", tIntegerzhTo tWord32zh),
- ("integerToInt64zh", tIntegerzhTo tInt64zh),
- ("integerToWord64zh", tIntegerzhTo tWord64zh),
- ("andIntegerzh", tdyadicIntegerzh),
- ("orIntegerzh", tdyadicIntegerzh),
- ("xorIntegerzh", tdyadicIntegerzh),
- ("complementIntegerzh", tIntegerzhTo tIntegerzhRes)]
-
-
-
-{- Wordzh -}
-
-tcWordzh = pvz "Word"
-tWordzh = Tcon tcWordzh
-ktWordzh = Kunlifted
-
-opsWordzh = [
- ("plusWordzh", tdyadic tWordzh),
- ("minusWordzh", tdyadic tWordzh),
- ("timesWordzh", tdyadic tWordzh),
- ("quotWordzh",   tdyadic tWordzh),
- ("remWordzh",   tdyadic tWordzh),
- ("andzh",    tdyadic tWordzh),
- ("orzh",    tdyadic tWordzh),
- ("xorzh",    tdyadic tWordzh),
- ("notzh",    tmonadic tWordzh),
- ("shiftLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
- ("shiftRLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
- ("word2Intzh", tArrow tWordzh tIntzh),
- ("wordToWord32zh", tArrow tWordzh tWord32zh),
- ("word2Integerzh", tArrow tWordzh tIntegerzhRes),
- ("gtWordzh", tcompare tWordzh),
- ("geWordzh", tcompare tWordzh),
- ("eqWordzh", tcompare tWordzh),
- ("neWordzh", tcompare tWordzh),
- ("ltWordzh", tcompare tWordzh),
- ("leWordzh", tcompare tWordzh)]
-
-{- Word32zh -}
-
-tcWord32zh = pvz "Word32"
-tWord32zh = Tcon tcWord32zh
-ktWord32zh = Kunlifted
-
-opsWord32zh = [
- ("word32ToWordzh", tArrow tWord32zh tWordzh),
- ("word32ToIntegerzh", tArrow tWord32zh tIntegerzhRes)]
-
-{- Word64zh -}
-
-tcWord64zh = pvz "Word64"
-tWord64zh = Tcon tcWord64zh
-ktWord64zh = Kunlifted
-
-opsWord64zh = [
- ("word64ToIntegerzh", tArrow tWord64zh tIntegerzhRes)]
-
-{- Explicitly sized Intzh and Wordzh -}
+tRWS :: Ty
+tRWS = tStatezh tRealWorld
 
-opsSized = [
- ("narrow8Intzh", tmonadic tIntzh),
- ("narrow16Intzh", tmonadic tIntzh),
- ("narrow32Intzh", tmonadic tIntzh),
- ("narrow8Wordzh", tmonadic tWordzh),
- ("narrow16Wordzh", tmonadic tWordzh),
- ("narrow32Wordzh", tmonadic tWordzh)]
+opsState :: [(Var, Ty)]
+opsState = [
+  ("realWorldzh", tRWS)]
 
 {- Arrays -}
 
-tcArrayzh = pvz "Array"
-tArrayzh t = Tapp (Tcon tcArrayzh) t
-ktArrayzh = Karrow Klifted Kunlifted
+tcByteArrayzh, tcMutableArrayzh, tcMutableByteArrayzh :: Qual Tcon
+ktByteArrayzh, ktMutableArrayzh, ktMutableByteArrayzh :: Kind
 
 tcByteArrayzh = pvz "ByteArray"
-tByteArrayzh = Tcon tcByteArrayzh
 ktByteArrayzh = Kunlifted
 
 tcMutableArrayzh = pvz "MutableArray"
-tMutableArrayzh s t = Tapp (Tapp (Tcon tcMutableArrayzh) s) t
 ktMutableArrayzh = Karrow Klifted (Karrow Klifted Kunlifted)
 
 tcMutableByteArrayzh = pvz "MutableByteArray"
-tMutableByteArrayzh s = Tapp (Tcon tcMutableByteArrayzh) s
 ktMutableByteArrayzh = Karrow Klifted Kunlifted
 
-opsArray = [
- ("newArrayzh", Tforall ("a",Klifted) 
-		       (Tforall ("s",Klifted)
-                                (tArrow tIntzh 
-                                       (tArrow (Tvar "a")
-                                               (tArrow (tStatezh (Tvar "s"))
-                                                       (tUtuple [tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")])))))),
- ("newByteArrayzh", Tforall ("s",Klifted)
-                           (tArrow tIntzh 
-                                   (tArrow (tStatezh (Tvar "s"))
-                                           (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
- ("newPinnedByteArrayzh", Tforall ("s",Klifted)
-                           (tArrow tIntzh 
-                                   (tArrow (tStatezh (Tvar "s"))
-                                           (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
- ("byteArrayContentszh", tArrow tByteArrayzh tAddrzh),
- ("indexCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
- ("indexWideCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
- ("indexIntArrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexWordArrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexAddrArrayzh", tArrow tByteArrayzh (tArrow tIntzh tAddrzh)),
- ("indexFloatArrayzh", tArrow tByteArrayzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleArrayzh", tArrow tByteArrayzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrArrayzh", Tforall ("a",Klifted) (tArrow tByteArrayzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexInt16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexInt32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt32zh)),
- ("indexInt64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt64zh)),
- ("indexWord8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexWord16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexWord32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord32zh)),
- ("indexWord64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord64zh)),
- ("readCharArrayzh", tReadMutableByteArrayzh tCharzh),
- ("readWideCharArrayzh", tReadMutableByteArrayzh tCharzh),
- ("readIntArrayzh", tReadMutableByteArrayzh tIntzh),
- ("readWordArrayzh", tReadMutableByteArrayzh tWordzh),
- ("readAddrArrayzh", tReadMutableByteArrayzh tAddrzh),
- ("readFloatArrayzh", tReadMutableByteArrayzh tFloatzh),
- ("readDoubleArrayzh", tReadMutableByteArrayzh tDoublezh),
- ("readStablePtrArrayzh", Tforall ("s",Klifted)
-				 (Tforall ("a",Klifted)
-					  (tArrow (tMutableByteArrayzh (Tvar "s"))
-				                  (tArrow tIntzh
-				                         (tArrow (tStatezh (Tvar "s"))
-				                                 (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
- ("readInt8Arrayzh", tReadMutableByteArrayzh tIntzh),
- ("readInt16Arrayzh", tReadMutableByteArrayzh tIntzh),
- ("readInt32Arrayzh", tReadMutableByteArrayzh tInt32zh),
- ("readInt64Arrayzh", tReadMutableByteArrayzh tInt64zh),
- ("readWord8Arrayzh", tReadMutableByteArrayzh tWordzh),
- ("readWord16Arrayzh", tReadMutableByteArrayzh tWordzh),
- ("readWord32Arrayzh", tReadMutableByteArrayzh tWord32zh),
- ("readWord64Arrayzh", tReadMutableByteArrayzh tWord64zh),
-
- ("writeCharArrayzh", tWriteMutableByteArrayzh tCharzh),
- ("writeWideCharArrayzh", tWriteMutableByteArrayzh tCharzh),
- ("writeIntArrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeWordArrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeAddrArrayzh", tWriteMutableByteArrayzh tAddrzh),
- ("writeFloatArrayzh", tWriteMutableByteArrayzh tFloatzh),
- ("writeDoubleArrayzh", tWriteMutableByteArrayzh tDoublezh),
- ("writeStablePtrArrayzh", Tforall ("s",Klifted)
-				  (Tforall ("a",Klifted)
-				           (tArrow (tMutableByteArrayzh (Tvar "s"))
-				                   (tArrow tIntzh
-				                          (tArrow (tStablePtrzh (Tvar "a"))
-			  		                          (tArrow (tStatezh (Tvar "s"))
-				                                          (tStatezh (Tvar "s")))))))),
- ("writeInt8Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt16Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt32Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt64Arrayzh", tWriteMutableByteArrayzh tInt64zh),
- ("writeWord8Arrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeWord16Arrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeWord32Arrayzh", tWriteMutableByteArrayzh tWord32zh),
- ("writeWord64Arrayzh", tWriteMutableByteArrayzh tWord64zh),
-
- ("indexCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
- ("indexWideCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
- ("indexIntOffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexWordOffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexAddrOffAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
- ("indexFloatOffAddrzh", tArrow tAddrzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleOffAddrzh", tArrow tAddrzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrOffAddrzh", Tforall ("a",Klifted) (tArrow tAddrzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexInt16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexInt32OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt32zh)),
- ("indexInt64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt64zh)),
- ("indexWord8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexWord16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexWord32ffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord32zh)),
- ("indexWord64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord64zh)),
-
- ("indexCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
- ("indexWideCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
- ("indexIntOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexWordOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexAddrOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tAddrzh)),
- ("indexFloatOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrOffForeignObjzh", Tforall ("a",Klifted) (tArrow tForeignObjzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexInt16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexInt32OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt32zh)),
- ("indexInt64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt64zh)),
- ("indexWord8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexWord16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexWord32ffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord32zh)),
- ("indexWord64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord64zh)),
-
- ("readCharOffAddrzh", tReadOffAddrzh tCharzh),
- ("readWideCharOffAddrzh", tReadOffAddrzh tCharzh),
- ("readIntOffAddrzh", tReadOffAddrzh tIntzh),
- ("readWordOffAddrzh", tReadOffAddrzh tWordzh),
- ("readAddrOffAddrzh", tReadOffAddrzh tAddrzh),
- ("readFloatOffAddrzh", tReadOffAddrzh tFloatzh),
- ("readDoubleOffAddrzh", tReadOffAddrzh tDoublezh),
- ("readStablePtrOffAddrzh", Tforall ("s",Klifted) 
-				(Tforall ("a",Klifted)
-			             (tArrow tAddrzh
-			                     (tArrow tIntzh
-                        			    (tArrow (tStatezh (Tvar "s"))
-			                                    (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
- ("readInt8OffAddrzh", tReadOffAddrzh tIntzh),
- ("readInt16OffAddrzh", tReadOffAddrzh tIntzh),
- ("readInt32OffAddrzh", tReadOffAddrzh tInt32zh),
- ("readInt64OffAddrzh", tReadOffAddrzh tInt64zh),
- ("readWord8OffAddrzh", tReadOffAddrzh tWordzh),
- ("readWord16OffAddrzh", tReadOffAddrzh tWordzh),
- ("readWord32OffAddrzh", tReadOffAddrzh tWord32zh),
- ("readWord64OffAddrzh", tReadOffAddrzh tWord64zh),
-
- ("writeCharOffAddrzh", tWriteOffAddrzh tCharzh),
- ("writeWideCharOffAddrzh", tWriteOffAddrzh tCharzh),
- ("writeIntOffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeWordOffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeAddrOffAddrzh", tWriteOffAddrzh tAddrzh),
- ("writeFloatOffAddrzh", tWriteOffAddrzh tFloatzh),
- ("writeDoubleOffAddrzh", tWriteOffAddrzh tDoublezh),
- ("writeStablePtrOffAddrzh", Tforall ("a",Klifted) (tWriteOffAddrzh (tStablePtrzh (Tvar "a")))),
- ("writeInt8OffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeInt16OffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeInt32OffAddrzh", tWriteOffAddrzh tInt32zh),
- ("writeInt64OffAddrzh", tWriteOffAddrzh tInt64zh),
- ("writeWord8OffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeWord16OffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeWord32OffAddrzh", tWriteOffAddrzh tWord32zh),
- ("writeWord64OffAddrzh", tWriteOffAddrzh tWord64zh),
- 
- ("sameMutableArrayzh", Tforall ("s",Klifted)
-                               (Tforall ("a",Klifted)
-                                        (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
-                                                (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
-                                                        tBool)))),
- ("sameMutableByteArrayzh", Tforall ("s",Klifted)
-                                   (tArrow (tMutableByteArrayzh (Tvar "s"))
-                                           (tArrow (tMutableByteArrayzh (Tvar "s"))
-                                                   tBool))),
- ("readArrayzh",Tforall ("s",Klifted)
-                        (Tforall ("a",Klifted)
-                                 (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
-			                 (tArrow tIntzh
-					         (tArrow (tStatezh (Tvar "s"))
-                                                         (tUtuple[tStatezh (Tvar "s"), Tvar "a"])))))),
- ("writeArrayzh",Tforall ("s",Klifted)
-                         (Tforall ("a",Klifted)
-                                  (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
-			                  (tArrow tIntzh
-				  	          (tArrow (Tvar "a")
-					                  (tArrow (tStatezh (Tvar "s"))
-                                                                  (tStatezh (Tvar "s")))))))),
- ("indexArrayzh", Tforall ("a",Klifted)
-                          (tArrow (tArrayzh (Tvar "a"))
-                                  (tArrow tIntzh
-                                          (tUtuple[Tvar "a"])))),
- ("unsafeFreezzeArrayzh",Tforall ("s",Klifted)
-                                (Tforall ("a",Klifted)
-                                         (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
-						 (tArrow (tStatezh (Tvar "s"))
-                                                         (tUtuple[tStatezh (Tvar "s"),tArrayzh (Tvar "a")]))))),
- ("unsafeFreezzeByteArrayzh",Tforall ("s",Klifted)
-                                    (tArrow (tMutableByteArrayzh (Tvar "s"))
-				     	    (tArrow (tStatezh (Tvar "s"))
-                                                    (tUtuple[tStatezh (Tvar "s"),tByteArrayzh])))),
- ("unsafeThawArrayzh",Tforall ("a",Klifted)
-                             (Tforall ("s",Klifted)
-                                      (tArrow (tArrayzh (Tvar "a"))
-					      (tArrow (tStatezh (Tvar "s"))
-                                                      (tUtuple[tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")]))))),
- ("sizzeofByteArrayzh", tArrow tByteArrayzh tIntzh), 
- ("sizzeofMutableByteArrayzh", Tforall ("s",Klifted) (tArrow (tMutableByteArrayzh (Tvar "s")) tIntzh))]
- where
- tReadMutableByteArrayzh t = 
-     Tforall ("s",Klifted)
-             (tArrow (tMutableByteArrayzh (Tvar "s"))
-                     (tArrow tIntzh
-                            (tArrow (tStatezh (Tvar "s"))
-                                    (tUtuple [tStatezh (Tvar "s"),t]))))
-
- tWriteMutableByteArrayzh t = 
-     Tforall ("s",Klifted)
-             (tArrow (tMutableByteArrayzh (Tvar "s"))
-                     (tArrow tIntzh
-                            (tArrow t
-                                    (tArrow (tStatezh (Tvar "s"))
-                                            (tStatezh (Tvar "s"))))))
-
- tReadOffAddrzh t = 
-     Tforall ("s",Klifted)
-             (tArrow tAddrzh
-                     (tArrow tIntzh
-                            (tArrow (tStatezh (Tvar "s"))
-                                    (tUtuple [tStatezh (Tvar "s"),t]))))
-
-
- tWriteOffAddrzh t = 
-     Tforall ("s",Klifted)
-             (tArrow tAddrzh
-                     (tArrow tIntzh
-                            (tArrow t
-                                    (tArrow (tStatezh (Tvar "s"))
-                                            (tStatezh (Tvar "s"))))))
-
-{- MutVars -}
-
-tcMutVarzh = pvz "MutVar"
-tMutVarzh s t = Tapp (Tapp (Tcon tcMutVarzh) s) t
-ktMutVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
-
-opsMutVarzh = [
- ("newMutVarzh", Tforall ("a",Klifted)    
-                    (Tforall ("s",Klifted)
-                        (tArrow (Tvar "a") (tArrow (tStatezh (Tvar "s"))
-						   (tUtuple [tStatezh (Tvar "s"),
-						             tMutVarzh (Tvar "s") (Tvar "a")]))))),
- ("readMutVarzh", Tforall ("s",Klifted)
-		    (Tforall ("a",Klifted)
-                        (tArrow (tMutVarzh (Tvar "s")(Tvar "a"))
-				(tArrow (tStatezh (Tvar "s"))
-                                        (tUtuple [tStatezh (Tvar "s"), Tvar "a"]))))),
- ("writeMutVarzh", Tforall ("s",Klifted)
-		    (Tforall ("a",Klifted)
-                        (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
-				(tArrow (Tvar "a")
-                                        (tArrow (tStatezh (Tvar "s"))
-                                                (tStatezh (Tvar "s"))))))),
- ("sameMutVarzh", Tforall ("s",Klifted)
-	   	    (Tforall ("a",Klifted)
-                        (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
-				(tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
-				        tBool))))]
-
 {- Real world and state. -}
 
 -- tjc: why isn't this one unboxed?
+tcRealWorld :: Qual Tcon
 tcRealWorld = pv "RealWorld"
+tRealWorld :: Ty
 tRealWorld = Tcon tcRealWorld
-ktRealWorld = Klifted
 
+tcStatezh :: Qual Tcon
 tcStatezh = pvz "State"
+tStatezh :: Ty -> Ty
 tStatezh t = Tapp (Tcon tcStatezh) t
-ktStatezh = Karrow Klifted Kunlifted
-
-tRWS = tStatezh tRealWorld
-
-opsState = [
-  ("realWorldzh", tRWS)]
-
-{- Exceptions -}
-
--- no primitive type
-opsExn = [
- ("catchzh", 
-	let t' = tArrow tRWS (tUtuple [tRWS, Tvar "a"]) in
-	Tforall ("a",Klifted)
-		(Tforall ("b",Klifted)
-			 (tArrow t'
-				 (tArrow (tArrow (Tvar "b") t') 
-                                         t')))),
-  ("raisezh", Tforall ("a",Klifted)
-		      (Tforall ("b",Klifted)
-			       (tArrow (Tvar "a") (Tvar "b")))),
-  ("blockAsyncExceptionszh", Tforall ("a",Klifted)			
-                                    (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
-					    (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
-  ("unblockAsyncExceptionszh", Tforall ("a",Klifted)			
-                                    (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
-					    (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))))]
-
-{- Mvars -} 
-
-tcMVarzh = pvz "MVar"
-tMVarzh s t = Tapp (Tapp (Tcon tcMVarzh) s) t
-ktMVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
-
-opsMVar = [
- ("newMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-                               (tArrow (tStatezh (Tvar "s"))
-				       (tUtuple[tStatezh (Tvar "s"),tMVarzh (Tvar "s") (Tvar "a")])))),
- ("takeMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (tStatezh (Tvar "s"))
-					       (tUtuple[tStatezh (Tvar "s"),Tvar "a"]))))),
- ("tryTakeMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (tStatezh (Tvar "s"))
-					       (tUtuple[tStatezh (Tvar "s"),tIntzh,Tvar "a"]))))),
- ("putMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (Tvar "a")
-				               (tArrow (tStatezh (Tvar "s"))
-					               (tStatezh (Tvar "s"))))))),
- ("tryPutMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (Tvar "a")
-				               (tArrow (tStatezh (Tvar "s"))
-					               (tUtuple [tStatezh (Tvar "s"), tIntzh])))))),
- ("sameMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-					       tBool)))),
- ("isEmptyMVarzh", Tforall ("s",Klifted)
-		      (Tforall ("a",Klifted)
-			       (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
-				       (tArrow (tStatezh (Tvar "s"))
-					       (tUtuple[tStatezh (Tvar "s"),tIntzh])))))]
-
-
-{- Weak Objects -}
 
-tcWeakzh = pvz "Weak"
-tWeakzh t = Tapp (Tcon tcWeakzh) t
-ktWeakzh = Karrow Klifted Kunlifted
-
-opsWeak = [
-  ("mkWeakzh", Tforall ("o",Kopen)
-                      (Tforall ("b",Klifted)
-			       (Tforall ("c",Klifted)
-					(tArrow (Tvar "o")
-					        (tArrow (Tvar "b")
-							(tArrow (Tvar "c")
-			                                        (tArrow tRWS (tUtuple[tRWS, tWeakzh (Tvar "b")])))))))),
-  ("deRefWeakzh", Tforall ("a",Klifted)
-			 (tArrow (tWeakzh (Tvar "a"))
-			         (tArrow tRWS (tUtuple[tRWS, tIntzh, Tvar "a"])))),
-  ("finalizeWeakzh", Tforall ("a",Klifted)
-			    (tArrow (tWeakzh (Tvar "a"))
-                                    (tArrow tRWS
-					    (tUtuple[tRWS,tIntzh,
-						     tArrow tRWS (tUtuple[tRWS, tUnit])]))))]
-
-
-{- Foreign Objects -}
-
-tcForeignObjzh = pvz "ForeignObj"
-tForeignObjzh = Tcon tcForeignObjzh
-ktForeignObjzh = Kunlifted
-
-opsForeignObjzh = [
- ("mkForeignObjzh", tArrow tAddrzh
-		           (tArrow tRWS (tUtuple [tRWS,tForeignObjzh]))),
- ("writeForeignObjzh", Tforall ("s",Klifted) 
-		               (tArrow tForeignObjzh
-			               (tArrow tAddrzh
-				               (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s")))))),
- ("foreignObjToAddrzh", tArrow tForeignObjzh tAddrzh),
- ("touchzh", Tforall ("o",Kopen)
-		     (tArrow (Tvar "o")
-			     (tArrow tRWS tRWS)))]
-
-
-{- Stable Pointers (but not names) -}
-
-tcStablePtrzh = pvz "StablePtr"
-tStablePtrzh t = Tapp (Tcon tcStablePtrzh) t
-ktStablePtrzh = Karrow Klifted Kunlifted
-
-opsStablePtrzh = [
-  ("makeStablePtrzh", Tforall ("a",Klifted) 
-			     (tArrow (Tvar "a")
-				     (tArrow tRWS (tUtuple[tRWS,tStablePtrzh (Tvar "a")])))),
-  ("deRefStablePtrzh", Tforall ("a",Klifted)
-			      (tArrow (tStablePtrzh (Tvar "a"))
-				      (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
-  ("eqStablePtrzh", Tforall ("a",Klifted)
-			   (tArrow (tStablePtrzh (Tvar "a"))
-                                   (tArrow (tStablePtrzh (Tvar "a")) tIntzh)))]
-
-{- Concurrency  operations -}
-
-tcThreadIdzh = pvz "ThreadId"
-tThreadIdzh = Tcon tcThreadIdzh
-ktThreadIdzh = Kunlifted
-
-opsConc = [
-  ("seqzh", Tforall ("a",Klifted)
-		    (tArrow (Tvar "a") tIntzh)),
-  ("parzh", Tforall ("a",Klifted)
-		    (tArrow (Tvar "a") tIntzh)),
-  ("delayzh", Tforall ("s",Klifted)
-		     (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
-  ("waitReadzh", Tforall ("s",Klifted)
-		     (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
-  ("waitWritezh", Tforall ("s",Klifted)
-		     (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
-  ("forkzh", Tforall ("a",Klifted)
-		    (tArrow (Tvar "a") 
-			    (tArrow tRWS (tUtuple[tRWS,tThreadIdzh])))),
-  ("killThreadzh", Tforall ("a",Klifted)
-		          (tArrow tThreadIdzh
-			          (tArrow (Tvar "a")
-                                          (tArrow tRWS tRWS)))),
-  ("yieldzh", tArrow tRWS tRWS),
-  ("myThreadIdzh", tArrow tRWS (tUtuple[tRWS, tThreadIdzh]))]
-
-{- Miscellaneous operations -}
-
-opsMisc =  [
-  ("dataToTagzh", Tforall ("a",Klifted) 
-			  (tArrow (Tvar "a") tIntzh)),
-  ("tagToEnumzh", Tforall ("a",Klifted)
-                          (tArrow tIntzh (Tvar "a"))),
-  ("unsafeCoercezh", Tforall ("a",Kopen) 
-                             (Tforall ("b",Kopen) 
-                                      (tArrow (Tvar "a") (Tvar "b")))) -- maybe unneeded
-  ]
-
-{- CCallable and CReturnable.
-   We just define the type constructors for the dictionaries
-   corresponding to these pseudo-classes. -}
-
-tcZCTCCallable = pv "ZCTCCallable"
-ktZCTCCallable = Karrow Kopen Klifted  -- ??
-tcZCTCReturnable = pv "ZCTCReturnable"
-ktZCTCReturnable = Karrow Kopen Klifted  -- ??
+{- Properly defined in PrelError, but needed in many modules before that. -}
+errorVals :: [(Var, Ty)]
+errorVals = [
+ ("error", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
+ ("irrefutPatError", str2A),
+ ("patError", str2A),
+ ("divZZeroError", forallAA),
+ ("overflowError", forallAA)]
 
 {- Non-primitive, but mentioned in the types of primitives. -}
 
+bv :: a -> Qual a
 bv = qual baseMname
 
-tcUnit = bv "Unit"
-tUnit = Tcon tcUnit
-ktUnit = Klifted
-tcBool = bv "Bool"
-tBool = Tcon tcBool
-ktBool = Klifted
+str2A, forallAA :: Ty  
+str2A = Tforall ("a",Kopen) (tArrow tAddrzh (Tvar "a"))
+forallAA = Tforall ("a",Kopen) (Tvar "a")
 
-{- Properly defined in PrelError, but needed in many modules before that. -}
-errorVals = [
- ("error", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
- ("irrefutPatError", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
- ("patError", Tforall ("a",Kopen) (tArrow tString (Tvar "a")))]
-  
+tcChar :: Qual Tcon
 tcChar = bv "Char"
+tChar :: Ty
 tChar = Tcon tcChar
-ktChar = Klifted
+tcList :: Qual Tcon
 tcList = bv "ZMZN"
+tList :: Ty -> Ty
 tList t = Tapp (Tcon tcList) t
-ktList = Karrow Klifted Klifted
+tString :: Ty
 tString = tList tChar
-
-{- Utilities for building types -}
-tmonadic t = tArrow t t
-tdyadic t = tArrow t (tArrow t t)
-tcompare t = tArrow t (tArrow t tBool)
-
diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs
index b3aa71e..0b6be42 100644
--- a/utils/ext-core/Printer.hs
+++ b/utils/ext-core/Printer.hs
@@ -1,44 +1,52 @@
+{-# OPTIONS -Werror -Wall -fno-warn-missing-signatures #-}
+
 module Printer where
 
 import Text.PrettyPrint.HughesPJ
-import Numeric (fromRat)
 import Char
 
 import Core
 import Encoding
+import PrimCoercions
 
 instance Show Module where
-  showsPrec d m = shows (pmodule m)
+  showsPrec _ m = shows (pmodule m)
 
 instance Show Tdef where
-  showsPrec d t = shows (ptdef t)
+  showsPrec _ t = shows (ptdef t)
 
 instance Show Cdef where
-  showsPrec d c = shows (pcdef c)
+  showsPrec _ c = shows (pcdef c)
 
 instance Show Vdefg where
-  showsPrec d v = shows (pvdefg v)
+  showsPrec _ v = shows (pvdefg v)
 
 instance Show Vdef where
-  showsPrec d v = shows (pvdef v)
+  showsPrec _ v = shows (pvdef v)
 
 instance Show Exp where
-  showsPrec d e = shows (pexp e)
+  showsPrec _ e = shows (pexp e)
 
 instance Show Alt where
-  showsPrec d a = shows (palt a)
+  showsPrec _ a = shows (palt a)
 
 instance Show Ty where
-  showsPrec d t = shows (pty t)
+  showsPrec _ t = shows (pty t)
 
 instance Show Kind where
-  showsPrec d k = shows (pkind k)
+  showsPrec _ k = shows (pkind k)
 
 instance Show Lit where
-  showsPrec d l = shows (plit l)
+  showsPrec _ l = shows (plit l)
 
 instance Show CoreLit where
-  showsPrec d l = shows (pclit l)
+  showsPrec _ l = shows (pclit l)
+
+instance Show KindOrCoercion where
+  showsPrec _ (Kind k) = shows (text "<K" <+> pkind k <> text ">")
+  showsPrec _ (Coercion (DefinedCoercion tbs (t1,t2))) = 
+     shows (text "<C" <+> hsep (map ptbind tbs) <+>
+              parens (pkind (Keq t1 t2)) <> text ">") 
 
 indent = nest 2
 
@@ -55,11 +63,13 @@ ptdef (Data qtcon tbinds cdefs) =
   (text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=')
   $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
 
-ptdef (Newtype qtcon tbinds (coercion,k) tyopt) =
+ptdef (Newtype qtcon tbinds (coercion,cTbs,k) tyopt) =
   text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds))
     $$ indent (axiomclause $$ repclause)
-       where axiomclause = char '^' <+> parens (pqname coercion <+> text "::"
-                                    <+> pkind k)
+       where axiomclause = char '^' <+> parens (pqname coercion <+> 
+                                          (hsep (map ptbind cTbs)) <+>
+                                          text "::"
+                                      <+> peqkind k)
 	     repclause = case tyopt of
                            Just ty -> char '=' <+> pty ty 
                            Nothing -> empty
@@ -67,9 +77,9 @@ ptdef (Newtype qtcon tbinds (coercion,k) tyopt) =
 pcdef (Constr qdcon tbinds tys)  =
   (pqname qdcon) <+> (sep [hsep (map pattbind tbinds),sep (map paty tys)])
 
-pname id = text id
+pname = text
 
-pqname (m,id) = pmname m <> pname id
+pqname (m,v) = pmname m <> pname v
 
 -- be sure to print the '.' here so we don't print out
 -- ".foo" for unqualified foo...
@@ -78,7 +88,7 @@ pmname Nothing = empty
 -- "%module foo" doesn't get printed as "%module ^foo"
 pmname (Just m) = char '^' <> panmname m <> char '.'
 
-panmname p@(pkgName, parents, name) =
+panmname (pkgName, parents, name) =
   let parentStrs = map pname parents in
          pname pkgName <> char ':' <>
          -- This is to be sure to not print out:
@@ -107,11 +117,23 @@ pakind (Kopen) = char '?'
 pakind k = parens (pkind k)
 
 pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
-pkind (Keq t1 t2) = parens (parens (pty t1) <+> text ":=:" <+> parens (pty t2)) 
+pkind (Keq from to) = peqkind (from,to)
 pkind k = pakind k
 
+peqkind (t1, t2) = parens (parens (pty t1) <+> text ":=:" <+> parens (pty t2)) 
+
 paty (Tvar n) = pname n
 paty (Tcon c) = pqname c
+paty (TransCoercion t1 t2) = 
+    parens (sep ([pqname transCoercion, pbty t1, pbty t2]))
+paty (SymCoercion t) = 
+    parens (sep [pqname symCoercion, paty t])
+paty (UnsafeCoercion t1 t2) = 
+    parens (sep [pqname unsafeCoercion, pbty t1, pbty t2])
+paty (LeftCoercion t) = 
+    parens (pqname leftCoercion <+> paty t)
+paty (RightCoercion t) = 
+    parens (pqname rightCoercion <+> paty t)
 paty t = parens (pty t)
 
 pbty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = parens(fsep [pbty t1, text "->",pty t2])
@@ -153,7 +175,7 @@ pfexp e = paexp e
 pappexp (App e1 e2) as = pappexp e1 (Left e2:as)
 pappexp (Appt e t) as = pappexp e (Right t:as)
 pappexp e as = fsep (paexp e : map pa as)
-           where pa (Left e) = paexp e
+           where pa (Left ex) = paexp ex
 		 pa (Right t) = char '@' <+> paty t
 
 pexp (Lam b e) = char '\\' <+> plamexp [b] e
@@ -204,6 +226,6 @@ escape s = foldr f [] (map ord s)
                  h0 = intToDigit r1
 		 hs = dropWhile (=='0') $ reverse $ mkHex cv
 		 mkHex 0 = ""
-		 mkHex cv = intToDigit r : mkHex q
-		    where (q,r) = quotRem cv 16
+		 mkHex num = intToDigit r : mkHex q
+		    where (q,r) = quotRem num 16
      f cv rest = (chr cv):rest
diff --git a/utils/ext-core/README b/utils/ext-core/README
index 0f6c16b..9afd388 100644
--- a/utils/ext-core/README
+++ b/utils/ext-core/README
@@ -3,13 +3,44 @@ A set of example programs for handling external core format.
 In particular, typechecker and interpreter give a precise semantics.
 
 To build, run "make".
+---------------------
+tjc April 2008:
+
+==== Notes ====
+
+The checker should work on most programs. Bugs I'm aware of:
+1. GHC generates some questionable coercion applications involving
+   partially-applied function arrows (for details, see:
+   http://www.haskell.org/pipermail/cvs-ghc/2008-April/041949.html)
+   This shows up when typechecking a few of the library modules.
+
+2. There's some weirdness involving funny character literals. This can
+   be fixed by writing a new lexer for chars rather than using Parsec's
+   built-in charLiteral lexer. But I haven't done that.
+
+Typechecking all the GHC libraries eats about a gig of heap and takes a
+long time. I blame Parsec. (Someone who was bored, or understood happy
+better than I do, could update the old happy parser, which is still in the
+repo.)
+
+The interpreter is not working yet.
+
+==== Building ====
+
+To run the checker and interpreter, you need to generate External Core
+for all the base, integer and ghc-prim libraries. This can be done by
+adding "-fext-core" to the GhcLibHcOpts in your build.mk file, then
+running "make" under libraries/.
 
-To run the checker and interpreter (which currently aren't working anyway),
-you need to generate External Core for all the base, integer and ghc-prim
-libraries. This can be done by adding "-fext-core" to the GhcLibHcOpts in
-your build.mk file, then running "make" under libraries/.
 Then you need to edit Driver.hs and change "baseDir" to point to your GHC
 libraries directory.
 
-Most recently tested with GHC 6.8.2. I make no claims of portability. --tjc
+Once you've done that:
+1. make prims (to generate the primops file)
+2. make
+3. make nofibtest (to run the parser/checker on all nofib programs...
+   for example.)
+
+Tested with GHC 6.8.2. I make no claims of portability.
+