External Core typechecker - improve handling of coercions

Reorganized coercion-related code in the typechecker (this was
brought about by typechecking the Core versions of the optimized GHC
libraries.) A few miscellaneous changes (fixed a bug in Prep involving
eta-expanding partial applications that had additional type
arguments.)

7 files changed, 183 insertions, 135 deletions

diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
index 95c72812a6..cab3e62ebd 100644
--- a/utils/ext-core/Check.hs
+++ b/utils/ext-core/Check.hs
@@ -91,7 +91,8 @@ checkModule globalEnv (Module mn tdefs vdefgs) =
                               vdefgs
         return (eextend globalEnv 
             (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})))
-    (mn, globalEnv)   
+         -- avoid name shadowing
+    (mn, eremove globalEnv mn)
 
 -- Like checkModule, but doesn't typecheck the code, instead just
 -- returning declared types for top-level defns.
@@ -229,51 +230,44 @@ mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
 
 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) 
                -> Vdefg -> CheckResult (Venv,Venv)
-checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
+checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
+      mn <- getMname
       case vdefg of
 	Rec vdefs ->
-	    do e_venv' <- foldM extendVenv e_venv e_vts
-	       l_venv' <- foldM extendVenv l_venv l_vts
+	    do (e_venv', l_venv') <- makeEnv mn vdefs
 	       let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
-	       mapM_ (\ (vdef@(Vdef ((m,_),t,e))) -> 
-			    do mn <- getMname
-                               requireModulesEq m mn "value definition" vdef True
-			       k <- checkTy (tcenv,tvenv) t
-			       require (k `eqKind` Klifted) ("unlifted kind in:\n" ++ show vdef)
-			       t' <- checkExp env' e
-			       requireM (equalTy tsenv t t') 
-					("declared type doesn't match expression type in:\n"  ++ show vdef ++ "\n" ++  
-					 "declared type: " ++ show t ++ "\n" ++
-					 "expression type: " ++ show t')) vdefs
-	       return (e_venv',l_venv')
-	    where e_vts  = [ (v,t) | Vdef ((Just _,v),t,_) <- vdefs ]
-	          l_vts  = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
-	Nonrec (vdef@(Vdef ((m,v),t,e))) ->
-	    do mn <- getMname
-               -- 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) 
-	       t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
-	       requireM (equalTy tsenv t t') 
-			("declared type doesn't match expression type in:\n" 
-                         ++ show vdef  ++ "\n"  ++
-			 "declared type: " ++ show t ++ "\n" ++
-			 "expression type: " ++ show t') 
-	       if isNothing m then
-                 do l_venv' <- extendVenv l_venv (v,t)
-                    return (e_venv,l_venv')
-	        else
-                              -- 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)
+               mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) 
+                        ("unlifted kind in:\n" ++ show vdef)) env') 
+                     vdefs
+               return (e_venv', l_venv')
+	Nonrec vdef ->
+	    do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv)
+               checkVdef (\ vdef k -> do
+                     require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
+	             require ((not top_level) || (not (k `eqKind` Kunlifted))) 
+                       ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
+               makeEnv mn [vdef]
+
+  where makeEnv mn vdefs = do
+             ev <- foldM extendVenv e_venv e_vts
+             lv <- foldM extendVenv l_venv l_vts
+             return (ev, lv)
+           where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
+                                     not (vdefIsMainWrapper mn (Just m))]
+                 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
+        checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
+          mn <- getMname
+          let isZcMain = vdefIsMainWrapper mn m
+          unless isZcMain $
+             requireModulesEq m mn "value definition" vdef True
+	  k <- checkTy (tcenv,tvenv) t
+	  checkKind vdef k
+	  t' <- checkExp env e
+	  requireM (equalTy tsenv t t') 
+		   ("declared type doesn't match expression type in:\n"  
+                    ++ show vdef ++ "\n" ++  
+		    "declared type: " ++ show t ++ "\n" ++
+		    "expression type: " ++ show t')
     
 vdefIsMainWrapper :: AnMname -> Mname -> Bool
 vdefIsMainWrapper enclosing defining = 
@@ -393,15 +387,11 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
 		 return t
 	    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)
+		 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
+                 require (eTy == fromTy) ("Type mismatch in cast: c = "
+                             ++ show c ++ "\nand eTy = " ++ show eTy
+                             ++ "\n and " ++ show fromTy)
+                 return toTy
 	    Note _ e -> 
 	      ch e
 	    External _ t -> 
@@ -466,7 +456,7 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
 	      checkExp env e
     
 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
-checkTy es@(tcenv,tvenv) t = ch t
+checkTy es@(tcenv,tvenv) = ch
      where
        ch (Tvar tv) = lookupM tvenv tv
        ch (Tcon qtc) = do
@@ -495,7 +485,7 @@ checkTy es@(tcenv,tvenv) t = ch t
                        -- :Co:TTypeable2 (->)
                        -- where in this case, :Co:TTypeable2 expects an
                        -- argument of kind (*->(*->*)) and (->) has kind
-                       -- (?->(?->*)). In general, I don't think it's
+                       -- (?->(?->*)). I'm not sure whether or not it's
                        -- sound to apply an arbitrary coercion to an
                        -- argument that's a subkind of what it expects.
                        then warn $ "Applying coercion " ++ show tc ++
@@ -507,23 +497,12 @@ checkTy es@(tcenv,tvenv) t = ch t
                      return $ Keq (substl tvs tys from) (substl tvs tys to)
                Nothing -> checkTapp t1 t2
             where checkTapp t1 t2 = do 
-	            k1 <- ch t1
+                    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
+		      Karrow k11 k12 -> do
+                         require (k2 `subKindOf` k11) kindError
+                         return k12
                             where kindError = 
                                     "kinds don't match in type application: "
                                     ++ show t ++ "\n" ++
@@ -533,39 +512,89 @@ checkTy es@(tcenv,tvenv) t = ch t
                            
        ch (Tforall tb 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
+               checkTy (tcenv,tvenv') t
        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)
+            (ty1,ty2) <- checkTyCo es t1
+            (ty3,ty4) <- checkTyCo es t2
+            require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
+                        show ty2 ++ " and " ++ show ty3)
+            return $ Keq ty1 ty4
        ch (SymCoercion t1) = do
-            k <- checkTy es t1
-            case k of
-               Keq ty1 ty2 -> return $ Keq ty2 ty1
-               _           -> fail ("Bad kind in sym. coercion: "
-                            ++ show k)
+            (ty1,ty2) <- checkTyCo es t1
+            return $ Keq ty2 ty1
        ch (UnsafeCoercion t1 t2) = do
             checkTy es t1
             checkTy es t2
             return $ Keq t1 t2
        ch (LeftCoercion t1) = do
-            k <- checkTy es t1
+            k <- checkTyCo es t1
             case k of
-              Keq (Tapp u _) (Tapp w _) -> return $ Keq u w
+              ((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
+            k <- checkTyCo es t1
             case k of
-              Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x
+              ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
               _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+       ch (InstCoercion ty arg) = do
+            forallK <- checkTyCo es ty
+            case forallK of
+              ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
+                 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
+                                            ++ show ty)
+                 argK <- checkTy es arg
+                 require (argK `eqKind` k1) ("Kind mismatch in type being "
+                           ++ "instantiated: " ++ show arg)
+                 let newLhs = substl [v1] [arg] b1
+                 let newRhs = substl [v2] [arg] b2
+                 return $ Keq newLhs newRhs
+              _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
+
+checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
+checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = 
+  (case splitTyConApp_maybe t of
+    Just (tc, tys) -> do
+       tcK <- qlookupM tcenv_ tcenv eempty tc
+       case tcK of
+ -- todo: avoid duplicating this code
+ -- blah, this almost calls for a different syntactic form
+ -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
+         Coercion (DefinedCoercion tbs (from, to)) -> do
+           require (length tys == length tbs) $ 
+            ("Arity mismatch in coercion app: " ++ show t)
+           let (tvs, tks) = unzip tbs
+           argKs <- mapM (checkTy es) tys
+           let kPairs = zip argKs tks
+           let kindsOk = all (uncurry eqKind) kPairs
+           if not kindsOk &&
+                        all (uncurry subKindOf) kPairs
+                       -- see comments in checkTy about this
+                       then warn $ "Applying coercion " ++ show tc ++
+                               " to arguments of kind " ++ show argKs
+                               ++ " when it expects: " ++ show tks
+                       else require kindsOk
+                        ("Kind mismatch in coercion app: " ++ show tks 
+                         ++ " and " ++ show argKs ++ " t = " ++ show t)
+           return (substl tvs tys from, substl tvs tys to)
+         _ -> checkTapp t1 t2
+    _ -> checkTapp t1 t2)
+       where checkTapp t1 t2 = do
+               (lhsRator, rhsRator) <- checkTyCo es t1
+               (lhs, rhs) <- checkTyCo es t2
+               -- Comp rule from paper
+               checkTy es (Tapp lhsRator lhs)
+               checkTy es (Tapp rhsRator rhs)
+               return (Tapp lhsRator lhs, Tapp rhsRator rhs)
+checkTyCo (tcenv, tvenv) (Tforall tb t) = do
+  tvenv' <- extendTvenv tvenv tb
+  (t1,t2) <- checkTyCo (tcenv, tvenv') t
+  return (Tforall tb t1, Tforall tb t2)
+checkTyCo es t = do
+  k <- checkTy es t
+  case k of
+    Keq t1 t2 -> return (t1, t2)
+    -- otherwise, expand by the "refl" rule
+    _          -> return (t, t)
 
 {- Type equality modulo newtype synonyms. -}
 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
@@ -598,6 +627,10 @@ equalTy tsenv t1 t2 =
             expand (RightCoercion t1) = do
                exp1 <- expand t1
                return $ RightCoercion exp1
+            expand (InstCoercion t1 t2) = do
+               exp1 <- expand t1
+               exp2 <- expand t2
+               return $ InstCoercion exp1 exp2
 	    expapp (t@(Tcon (m,tc))) ts = 
 	      do env <- mlookupM tsenv_ tsenv eempty m
 		 case elookup env tc of 
@@ -685,6 +718,7 @@ substl tvs ts t = f (zip tvs ts) t
        UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
        LeftCoercion t1 -> LeftCoercion (f env t1)
        RightCoercion t1 -> RightCoercion (f env t1)
+       InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
      where free = foldr union [] (map (freeTvars.snd) env)
            t' = freshTvar free 
    
@@ -692,13 +726,14 @@ substl tvs ts t = f (zip tvs ts) t
 freeTvars :: Ty -> [Tvar]
 freeTvars (Tcon _) = []
 freeTvars (Tvar v) = [v]
-freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
+freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1) 
 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
 freeTvars (SymCoercion t) = freeTvars t
 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
 freeTvars (LeftCoercion t) = freeTvars t
 freeTvars (RightCoercion t) = freeTvars t
+freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
 
 {- Return any tvar *not* in the argument list. -}
 freshTvar :: [Tvar] -> Tvar
diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs
index 5f8ed827d5..66270cd36c 100644
--- a/utils/ext-core/Core.hs
+++ b/utils/ext-core/Core.hs
@@ -60,6 +60,7 @@ data Ty
   | TransCoercion Ty Ty
   | SymCoercion Ty
   | UnsafeCoercion Ty Ty
+  | InstCoercion Ty Ty
   | LeftCoercion Ty
   | RightCoercion Ty
 
@@ -132,9 +133,9 @@ eqKind Kunlifted Kunlifted = True
 eqKind Kopen Kopen = True
 eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
                                    &&  k2 `eqKind` l2
-eqKind _ _ = False -- no Keq kind is ever equal to any other...
-                   -- maybe ok for now?
-
+eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1
+                              && t2 == u2
+eqKind _ _ = False
 
 splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
 splitTyConApp_maybe (Tvar _) = Nothing
diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs
index f080093369..42e21e9113 100644
--- a/utils/ext-core/ParsecParser.hs
+++ b/utils/ext-core/ParsecParser.hs
@@ -109,21 +109,6 @@ coreQualifiedGen p = (try (do
    -- unqualified name
    (p >>= (\ res -> return (Nothing, res)))
 
-{-
-coreMaybeMname = optionMaybe coreMname
-
-coreRequiredQualifiedName = do
-  mname <- coreMname
-  theId <- identifier
-  return (Just mname, theId)
-
-coreMname = do
-  char '^'
-  nm <- try coreModuleName
-  symbol "."
-  return nm
--}
-
 coreAxiom :: Parser Axiom
 coreAxiom = parens (do
               coercionName <- coreQualifiedCon
@@ -204,7 +189,8 @@ coreBty = do
              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")
+             RightCo k -> app k 1 maybeRest "right"
+             InstCo k  -> app k 2 maybeRest "inst")
                  where app k arity args _ | length args == arity = k args
                        app _ _ args err = 
                            primCoercionError (err ++ 
@@ -235,24 +221,26 @@ coreTcon =
                                     -- the "try"s are crucial; they force
                                     -- backtracking
            maybeCoercion <- choice [try symCo, try transCo, try unsafeCo,
-                                    try leftCo, rightCo]
+                                    try instCo, 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))
+              RightC  -> RightCo (\ [x] -> RightCoercion x)
+              InstC   -> InstCo (\ [x,y] -> InstCoercion x y))
     <|> (coreQualifiedCon >>= (return . ATy . Tcon))
 
-data CoercionTy = TransC | SymC | UnsafeC | LeftC | RightC
+data CoercionTy = TransC | InstC | SymC | UnsafeC | LeftC | RightC
 
-symCo, transCo, unsafeCo :: Parser CoercionTy
+symCo, transCo, unsafeCo, instCo, leftCo, rightCo :: 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
+instCo   = string "ghczmprim:GHCziPrim.inst"    >> return InstC
 
 coreForallTy :: Parser Ty
 coreForallTy = do
@@ -270,7 +258,9 @@ coreKind = do
   return $ foldl Karrow hd maybeRest
 
 coreAtomicKind = try liftedKind <|> try unliftedKind 
-       <|> try openKind {- <|> try (parens equalityKind) -}
+       <|> try openKind <|> try (do
+                    (from,to) <- parens equalityKind
+                    return $ Keq from to)
        <|> try (parens coreKind)
 
 liftedKind = do
@@ -301,6 +291,7 @@ data ATyOp =
  | Unsafe ([Ty] -> Ty)
  | LeftCo ([Ty] -> Ty)
  | RightCo ([Ty] -> Ty)
+ | InstCo ([Ty] -> Ty)
 
 coreVdefGroups :: Parser [Vdefg]
 coreVdefGroups = option [] (do
@@ -461,12 +452,15 @@ intOrRatLit :: Parser CoreLit
 intOrRatLit = do
  -- Int and lit combined into one to avoid ambiguity.
  -- Argh....
-  lhs <- anIntLit
+  lhs <- intLit
   maybeRhs <- optionMaybe (symbol "%" >> anIntLit)
   case maybeRhs of
     Nothing  -> return $ Lint lhs
     Just rhs -> return $ Lrational (lhs % rhs)
 
+intLit :: Parser Integer
+intLit = anIntLit <|> parens anIntLit
+
 anIntLit :: Parser Integer
 anIntLit = do
   sign <- option 1 (symbol "-" >> return (-1)) 
diff --git a/utils/ext-core/Prep.hs b/utils/ext-core/Prep.hs
index 05250afdc8..df664a5fb8 100644
--- a/utils/ext-core/Prep.hs
+++ b/utils/ext-core/Prep.hs
@@ -20,11 +20,6 @@ import Check
 
 import Data.List
 
-primArgTys :: Env Var [Ty]
-primArgTys = efromlist (map f (etolist (venv_ primEnv)))
-  where f (v,t) = (v,atys)
-             where (_,atys,_) = splitTy t
-
 prepModule :: Menv -> Module -> Module
 prepModule globalEnv (Module mn tdefs vdefgs) = 
     Module mn tdefs vdefgs' 
@@ -76,24 +71,38 @@ 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 = 
-        etaExpand (drop n atys) (rewindApp env op as)
+        -- possibly dubious to assume no type args
+        etaExpand [] (drop n atys) (rewindApp env op as)
         where (tbs,atys0,_) = splitTy (qlookup cenv_ eempty qdc)
 	      atys = map (substl (map fst tbs) ts) atys0
 	      ts = [t | Right t <- as]
               n = length [e | Left e <- as]
     unwindApp env (op@(Var(qv@(_,p)))) as | isPrimVar qv =
-	etaExpand (drop n atys) (rewindApp env op as)
-        where Just atys = elookup primArgTys p
+	etaExpand (snd (unzip extraTbs)) (drop n atys) (rewindApp env op as)
+        where -- TODO: avoid copying code. these two cases are the same
+
+              -- etaExpand needs to add the type arguments too! Bah!
+              (tbs, atys0, _) = (maybe (error "unwindApp") splitTy (elookup (venv_ primEnv) p))
+              n_args = length ts
+              (appliedTbs, extraTbs) = (take n_args tbs, drop n_args tbs)
+              atys = map (substl (map fst appliedTbs) ts) atys0
+              ts = [t | Right t <- as]
               n = length [e | Left e <- as]
     unwindApp env op as = rewindApp env op as
 
 
-    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
+    etaExpand :: [Kind] -> [Ty] -> Exp -> Exp
+    etaExpand ks ts e = 
+         -- what a pain
+         let tyArgs = [("$t_"++(show i),k) | (i, k) <- zip [(1::Integer)..] ks]   
+             termArgs = [ ('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in
+          foldr (\ (t1,k1) e -> Lam (Tb (t1,k1)) e)
+	   (foldr (\ (v,t) e -> Lam (Vb (v,t)) e)
+              (foldl (\ e (v,_) -> App e (Var (unqual v)))
+                 (foldl (\ e (tv,_) -> Appt e (Tvar tv))
+                   e tyArgs)
+              termArgs) termArgs)
+           tyArgs
 
     rewindApp _ e [] = e
     rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindOfTy tvenv t `eqKind` Kunlifted && suspends e2 =
diff --git a/utils/ext-core/PrimCoercions.hs b/utils/ext-core/PrimCoercions.hs
index 7536cb6caf..8dd0176807 100644
--- a/utils/ext-core/PrimCoercions.hs
+++ b/utils/ext-core/PrimCoercions.hs
@@ -11,12 +11,14 @@ pvz :: Id -> Qual Id
 pvz = (qual primMname) . (++ "zh")
 
 {- Coercions -}
-symCoercion, transCoercion, unsafeCoercion :: Qual Tcon
+symCoercion, transCoercion, unsafeCoercion,
+ leftCoercion, rightCoercion, instCoercion :: Qual Tcon
 symCoercion    = pv "sym"
 transCoercion  = pv "trans"
 unsafeCoercion = pv "CoUnsafe"
 leftCoercion   = pv "left"
-rightCoercion   = pv "right"
+rightCoercion  = pv "right"
+instCoercion   = pv "inst"
 
 {- Addrzh -}
 tcAddrzh = pvz "Addr"
diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs
index 0cd8b09adf..2649a0015a 100644
--- a/utils/ext-core/Printer.hs
+++ b/utils/ext-core/Printer.hs
@@ -143,6 +143,8 @@ pty (LeftCoercion t) =
     (pqname leftCoercion <+> paty t)
 pty (RightCoercion t) = 
     (pqname rightCoercion <+> paty t)
+pty (InstCoercion t1 t2) = 
+    (sep [pqname instCoercion, paty t1, paty t2])
 pty t = pbty t
 
 pappty (Tapp t1 t2) ts = pappty t1 (t2:ts)
diff --git a/utils/ext-core/README b/utils/ext-core/README
index 9afd388175..4fb16ffcf2 100644
--- a/utils/ext-core/README
+++ b/utils/ext-core/README
@@ -9,15 +9,20 @@ 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:
+1. There's some business I don't quite understand involving
+   coercions and subkinding (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.
 
+3. When typechecking the ghc-prim:GHC.PrimopWrappers library module,
+   some declarations seem to have the wrong type signature (due to 
+   confusion between (forall (t::*) ...) and (forall (t::?) ...).)
+   This may be a GHC bug.
+
 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