+#include "HsVersions.h"
+
+import Unique ( Unique )
+import Outputable
+import DATA_IOREF
+\end{code}
+
+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:<any>. String -> a
+ (->) :: ?? -> ? -> *
+ (\(x::t) -> ...) Here t::<any> (i.e. not unboxed tuple)
+
+\begin{code}
+data Kind
+ = LiftedTypeKind -- *
+ | OpenTypeKind -- ?
+ | UnliftedTypeKind -- #
+ | UbxTupleKind -- (##)
+ | ArgTypeKind -- ??
+ | FunKind Kind Kind -- k1 -> k2
+ | KindVar KindVar
+ deriving( Eq )
+
+data KindVar = KVar Unique (IORef (Maybe SimpleKind))
+ -- INVARIANT: a KindVar can only be instantaited by a SimpleKind
+
+type SimpleKind = Kind
+ -- A SimpleKind has no ? or # kinds in it:
+ -- sk ::= * | sk1 -> sk2 | kvar
+
+instance Eq KindVar where
+ (KVar u1 _) == (KVar u2 _) = u1 == u2
+
+mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar
+mkKindVar = KVar
+\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?
+
+In the olden days, when we generalise, we make generic type variables
+whose kind is simple. So generic type variables (other than built-in
+constants like 'error') always have simple kinds. But I don't see any
+reason to do that any more (TcMType.zapTcTyVarToTyVar).
+
+
+\begin{code}
+liftedTypeKind = LiftedTypeKind
+unliftedTypeKind = UnliftedTypeKind
+openTypeKind = OpenTypeKind
+argTypeKind = ArgTypeKind
+ubxTupleKind = UbxTupleKind
+
+mkArrowKind :: Kind -> Kind -> Kind
+mkArrowKind k1 k2 = k1 `FunKind` k2
+
+mkArrowKinds :: [Kind] -> Kind -> Kind
+mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds