+
+ subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
+ -- It's only worth doing the substitution for coercions,
+ -- becuase only they can have free type variables
+ | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
+ | otherwise = old_var
+\end{code}
+
+----------------------------------------------------
+-- Kind Stuff
+
+Kinds
+~~~~~
+There's a little subtyping at the kind level:
+
+ ?
+ / \
+ / \
+ ?? (#)
+ / \
+ * #
+
+where * [LiftedTypeKind] means boxed type
+ # [UnliftedTypeKind] means unboxed type
+ (#) [UbxTupleKind] means unboxed tuple
+ ?? [ArgTypeKind] is the lub of *,#
+ ? [OpenTypeKind] means any type at all
+
+In particular:
+
+ error :: forall a:?. String -> a
+ (->) :: ?? -> ? -> *
+ (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
+
+\begin{code}
+type KindVar = TyVar -- invariant: KindVar will always be a
+ -- TcTyVar with details MetaTv TauTv ...
+-- kind var constructors and functions are in TcType
+
+type SimpleKind = Kind
+\end{code}
+
+Kind inference
+~~~~~~~~~~~~~~
+During kind inference, a kind variable unifies only with
+a "simple kind", sk
+ sk ::= * | sk1 -> sk2
+For example
+ data T a = MkT a (T Int#)
+fails. We give T the kind (k -> *), and the kind variable k won't unify
+with # (the kind of Int#).
+
+Type inference
+~~~~~~~~~~~~~~
+When creating a fresh internal type variable, we give it a kind to express
+constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
+with kind ??.
+
+During unification we only bind an internal type variable to a type
+whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
+
+When unifying two internal type variables, we collect their kind constraints by
+finding the GLB of the two. Since the partial order is a tree, they only
+have a glb if one is a sub-kind of the other. In that case, we bind the
+less-informative one to the more informative one. Neat, eh?
+
+
+\begin{code}
+
+\end{code}
+
+%************************************************************************
+%* *
+ Functions over Kinds
+%* *
+%************************************************************************
+
+\begin{code}
+kindFunResult :: Kind -> Kind
+kindFunResult k = funResultTy k
+
+splitKindFunTys :: Kind -> ([Kind],Kind)
+splitKindFunTys k = splitFunTys k
+
+splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
+splitKindFunTysN k = splitFunTysN k
+
+isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
+
+isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
+
+isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
+isOpenTypeKind other = False
+
+isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
+
+isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
+isUbxTupleKind other = False
+
+isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
+
+isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
+isArgTypeKind other = False
+
+isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+
+isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
+isUnliftedTypeKind other = False
+
+isSubOpenTypeKind :: Kind -> Bool
+-- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
+isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
+ ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
+ False
+isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
+isSubOpenTypeKind other = ASSERT( isKind other ) False
+ -- This is a conservative answer
+ -- It matters in the call to isSubKind in
+ -- checkExpectedKind.
+
+isSubArgTypeKindCon kc
+ | isUnliftedTypeKindCon kc = True
+ | isLiftedTypeKindCon kc = True
+ | isArgTypeKindCon kc = True
+ | otherwise = False
+
+isSubArgTypeKind :: Kind -> Bool
+-- True of any sub-kind of ArgTypeKind
+isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
+isSubArgTypeKind other = False
+
+isSuperKind :: Type -> Bool
+isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
+isSuperKind other = False
+
+isKind :: Kind -> Bool
+isKind k = isSuperKind (typeKind k)
+
+isSubKind :: Kind -> Kind -> Bool
+-- (k1 `isSubKind` k2) checks that k1 <: k2
+isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
+isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
+ = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
+isSubKind k1 k2 = False
+
+eqKind :: Kind -> Kind -> Bool
+eqKind = tcEqType
+
+isSubKindCon :: TyCon -> TyCon -> Bool
+-- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
+isSubKindCon kc1 kc2
+ | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
+ | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
+ | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
+ | isOpenTypeKindCon kc2 = True
+ -- we already know kc1 is not a fun, its a TyCon
+ | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
+ | otherwise = False
+
+defaultKind :: Kind -> Kind
+-- Used when generalising: default kind '?' and '??' to '*'
+--
+-- When we generalise, we make generic type variables whose kind is
+-- simple (* or *->* etc). So generic type variables (other than
+-- built-in constants like 'error') always have simple kinds. This is important;
+-- consider
+-- f x = True
+-- We want f to get type
+-- f :: forall (a::*). a -> Bool
+-- Not
+-- f :: forall (a::??). a -> Bool
+-- because that would allow a call like (f 3#) as well as (f True),
+--and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
+defaultKind k
+ | isSubOpenTypeKind k = liftedTypeKind
+ | isSubArgTypeKind k = liftedTypeKind
+ | otherwise = k
+
+isEqPred :: PredType -> Bool
+isEqPred (EqPred _ _) = True
+isEqPred other = False