New kind-polymorphic core

This big patch implements a kind-polymorphic core for GHC. The current
implementation focuses on making sure that all kind-monomorphic programs still
work in the new core; it is not yet guaranteed that kind-polymorphic programs
(using the new -XPolyKinds flag) will work.

For more information, see http://haskell.org/haskellwiki/GHC/Kinds

compiler/basicTypes/MkId.lhs

@@ -1024,7 +1024,7 @@ voidArgId       -- :: State# RealWorld
 coercionTokenId :: Id 	      -- :: () ~ ()
 coercionTokenId -- Used to replace Coercion terms when we go to STG
   = pcMiscPrelId coercionTokenName 
-                 (mkTyConApp eqPrimTyCon [unitTy, unitTy])
+                 (mkTyConApp eqPrimTyCon [liftedTypeKind, unitTy, unitTy])
                  noCafIdInfo
 \end{code}
 

compiler/basicTypes/OccName.lhs

@@ -53,6 +53,7 @@ module OccName (
         mkDFunOcc,
 	mkTupleOcc, 
 	setOccNameSpace,
+        demoteOccName,
 
 	-- ** Derived 'OccName's
         isDerivedOccName,
@@ -204,8 +205,35 @@ pprNameSpaceBrief DataName  = char 'd'
 pprNameSpaceBrief VarName   = char 'v'
 pprNameSpaceBrief TvName    = ptext (sLit "tv")
 pprNameSpaceBrief TcClsName = ptext (sLit "tc")
+
+-- demoteNameSpace lowers the NameSpace if possible.  We can not know
+-- in advance, since a TvName can appear in an HsTyVar.
+-- see Note [Demotion]
+demoteNameSpace :: NameSpace -> Maybe NameSpace
+demoteNameSpace VarName = Nothing
+demoteNameSpace DataName = Nothing
+demoteNameSpace TvName = Nothing
+demoteNameSpace TcClsName = Just DataName
 \end{code}
 
+Note [Demotion]
+~~~~~~~~~~~~~~~
+
+When the user writes:
+  data Nat = Zero | Succ Nat
+  foo :: f Zero -> Int
+
+'Zero' in the type signature of 'foo' is parsed as:
+  HsTyVar ("Zero", TcClsName)
+
+When the renamer hits this occurence of 'Zero' it's going to realise
+that it's not in scope. But because it is renaming a type, it knows
+that 'Zero' might be a promoted data constructor, so it will demote
+its namespace to DataName and do a second lookup.
+
+The final result (after the renamer) will be:
+  HsTyVar ("Zero", DataName)
+
 
 %************************************************************************
 %*									*
@@ -316,6 +344,13 @@ mkClsOcc = mkOccName clsName
 
 mkClsOccFS :: FastString -> OccName
 mkClsOccFS = mkOccNameFS clsName
+
+-- demoteOccName lowers the Namespace of OccName.
+-- see Note [Demotion]
+demoteOccName :: OccName -> Maybe OccName
+demoteOccName (OccName space name) = do
+  space' <- demoteNameSpace space
+  return $ OccName space' name
 \end{code}
 
 

compiler/basicTypes/RdrName.lhs

@@ -40,7 +40,7 @@ module RdrName (
 	nameRdrName, getRdrName, 
 
 	-- ** Destruction
-	rdrNameOcc, rdrNameSpace, setRdrNameSpace,
+	rdrNameOcc, rdrNameSpace, setRdrNameSpace, demoteRdrName,
 	isRdrDataCon, isRdrTyVar, isRdrTc, isQual, isQual_maybe, isUnqual, 
 	isOrig, isOrig_maybe, isExact, isExact_maybe, isSrcRdrName,
 
@@ -159,6 +159,14 @@ setRdrNameSpace (Orig m occ) ns = Orig m (setOccNameSpace ns occ)
 setRdrNameSpace (Exact n)    ns = ASSERT( isExternalName n ) 
 		       	          Orig (nameModule n)
 				       (setOccNameSpace ns (nameOccName n))
+
+-- demoteRdrName lowers the NameSpace of RdrName.
+-- see Note [Demotion] in OccName
+demoteRdrName :: RdrName -> Maybe RdrName
+demoteRdrName (Unqual occ) = fmap Unqual (demoteOccName occ)
+demoteRdrName (Qual m occ) = fmap (Qual m) (demoteOccName occ)
+demoteRdrName (Orig _ _) = panic "demoteRdrName"
+demoteRdrName (Exact _) = panic "demoteRdrName"
 \end{code}
 
 \begin{code}

compiler/basicTypes/Var.lhs

@@ -39,7 +39,7 @@
 
 module Var (
         -- * The main data type and synonyms
-        Var, TyVar, CoVar, Id, DictId, DFunId, EvVar, EqVar, EvId, IpId,
+        Var, TyVar, CoVar, Id, KindVar, DictId, DFunId, EvVar, EqVar, EvId, IpId,
 
 	-- ** Taking 'Var's apart
 	varName, varUnique, varType, 
@@ -60,20 +60,21 @@ module Var (
 	mustHaveLocalBinding,
 
 	-- ** Constructing 'TyVar's
-	mkTyVar, mkTcTyVar, 
+	mkTyVar, mkTcTyVar, mkKindVar,
 
 	-- ** Taking 'TyVar's apart
         tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails,
 
 	-- ** Modifying 'TyVar's
-	setTyVarName, setTyVarUnique, setTyVarKind
+	setTyVarName, setTyVarUnique, setTyVarKind, updateTyVarKind,
+        updateTyVarKindM
 
     ) where
 
 #include "HsVersions.h"
 #include "Typeable.h"
 
-import {-# SOURCE #-}	TypeRep( Type, Kind )
+import {-# SOURCE #-}	TypeRep( Type, Kind, SuperKind )
 import {-# SOURCE #-}	TcType( TcTyVarDetails, pprTcTyVarDetails )
 import {-# SOURCE #-}	IdInfo( IdDetails, IdInfo, coVarDetails, vanillaIdInfo, pprIdDetails )
 
@@ -98,7 +99,10 @@ import Data.Data
 
 \begin{code}
 type Id    = Var       -- A term-level identifier
-type TyVar = Var
+
+type TyVar   = Var     -- Type *or* kind variable
+type KindVar = Var     -- Definitely a kind variable
+     	       	       -- See Note [Kind and type variables]
 
 -- See Note [Evidence: EvIds and CoVars]
 type EvId   = Id        -- Term-level evidence: DictId, IpId, or EqVar
@@ -125,6 +129,16 @@ Note [Evidence: EvIds and CoVars]
 * Only CoVars can occur in Coercions (but NB the LCoercion hack; see
   Note [LCoercions] in Coercion).
 
+Note [Kind and type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Before kind polymorphism, TyVar were used to mean type variables. Now
+they are use to mean kind *or* type variables. KindVar is used when we
+know for sure that it is a kind variable. In future, we might want to
+go over the whole compiler code to use:
+   - KiTyVar to mean kind or type variables
+   - TyVar   to mean         type variables only
+   - KindVar to mean kind         variables
+
 
 %************************************************************************
 %*									*
@@ -142,7 +156,8 @@ in its @VarDetails@.
 -- | Essentially a typed 'Name', that may also contain some additional information
 -- about the 'Var' and it's use sites.
 data Var
-  = TyVar {
+  = TyVar {  -- type and kind variables
+             -- see Note [Kind and type variables]
 	varName    :: !Name,
 	realUnique :: FastInt,		-- Key for fast comparison
 					-- Identical to the Unique in the name,
@@ -195,7 +210,8 @@ After CoreTidy, top-level LocalIds are turned into GlobalIds
 
 \begin{code}
 instance Outputable Var where
-  ppr var = ppr (varName var) <+> ifPprDebug (brackets (ppr_debug var))
+  ppr var = ifPprDebug (text "(") <+> ppr (varName var) <+> ifPprDebug (brackets (ppr_debug var))
+            <+> ifPprDebug (text "::" <+> ppr (tyVarKind var) <+> text ")")
 
 ppr_debug :: Var -> SDoc
 ppr_debug (TyVar {})                           = ptext (sLit "tv")
@@ -255,7 +271,7 @@ setVarType id ty = id { varType = ty }
 
 %************************************************************************
 %*									*
-\subsection{Type variables}
+\subsection{Type and kind variables}
 %*									*
 %************************************************************************
 
@@ -274,6 +290,14 @@ setTyVarName   = setVarName
 
 setTyVarKind :: TyVar -> Kind -> TyVar
 setTyVarKind tv k = tv {varType = k}
+
+updateTyVarKind :: (Kind -> Kind) -> TyVar -> TyVar
+updateTyVarKind update tv = tv {varType = update (tyVarKind tv)}
+
+updateTyVarKindM :: (Monad m) => (Kind -> m Kind) -> TyVar -> m TyVar
+updateTyVarKindM update tv
+  = do { k' <- update (tyVarKind tv)
+       ; return $ tv {varType = k'} }
 \end{code}
 
 \begin{code}
@@ -298,6 +322,15 @@ tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var)
 
 setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar
 setTcTyVarDetails tv details = tv { tc_tv_details = details }
+
+mkKindVar :: Name -> SuperKind -> KindVar
+-- mkKindVar take a SuperKind as argument because we don't have access
+-- to tySuperKind here.
+mkKindVar name kind = TyVar
+  { varName    = name
+  , realUnique = getKeyFastInt (nameUnique name)
+  , varType    = kind }
+
 \end{code}
 
 %************************************************************************

compiler/coreSyn/CoreLint.lhs

@@ -218,11 +218,13 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
 %************************************************************************
 
 \begin{code}
-type InType      = Type	-- Substitution not yet applied
+--type InKind      = Kind	-- Substitution not yet applied
+type InType      = Type	
 type InCoercion  = Coercion
 type InVar       = Var
 type InTyVar     = TyVar
 
+type OutKind     = Kind	-- Substitution has been applied to this
 type OutType     = Type	-- Substitution has been applied to this
 type OutCoercion = Coercion
 type OutVar      = Var
@@ -296,19 +298,6 @@ lintCoreExpr (Let (Rec pairs) body)
     (_, dups) = removeDups compare bndrs
 
 lintCoreExpr e@(App _ _)
-    | Var x <- fun -- Greivous hack for Eq# construction: Eq# may have type arguments
-                   -- of kind (* -> *) but its type insists on *. When we have polymorphic kinds,
-                   -- we should do this properly
-    , Just dc <- isDataConWorkId_maybe x
-    , dc == eqBoxDataCon
-    , [Type arg_ty1, Type arg_ty2, co_e] <- args
-    = do arg_kind1 <- lintType arg_ty1
-         arg_kind2 <- lintType arg_ty2
-         unless (arg_kind1 `eqKind` arg_kind2)
-                (addErrL (mkEqBoxKindErrMsg arg_ty1 arg_ty2))
-         
-         lintCoreArg (mkCoercionType arg_ty1 arg_ty2 `mkFunTy` mkEqPred (arg_ty1, arg_ty2)) co_e
-    | otherwise
     = do { fun_ty <- lintCoreExpr fun
          ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
   where
@@ -370,6 +359,27 @@ lintCoreExpr (Coercion co)
        ; return (mkCoercionType ty1 ty2) }
 \end{code}
 
+Note [Kind instantiation in coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider the following coercion axiom:
+  ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
+
+Consider the following instantiation:
+  ax_co <* -> *> <Monad>
+
+We need to split the co_ax_tvs into kind and type variables in order
+to find out the coercion kind instantiations. Those can only be Refl
+since we don't have kind coercions. This is just a way to represent
+kind instantiation.
+
+We use the number of kind variables to know how to split the coercions
+instantiations between kind coercions and type coercions. We lint the
+kind coercions and produce the following substitution which is to be
+applied in the type variables:
+  k_ag   ~~>   * -> *
+
+
 %************************************************************************
 %*									*
 \subsection[lintCoreArgs]{lintCoreArgs}
@@ -432,10 +442,14 @@ lintValApp arg fun_ty arg_ty
 checkTyKind :: OutTyVar -> OutType -> LintM ()
 -- Both args have had substitution applied
 checkTyKind tyvar arg_ty
+  | isSuperKind tyvar_kind  -- kind forall
+  -- IA0_NOTE: I added this case to handle kind foralls
+  = lintKind arg_ty
 	-- Arg type might be boxed for a function with an uncommitted
 	-- tyvar; notably this is used so that we can give
 	-- 	error :: forall a:*. String -> a
 	-- and then apply it to both boxed and unboxed types.
+  | otherwise  -- type forall
   = do { arg_kind <- lintType arg_ty
        ; unless (arg_kind `isSubKind` tyvar_kind)
                 (addErrL (mkKindErrMsg tyvar arg_ty)) }
@@ -458,6 +472,16 @@ checkTyCoKind tv co
 checkTyCoKinds :: [TyVar] -> [OutCoercion] -> LintM [(OutType, OutType)]
 checkTyCoKinds = zipWithM checkTyCoKind
 
+checkKiCoKind :: KindVar -> OutCoercion -> LintM Kind
+-- see lintCoercion (AxiomInstCo {}) and Note [Kind instantiation in coercions]
+checkKiCoKind kv co
+  = do { ki <- lintKindCoercion co
+       ; unless (isSuperKind (tyVarKind kv)) (addErrL (mkTyCoAppErrMsg kv co))
+       ; return ki }
+
+checkKiCoKinds :: [KindVar] -> [OutCoercion] -> LintM [Kind]
+checkKiCoKinds = zipWithM checkKiCoKind
+
 checkDeadIdOcc :: Id -> LintM ()
 -- Occurrences of an Id should never be dead....
 -- except when we are checking a case pattern
@@ -622,11 +646,11 @@ lintAndScopeId id linterF
 lintInTy :: InType -> LintM OutType
 -- Check the type, and apply the substitution to it
 -- See Note [Linting type lets]
--- ToDo: check the kind structure of the type
 lintInTy ty 
   = addLoc (InType ty) $
     do	{ ty' <- applySubstTy ty
-	; _ <- lintType ty'
+	; k <- lintType ty'
+	; lintKind k
 	; return ty' }
 
 lintInCo :: InCoercion -> LintM OutCoercion
@@ -639,21 +663,42 @@ lintInCo co
         ; return co' }
 
 -------------------
-lintKind :: Kind -> LintM ()
--- Check well-formedness of kinds: *, *->*, etc
-lintKind (TyConApp tc []) 
-  | tyConKind tc `eqKind` tySuperKind
-  = return ()
+lintKind :: OutKind -> LintM ()
+-- Check well-formedness of kinds: *, *->*, Either * (* -> *), etc
 lintKind (FunTy k1 k2)
   = lintKind k1 >> lintKind k2
-lintKind kind 
+
+lintKind kind@(TyConApp tc kis)
+  = do { unless (tyConArity tc == length kis || isSuperKindTyCon tc)
+           (addErrL malformed_kind)
+       ; mapM_ lintKind kis }
+  where
+    malformed_kind = hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind))
+
+lintKind (TyVarTy kv) = checkTyCoVarInScope kv
+lintKind kind
   = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
 
 -------------------
 lintTyBndrKind :: OutTyVar -> LintM ()
-lintTyBndrKind tv = lintKind (tyVarKind tv)
+-- Handles both type and kind foralls.
+lintTyBndrKind tv =
+  let ki = tyVarKind tv in
+  if isSuperKind ki
+  then return ()    -- kind forall
+  else lintKind ki  -- type forall
 
 -------------------
+lintKindCoercion :: OutCoercion -> LintM OutKind
+-- Kind coercions are only reflexivity because they mean kind
+-- instantiation.  See Note [Kind coercions] in Coercion
+lintKindCoercion co
+  = do { (k1,k2) <- lintCoercion co
+       ; checkL (k1 `eqKind` k2) 
+                (hang (ptext (sLit "Non-refl kind coercion")) 
+                    2 (ppr co))
+       ; return k1 }
+
 lintCoercion :: OutCoercion -> LintM (OutType, OutType)
 -- Check the kind of a coercion term, returning the kind
 lintCoercion (Refl ty)
@@ -661,9 +706,21 @@ lintCoercion (Refl ty)
        ; return (ty, ty) }
 
 lintCoercion co@(TyConAppCo tc cos)
-  = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
-       ; check_co_app co (tyConKind tc) ss
-       ; return (mkTyConApp tc ss, mkTyConApp tc ts) }
+  = do   -- We use the kind of the type constructor to know how many
+         -- kind coercions we have (one kind coercion for one kind
+         -- instantiation).
+       { let ki | tc `hasKey` funTyConKey && length cos == 2
+                  = mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind
+                  -- It's a fully applied function, so we must use the
+                  -- most permissive type for the arrow constructor
+                | otherwise = tyConKind tc
+             (kvs, _) = splitForAllTys ki
+             (cokis, cotys) = splitAt (length kvs) cos
+         -- kis are the kind instantiations of tc
+       ; kis <- mapM lintKindCoercion cokis
+       ; (ss,ts) <- mapAndUnzipM lintCoercion cotys
+       ; check_co_app co ki (kis ++ ss)
+       ; return (mkTyConApp tc (kis ++ ss), mkTyConApp tc (kis ++ ts)) }
 
 lintCoercion co@(AppCo co1 co2)
   = do { (s1,t1) <- lintCoercion co1
@@ -672,7 +729,9 @@ lintCoercion co@(AppCo co1 co2)
        ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
 
 lintCoercion (ForAllCo v co)
-  = do { lintKind (tyVarKind v)
+  = do { let kind = tyVarKind v
+         -- lintKind when type forall, otherwise we are a kind forall
+       ; unless (isSuperKind kind) (lintKind kind)
        ; (s,t) <- addInScopeVar v (lintCoercion co)
        ; return (ForAllTy v s, ForAllTy v t) }
 
@@ -684,13 +743,21 @@ lintCoercion (CoVarCo cv)
   = do { checkTyCoVarInScope cv
        ; return (coVarKind cv) }
 
-lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs
+lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
                                    , co_ax_lhs = lhs
-                                   , co_ax_rhs = rhs }) 
+                                   , co_ax_rhs = rhs })
                            cos)
-  = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos)
-       ; return (substTyWith tvs tys1 lhs,
-                 substTyWith tvs tys2 rhs) }
+  = ASSERT2 (not (any isKiVar tvs), ppr ktvs)
+    do   -- see Note [Kind instantiation in coercions]
+       { kis <- checkKiCoKinds kvs kcos
+       ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs
+             subst = zipOpenTvSubst kvs kis
+       ; (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs' tcos)
+       ; return (substTyWith ktvs (kis ++ tys1) lhs,
+                 substTyWith ktvs (kis ++ tys2) rhs) }
+  where
+    (kvs, tvs) = splitKiTyVars ktvs
+    (kcos, tcos) = splitAt (length kvs) cos
 
 lintCoercion (UnsafeCo ty1 ty2)
   = do { _k1 <- lintType ty1
@@ -741,20 +808,21 @@ checkTcApp co n ty
 lintType :: OutType -> LintM Kind
 lintType (TyVarTy tv)
   = do { checkTyCoVarInScope tv
-       ; return (tyVarKind tv) }
+       ; let kind = tyVarKind tv
+       ; lintKind kind
+       ; if (isSuperKind kind) then failWithL msg
+         else return kind }
+  where msg = hang (ptext (sLit "Expecting a type, but got a kind"))
+                 2 (ptext (sLit "Offending kind:") <+> ppr tv)
 
 lintType ty@(AppTy t1 t2) 
   = do { k1 <- lintType t1
        ; lint_ty_app ty k1 [t2] }
 
 lintType ty@(FunTy t1 t2)
-  = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
+  = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
 
 lintType ty@(TyConApp tc tys)
-  | tc `hasKey` eqPrimTyConKey	-- See Note [The ~# TyCon] in TysPrim
-  = lint_prim_eq_pred ty tys
-  | tc `hasKey` eqTyConKey
-  = lint_eq_pred ty tys
   | tyConHasKind tc
   = lint_ty_app ty (tyConKind tc) tys
   | otherwise
@@ -766,58 +834,43 @@ lintType (ForAllTy tv ty)
 
 ----------------
 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
-lint_ty_app ty k tys 
-  = do { ks <- mapM lintType tys
-       ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
-
-lint_eq_pred :: Type -> [OutType] -> LintM Kind
-lint_eq_pred ty arg_tys = case arg_tys of
-  [ty1, ty2] ->  do { k1 <- lintType ty1
-                    ; k2 <- lintType ty2
-                    ; unless (k1 `eqKind` k2) 
-                             (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
-                                           , nest 2 (ppr ty) ]))
-                    ; return constraintKind }
-  [ty1] -> do { k1 <- lintType ty1;
-                return (k1 `mkFunTy` constraintKind) }
-  []    -> do { return (typeKind ty) }
-  _     -> failWithL (ptext (sLit "Oversaturated (~) type") <+> ppr ty)
-
-
-lint_prim_eq_pred :: Type -> [OutType] -> LintM Kind
-lint_prim_eq_pred ty arg_tys
-  | [ty1,ty2] <- arg_tys
-  = do { k1 <- lintType ty1
-       ; k2 <- lintType ty2
-       ; checkL (k1 `eqKind` k2) 
-                (ptext (sLit "Mismatched arg kinds:") <+> ppr ty)
-       ; return unliftedTypeKind }
-  | otherwise
-  = failWithL (ptext (sLit "Unsaturated ~# type") <+> ppr ty)
+lint_ty_app ty k tys = lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
 
 ----------------
 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
-check_co_app ty k tys 
-  = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))  
-                            k (map typeKind tys)
-       ; return () }
-                      
+check_co_app ty k tys = lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys >> return ()
+
 ----------------
-lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
-lint_kind_app doc kfn ks = go kfn ks
+lint_kind_app :: SDoc -> Kind -> [OutType] -> LintM Kind
+-- Takes care of linting the OutTypes
+lint_kind_app doc kfn tys = go kfn tys
   where
-    fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
-               	     nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
-               	     nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
-
-    go kfn []     = return kfn
-    go kfn (k:ks) = case splitKindFunTy_maybe kfn of
-       	              Nothing         -> failWithL fail_msg
-		      Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
-                                                     (addErrL fail_msg)
-                                            ; go kfb ks } 
+    fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
+                    , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
+                    , nest 2 (ptext (sLit "Arg types =") <+> ppr tys) ]
+
+    go kfn [] = return kfn
+    go kfn (ty:tys) =
+      case splitKindFunTy_maybe kfn of
+      { Nothing ->
+          case splitForAllTy_maybe kfn of
+          { Nothing -> failWithL fail_msg
+          ; Just (kv, body) -> do
+              -- Something of kind (forall kv. body) gets instantiated
+              -- with ty. 'kv' is a kind variable and 'ty' is a kind.
+            { unless (isSuperKind (tyVarKind kv)) (addErrL fail_msg)
+            ; lintKind ty
+            ; go (substKiWith [kv] [ty] body) tys } }
+      ; Just (kfa, kfb) -> do
+          -- Something of kind (kfa -> kfb) is applied to ty. 'ty' is
+          -- a type accepting kind 'kfa'.
+        { k <- lintType ty
+        ; lintKind kfa
+        ; unless (k `isSubKind` kfa) (addErrL fail_msg)
+        ; go kfb tys } }
+
 \end{code}
-    
+
 %************************************************************************
 %*									*
 \subsection[lint-monad]{The Lint monad}
@@ -1168,14 +1221,6 @@ mkStrictMsg binder
 	     ]
 
 
-mkEqBoxKindErrMsg :: Type -> Type -> Message
-mkEqBoxKindErrMsg ty1 ty2
-  = vcat [ptext (sLit "Kinds don't match in type arguments of Eq#:"),
-          hang (ptext (sLit "Arg type 1:"))   
-                 4 (ppr ty1 <+> dcolon <+> ppr (typeKind ty1)),
-          hang (ptext (sLit "Arg type 2:"))   
-                 4 (ppr ty2 <+> dcolon <+> ppr (typeKind ty2))]
-
 mkKindErrMsg :: TyVar -> Type -> Message
 mkKindErrMsg tyvar arg_ty
   = vcat [ptext (sLit "Kinds don't match in type application:"),

compiler/coreSyn/CoreUtils.lhs

@@ -67,6 +67,7 @@ import Util
 import Pair
 import Data.Word
 import Data.Bits
+import Data.List ( mapAccumL )
 \end{code}
 
 
@@ -1064,9 +1065,10 @@ dataConInstPat :: [FastString]          -- A long enough list of FSs to use for
 --
 --  where the double-primed variables are created with the FastStrings and
 --  Uniques given as fss and us
-dataConInstPat fss uniqs con inst_tys
-  = (ex_bndrs, arg_ids)
-  where
+dataConInstPat fss uniqs con inst_tys 
+  = ASSERT( univ_tvs `equalLength` inst_tys )
+    (ex_bndrs, arg_ids)
+  where 
     univ_tvs = dataConUnivTyVars con
     ex_tvs   = dataConExTyVars con
     arg_tys  = dataConRepArgTys con
@@ -1077,19 +1079,25 @@ dataConInstPat fss uniqs con inst_tys
     (ex_uniqs, id_uniqs) = splitAt n_ex uniqs
     (ex_fss,   id_fss)   = splitAt n_ex fss
 
-      -- Make existential type variables
-    ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_fss ex_tvs
-    mk_ex_var uniq fs var = mkTyVar new_name kind
+      -- Make the instantiating substitution for universals
+    univ_subst = zipOpenTvSubst univ_tvs inst_tys
+
+      -- Make existential type variables, applyingn and extending the substitution
+    (full_subst, ex_bndrs) = mapAccumL mk_ex_var univ_subst 
+                                       (zip3 ex_tvs ex_fss ex_uniqs)
+
+    mk_ex_var :: TvSubst -> (TyVar, FastString, Unique) -> (TvSubst, TyVar)
+    mk_ex_var subst (tv, fs, uniq) = (Type.extendTvSubst subst tv (mkTyVarTy new_tv)
+                                     , new_tv)
       where
+        new_tv   = mkTyVar new_name kind
         new_name = mkSysTvName uniq fs
-        kind     = tyVarKind var
-
-      -- Make the instantiating substitution
-    subst = zipOpenTvSubst (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
+        kind     = Type.substTy subst (tyVarKind tv)
 
       -- Make value vars, instantiating types
-    mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (Type.substTy subst ty) noSrcSpan
     arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys
+    mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq 
+                                       (Type.substTy full_subst ty) noSrcSpan
 \end{code}
 
 %************************************************************************

compiler/coreSyn/MkCore.lhs

@@ -288,8 +288,10 @@ mkIPUnbox ipx = Var x `Cast` mkAxInstCo (ipCoAxiom ip) [ty]
 \begin{code}
 
 mkEqBox :: Coercion -> CoreExpr
-mkEqBox co = Var (dataConWorkId eqBoxDataCon) `mkTyApps` [ty1, ty2] `App` Coercion co
+mkEqBox co = ASSERT( typeKind ty2 `eqKind` k )
+             Var (dataConWorkId eqBoxDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
   where Pair ty1 ty2 = coercionKind co
+        k = typeKind ty1
 
 \end{code}
 

compiler/coreSyn/MkExternalCore.lhs

@@ -23,6 +23,7 @@ import TyCon
 -- import Class
 import TypeRep
 import Type
+import Kind
 import PprExternalCore () -- Instances
 import DataCon
 import Coercion

compiler/coreSyn/PprCore.lhs

@@ -28,6 +28,7 @@ import Demand
 import DataCon
 import TyCon
 import Type
+import Kind