More simplification of the sub-kinding story

9 files changed, 149 insertions, 200 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index cd4e2523ac..47e25839fa 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -689,8 +689,8 @@ lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
   | isSuperKind k1 
   = return superKind
   | otherwise
-  = do { unless (k1 `isSubKind` argTypeKind)  (addErrL (msg (ptext (sLit "argument")) k1))
-       ; unless (k2 `isSubKind` openTypeKind) (addErrL (msg (ptext (sLit "result"))   k2))
+  = do { unless (okArrowArgKind k1)    (addErrL (msg (ptext (sLit "argument")) k1))
+       ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result"))   k2))
        ; return liftedTypeKind }
   where
     msg ar k
@@ -791,7 +791,11 @@ lintCoercion (CoVarCo cv)
   = do { checkTyCoVarInScope cv
        ; cv' <- lookupIdInScope cv 
        ; let (s,t) = coVarKind cv'
-       ; return (typeKind s, s, t) }
+             k     = typeKind s
+       ; when (isSuperKind k) $
+         checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
+                                   2 (ppr cv))
+       ; return (k, s, t) }
 
 lintCoercion (UnsafeCo ty1 ty2)
   = do { k1 <- lintType ty1
@@ -846,33 +850,27 @@ lintCoercion co@(AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
                                       , co_ax_rhs = rhs })
                              cos)
   = do {  -- See Note [Kind instantiation in coercions]
-         let (kvs, tvs)   = splitKiTyVars ktvs
-             (kcos, tcos) = splitAt (length kvs) cos
-       ; unless (not (any isKiVar tvs)
-                 && kvs `equalLength` kcos 
-                 && tvs `equalLength` tcos) (bad_ax (ptext (sLit "lengths")))
-
-       ; kis <- mapM check_ki kcos
-       ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs
-             subst = zipOpenTvSubst kvs kis
-       ; (tks, tys1, tys2) <- mapAndUnzip3M lintCoercion tcos
-
-       ; zipWithM_ check_ki2 tvs' tks
-       ; let lhs' = substTyWith ktvs (kis ++ tys1) lhs
-             rhs' = substTyWith ktvs (kis ++ tys2) rhs
-
+         unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
+       ; in_scope <- getInScope
+       ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
+       ; (subst_l, subst_r) <- foldlM check_ki 
+                                      (empty_subst, empty_subst) 
+                                      (ktvs `zip` cos)
+       ; let lhs' = Type.substTy subst_l lhs
+             rhs' = Type.substTy subst_r rhs
        ; return (typeKind lhs', lhs', rhs') }
   where
     bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
                         2 (ppr co))
-    check_ki co
-      = do { (k, k1, k2) <- lintCoercion co
-           ; unless (isSuperKind k)  (bad_ax (ptext (sLit "check_ki1a")))
-           ; unless (k1 `eqKind` k2) (bad_ax (ptext (sLit "check_ki1b")))
-           ; return k1 }   -- Kind coercions must be refl
-
-    check_ki2 tv k = unless (k `isSubKind` tyVarKind tv) 
-                            (bad_ax (ptext (sLit "check_ki2")))
+
+    check_ki (subst_l, subst_r) (ktv, co)
+      = do { (k, t1, t2) <- lintCoercion co
+           ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
+                  -- Using subst_l is ok, because subst_l and subst_r
+                  -- must agree on kind equalities
+           ; unless (k `isSubKind` ktv_kind) (bad_ax (ptext (sLit "check_ki2")))
+           ; return (Type.extendTvSubst subst_l ktv t1, 
+                     Type.extendTvSubst subst_r ktv t2) } 
 \end{code}
 
 %************************************************************************
@@ -993,6 +991,9 @@ updateTvSubst subst' m =
 getTvSubst :: LintM TvSubst
 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
 
+getInScope :: LintM InScopeSet
+getInScope = LintM (\ _ subst errs -> (Just (getTvInScope subst), errs))
+
 applySubstTy :: InType -> LintM OutType
 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
 
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 0fb9d43a6e..cb388ff057 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -481,7 +481,7 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
 
   -- So tv is a meta tyvar, and presumably it is
   -- an *untouchable* meta tyvar, else it'd have been unified
-  | not (k2 `isSubKind` k1)   	 -- Kind error
+  | not (k2 `tcIsSubKind` k1)   	 -- Kind error
   = mkErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
 
   -- Occurs check
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index fe13f76140..f26bfbbf9a 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -887,7 +887,6 @@ tcTyVarBndrs bndrs thing_inside = do
   where
     zonk (name, kind)
       = do { kind' <- zonkTcKind kind
-           ; checkTc (noHashInKind kind') (ptext (sLit "Kind signature contains # or (#)"))
            ; return (mkTyVar name kind') }
 
 tcTyVarBndrsKindGen :: [LHsTyVarBndr Name] -> ([TyVar] -> TcM r) -> TcM r
@@ -964,8 +963,9 @@ kindGeneralizeKinds kinds
                                             `minusVarSet` gbl_tvs)
 
              (_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
+                           -- We do not get a later chance to tidy!
 
-       ; kvs <- ASSERT2 (all isKiVar kvs_to_quantify, ppr kvs_to_quantify)
+       ; kvs <- ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify)
                 zonkQuantifiedTyVars tidy_kvs_to_quantify
 
          -- Zonk the kinds again, to pick up either the kind 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index cee7bc9ef4..518a40363c 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -70,8 +70,6 @@ module TcMType (
 
   zonkTcTypeAndSubst,
   tcGetGlobalTyVars, 
-
-  compatKindTcM, isSubKindTcM
   ) where
 
 #include "HsVersions.h"
@@ -389,7 +387,7 @@ writeMetaTyVarRef tyvar ref ty
        ; writeMutVar ref (Indirect ty) 
        ; when (   not (isPredTy tv_kind) 
                     -- Don't check kinds for updates to coercion variables
-               && not (zonked_ty_kind `isSubKind` zonked_tv_kind))
+               && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
        $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
                         2 (    ppr tyvar <+> text "::" <+> ppr tv_kind 
                            <+> text ":=" 
@@ -419,22 +417,26 @@ newFlexiTyVarTy kind = do
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
-tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 -- Instantiate with META type variables
+-- Note that this works for a sequence of kind and type
+-- variables.  Eg    [ (k:BOX), (a:k->k) ]
+--             Gives [ (k7:BOX), (a8:k7->k7) ]
 tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
     -- emptyTvSubst has an empty in-scope set, but that's fine here
     -- Since the tyvars are freshly made, they cannot possibly be
     -- captured by any existing for-alls.
 
-tcInstTyVarsX :: TvSubst -> [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+-- The "X" part is because of extending the substitution
 tcInstTyVarsX subst tyvars =
-  do { (subst', tyvars') <- mapAccumLM tcInstTyVar subst tyvars
+  do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
      ; return (tyvars', mkTyVarTys tyvars', subst') }
 
-tcInstTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
+tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
-tcInstTyVar subst tyvar
+tcInstTyVarX subst tyvar
   = do  { uniq <- newMetaUnique
         ; ref <- newMutVar Flexi
         ; let name   = mkSystemName uniq (getOccName tyvar)
@@ -563,15 +565,14 @@ zonkTcPredType = zonkTcType
 defaultKindVarToStar :: TcTyVar -> TcM Kind
 -- We have a meta-kind: unify it with '*'
 defaultKindVarToStar kv 
-  = do { ASSERT ( isKiVar kv && isMetaTyVar kv )
+  = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
          writeMetaTyVar kv liftedTypeKind
        ; return liftedTypeKind }
 
 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
--- Precondition: a kind variable occurs before a type
---               variable mentioning it in its kind
+-- A kind variable k may occur *after* a tyvar mentioning k in its kind
 zonkQuantifiedTyVars tyvars
-  = do { let (kvs, tvs) = partitionKiTyVars tyvars
+  = do { let (kvs, tvs) = partition isKindVar tyvars
        ; poly_kinds <- xoptM Opt_PolyKinds
        ; if poly_kinds then
              mapM zonkQuantifiedTyVar (kvs ++ tvs)
@@ -820,19 +821,6 @@ zonkType zonk_tc_tyvar ty
 %************************************************************************
 
 \begin{code}
-compatKindTcM :: Kind -> Kind -> TcM Bool
-compatKindTcM k1 k2
-  = do { k1' <- zonkTcKind k1
-       ; k2' <- zonkTcKind k2
-       ; return $ k1' `isSubKind` k2' || k2' `isSubKind` k1' }
-
-isSubKindTcM :: Kind -> Kind -> TcM Bool
-isSubKindTcM k1 k2
-  = do { k1' <- zonkTcKind k1
-       ; k2' <- zonkTcKind k2
-       ; return $ k1' `isSubKind` k2' }
-
--------------
 zonkTcKind :: TcKind -> TcM TcKind
 zonkTcKind k = zonkTcType k
 \end{code}
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 6bd8dd90d8..ae948b5f95 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1130,7 +1130,7 @@ getSolvableCTyFunEqs untch cts
       , isTouchableMetaTyVar_InRange untch tv
            -- And it's a *touchable* unification variable
 
-      , typeKind xi `isSubKind` tyVarKind tv
+      , typeKind xi `tcIsSubKind` tyVarKind tv
          -- Must do a small kind check since TcCanonical invariants 
          -- on family equations only impose compatibility, not subkinding
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 322506ff3f..8fa79e9148 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -1367,7 +1367,7 @@ checkValidClass cls
         ; mapM_ check_at_defs at_stuff	}
   where
     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
-    unary = isSingleton (snd (splitKiTyVars tyvars))  -- IA0_NOTE: only count type arguments
+    unary = count isTypeVar tyvars == 1   -- Ignore kind variables
 
     check_op constrained_class_methods (sel_id, dm) 
       = addErrCtxt (classOpCtxt sel_id tau) $ do
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index e0d5f63722..c94752111c 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -37,6 +37,7 @@ module TcType (
   isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
   isAmbiguousTyVar, metaTvRef, 
   isFlexi, isIndirect, isRuntimeUnkSkol,
+  isTypeVar, isKindVar,
 
   --------------------------------
   -- Builders
@@ -118,7 +119,7 @@ module TcType (
   unliftedTypeKind, liftedTypeKind, argTypeKind,
   openTypeKind, constraintKind, mkArrowKind, mkArrowKinds, 
   isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
-  isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind,
+  isSubArgTypeKind, tcIsSubKind, splitKindFunTys, defaultKind,
   mkMetaKindVar,
 
   --------------------------------
diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs
index 3fda25c592..b3684151b1 100644
--- a/compiler/types/Kind.lhs
+++ b/compiler/types/Kind.lhs
@@ -36,18 +36,18 @@ module Kind (
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
         isUbxTupleKind, isArgTypeKind, isConstraintKind,
-        isConstraintOrLiftedKind, isKind,
-        isSuperKind, isSuperKindTyCon, noHashInKind,
+        isConstraintOrLiftedKind, isKind, isKindVar,
+        isSuperKind, isSuperKindTyCon,
         isLiftedTypeKindCon, isConstraintKindCon,
         isAnyKind, isAnyKindCon,
+        okArrowArgKind, okArrowResultKind,
 
-        isSubArgTypeKind, tcIsSubArgTypeKind, 
-        isSubOpenTypeKind, tcIsSubOpenTypeKind,
-        isSubKind, tcIsSubKind, defaultKind,
-        isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon,
+        isSubArgTypeKind, isSubOpenTypeKind, 
+        isSubKind, isSubKindCon, 
+        tcIsSubKind, tcIsSubKindCon,
+        defaultKind,
 
         -- ** Functions on variables
-        isKiVar, splitKiTyVars, partitionKiTyVars,
         kiVarsOfKind, kiVarsOfKinds
 
        ) where
@@ -59,38 +59,9 @@ import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
 import TypeRep
 import TysPrim
 import TyCon
-import Var
 import VarSet
 import PrelNames
 import Outputable
-
-import Data.List ( partition )
-\end{code}
-
-%************************************************************************
-%*									*
-        Predicates over Kinds
-%*									*
-%************************************************************************
-
-\begin{code}
--------------------
--- Lastly we need a few functions on Kinds
-
-isLiftedTypeKindCon :: TyCon -> Bool
-isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
-
--- This checks that its argument does not contain # or (#).
--- It is used in tcTyVarBndrs.
-noHashInKind :: Kind -> Bool
-noHashInKind (TyVarTy {}) = True
-noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2
-noHashInKind (ForAllTy _ ki) = noHashInKind ki
-noHashInKind (TyConApp kc kis)
-  =  not (kc `hasKey` unliftedTypeKindTyConKey)
-  && not (kc `hasKey` ubxTupleKindTyConKey)
-  && all noHashInKind kis
-noHashInKind _ = panic "noHashInKind"
 \end{code}
 
 %************************************************************************
@@ -139,37 +110,34 @@ isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
   isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
 
 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
-  isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon,
-  isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon,
-  isAnyKindCon :: TyCon -> Bool
+  isUnliftedTypeKindCon, isSubArgTypeKindCon, 
+  isSubOpenTypeKindCon, isConstraintKindCon,
+  isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool
 
-isAnyKindCon tc     = tyConUnique tc == anyKindTyConKey
+
+isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
+isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
+isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
+isUbxTupleKindCon     tc = tyConUnique tc == ubxTupleKindTyConKey
+isArgTypeKindCon      tc = tyConUnique tc == argTypeKindTyConKey
+isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
 
 isAnyKind (TyConApp tc _) = isAnyKindCon tc
 isAnyKind _               = False
 
-isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
-
 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
 isOpenTypeKind _               = False
 
-isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
-
 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
 isUbxTupleKind _               = False
 
-isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
-
 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
 isArgTypeKind _               = False
 
-isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
-
 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 isUnliftedTypeKind _               = False
 
-isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
-
 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 isConstraintKind _               = False
 
@@ -177,106 +145,120 @@ isConstraintOrLiftedKind (TyConApp tc _)
   = isConstraintKindCon tc || isLiftedTypeKindCon tc
 isConstraintOrLiftedKind _ = False
 
--- Subkinding
+--------------------------------------------
+--            Kinding for arrow (->)
+-- Says when a kind is acceptable on lhs or rhs of an arrow
+--     arg -> res
+
+okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
+okArrowArgKindCon kc
+  | isLiftedTypeKindCon   kc = True
+  | isUnliftedTypeKindCon kc = True
+  | isConstraintKindCon   kc = True
+  | otherwise                = False
+
+okArrowResultKindCon kc
+  | okArrowArgKindCon kc = True
+  | isUbxTupleKindCon kc = True
+  | otherwise            = False
+
+okArrowArgKind, okArrowResultKind :: Kind -> Bool
+okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
+okArrowArgKind    _                = False
+
+okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
+okArrowResultKind _                = False
+
+-----------------------------------------
+--              Subkinding
 -- The tc variants are used during type-checking, where we don't want the
 -- Constraint kind to be a subkind of anything
 -- After type-checking (in core), Constraint is a subkind of argTypeKind
-isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool
+isSubOpenTypeKind :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
 isSubOpenTypeKind _                = False
 
--- ^ True of any sub-kind of OpenTypeKind
-tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc
-tcIsSubOpenTypeKind _                = False
-
 isSubOpenTypeKindCon kc
-  | isSubArgTypeKindCon kc   = True
-  | isUbxTupleKindCon kc     = True
-  | isOpenTypeKindCon kc     = True
-  | otherwise                = False
-
-tcIsSubOpenTypeKindCon kc
-  | tcIsSubArgTypeKindCon kc = True
-  | isUbxTupleKindCon kc     = True
-  | isOpenTypeKindCon kc     = True
-  | otherwise                = False
+  =  isSubArgTypeKindCon kc
+  || isUbxTupleKindCon   kc
+  || isOpenTypeKindCon   kc
+  || isConstraintKindCon kc   -- Needed for error (Num a) "blah"
+                              -- and so that (Ord a -> Eq a) is well-kinded
 
 isSubArgTypeKindCon kc
-  | isUnliftedTypeKindCon kc = True
-  | isLiftedTypeKindCon kc   = True
-  | isArgTypeKindCon kc      = True
-  | isConstraintKindCon kc   = True
-  | otherwise                = False
+  =  isUnliftedTypeKindCon kc
+  || isLiftedTypeKindCon   kc  
+  || isArgTypeKindCon      kc     
 
-tcIsSubArgTypeKindCon kc
-  | isConstraintKindCon kc   = False
-  | otherwise                = isSubArgTypeKindCon kc
-
-isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool
+isSubArgTypeKind :: Kind -> Bool
 -- ^ True of any sub-kind of ArgTypeKind 
 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
 isSubArgTypeKind _                = False
 
-tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc
-tcIsSubArgTypeKind _                = False
-
--- | Is this a super-kind (i.e. a type-of-kinds)?
-isSuperKind :: Type -> Bool
-isSuperKind (TyConApp skc []) = isSuperKindTyCon skc
-isSuperKind _                 = False
-
-isSuperKindTyCon :: TyCon -> Bool
-isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
-
 -- | Is this a kind (i.e. a type-of-types)?
 isKind :: Kind -> Bool
 isKind k = isSuperKind (typeKind k)
 
-isSubKind, tcIsSubKind :: Kind -> Kind -> Bool
-isSubKind   = isSubKind' False
-tcIsSubKind = isSubKind' True
-
--- The first argument denotes whether we are in the type-checking phase or not
-isSubKind' :: Bool -> Kind -> Kind -> Bool
+isSubKind :: Kind -> Kind -> Bool
 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
 
-isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2)
-  = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2)
+isSuperKindTyCon :: TyCon -> Bool
+isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
+
+isSubKind (FunTy a1 r1) (FunTy a2 r2)
+  = (isSubKind a2 a1) && (isSubKind r1 r2)
 
-isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
+isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
   | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
     -- handles promoted kinds (List *, Nat, etc.)
-    = eqKind k1 k2
+  = eqKind k1 k2
 
   | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
     -- handles BOX
-    = WARN( not (isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
-                  && null k1s && null k2s), 
+  = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
+             && null k1s && null k2s, 
              ppr kc1 <+> ppr kc2 )
-      kc1 == kc2
+    True   -- If one is BOX, the other must be too
 
   | otherwise = -- handles usual kinds (*, #, (#), etc.)
                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
-                if duringTc then kc1 `tcIsSubKindCon` kc2
-                else kc1 `isSubKindCon` kc2
+                kc1 `isSubKindCon` kc2
 
-isSubKind' _duringTc k1 k2 = eqKind k1 k2
+isSubKind k1 k2 = eqKind k1 k2
 
 isSubKindCon :: TyCon -> TyCon -> Bool
 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
 isSubKindCon kc1 kc2
-  | kc1 == kc2                                             = True
-  | isSubArgTypeKindCon  kc1  && isArgTypeKindCon  kc2     = True
-  | isSubOpenTypeKindCon kc1  && isOpenTypeKindCon kc2     = True
-  | otherwise                                              = False
+  | kc1 == kc2            = True
+  | isArgTypeKindCon  kc2 = isSubArgTypeKindCon  kc1
+  | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 
+  | otherwise             = False
+
+-------------------------
+-- Hack alert: we need a tiny variant for the typechecker
+-- Reason:     f :: Int -> (a~b)
+--             g :: forall (c::Constraint). Int -> c
+-- We want to reject these, even though Constraint is
+-- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
+-- *after* the typechecker
+--   a) So that (Ord a -> Eq a) is a legal type
+--   b) So that the simplifer can generate (error (Eq a) "urk")
+--
+-- Easiest way to reject is simply to make Constraint not
+-- below OpenTypeKind when type checking
+
+tcIsSubKind :: Kind -> Kind -> Bool
+tcIsSubKind k1 k2
+  | isConstraintKind k1 = isConstraintKind k2
+  | otherwise           = isSubKind k1 k2
 
 tcIsSubKindCon :: TyCon -> TyCon -> Bool
 tcIsSubKindCon kc1 kc2
-  | kc1 == kc2                                         = True
-  | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False
-  | otherwise                                          = isSubKindCon kc1 kc2
+  | isConstraintKindCon kc1 = isConstraintKindCon kc2
+  | otherwise               = isSubKindCon kc1 kc2
 
+-------------------------
 defaultKind :: Kind -> Kind
 -- ^ Used when generalising: default OpenKind and ArgKind to *.
 -- See "Type#kind_subtyping" for more information on what that means
@@ -294,20 +276,8 @@ defaultKind :: Kind -> Kind
 -- and the calling conventions differ.
 -- This defaulting is done in TcMType.zonkTcTyVarBndr.
 defaultKind k
-  | tcIsSubOpenTypeKind k = liftedTypeKind
-  | otherwise             = k
-
-splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
--- Precondition: kind variables should precede type variables
--- Postcondition: appending the two result lists gives the input!
-splitKiTyVars = span (isSuperKind . tyVarKind)
-
-partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
-partitionKiTyVars = partition (isSuperKind . tyVarKind)
-
--- Checks if this "type or kind" variable is a kind variable
-isKiVar :: TyVar -> Bool
-isKiVar v = isSuperKind (varType v)
+  | isSubOpenTypeKind k = liftedTypeKind
+  | otherwise           = k
 
 -- Returns the free kind variables in a kind
 kiVarsOfKind :: Kind -> VarSet
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index dbb2c5e0bb..114e3e9cfc 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -63,6 +63,7 @@ module Type (
         funTyCon,
 
         -- ** Predicates on types
+        isTypeVar, isKindVar,
         isTyVarTy, isFunTy, isDictTy, isPredTy, isKindTy,
 
 	-- (Lifting and boxity)
@@ -89,7 +90,7 @@ module Type (
 	-- * Type free variables
 	tyVarsOfType, tyVarsOfTypes,
 	expandTypeSynonyms, 
-	typeSize, varSetElemsKvsFirst, sortQuantVars,
+	typeSize, varSetElemsKvsFirst, 
 
 	-- * Type comparison
         eqType, eqTypeX, eqTypes, cmpType, cmpTypes, 
@@ -165,6 +166,7 @@ import Util
 import Outputable
 import FastString
 
+import Data.List        ( partition )
 import Maybes		( orElse )
 import Data.Maybe	( isJust )
 
@@ -689,8 +691,8 @@ mkPiKinds :: [TyVar] -> Kind -> Kind
 -- returns forall k1 k2. (k1 -> *) -> k2
 mkPiKinds [] res = res
 mkPiKinds (tv:tvs) res 
-  | isKiVar tv = ForAllTy tv          (mkPiKinds tvs res)
-  | otherwise  = FunTy (tyVarKind tv) (mkPiKinds tvs res)
+  | isKindVar tv = ForAllTy tv          (mkPiKinds tvs res)
+  | otherwise    = FunTy (tyVarKind tv) (mkPiKinds tvs res)
 
 mkPiType  :: Var -> Type -> Type
 -- ^ Makes a @(->)@ type or a forall type, depending
@@ -975,23 +977,10 @@ typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
 
 varSetElemsKvsFirst :: VarSet -> [TyVar]
 -- {k1,a,k2,b} --> [k1,k2,a,b]
-varSetElemsKvsFirst set = uncurry (++) $ partitionKiTyVars (varSetElems set)
-
-sortQuantVars :: [Var] -> [Var]
--- Sort the variables so the true kind then type variables come first
-sortQuantVars = sortLe le
+varSetElemsKvsFirst set 
+  = kvs ++ tvs
   where
-    v1 `le` v2 = case (is_tv v1, is_tv v2) of
-                   (True, False)  -> True
-                   (False, True)  -> False
-                   (True, True)   ->
-                     case (is_kv v1, is_kv v2) of
-                       (True, False) -> True
-                       (False, True) -> False
-                       _             -> v1 <= v2  -- Same family
-                   (False, False) -> v1 <= v2
-    is_tv v = isTyVar v
-    is_kv v = isSuperKind (tyVarKind v)
+    (kvs, tvs) = partition isKindVar (varSetElems set)
 \end{code}