TODO This page is somewhat old. It needs to be updated with recent information. The followings are the latest related information.
GHC User's Guide:
Kinds classify types. So for example:
Int :: * Int -> Int :: * Maybe :: * -> * Int# :: # (# Int, Int #) :: #
The base kinds are these:
*" is the kind of lifted, boxed values. Things like
Maybe Floathave kind
#" is the kind of unlifted values. Things like
- With the advent of data type promotion and kind polymorphism we can have a lot more kinds.
- Kinds are in flux with levity polymorphism. See LevityPolymorphism. See also TypeType.
(Unboxed tuples used to have a distinct kind, but in 2012 we combined unboxed tuples with other unboxed values in a single kind "
Kinds are represented by the data type
Type (see Commentary/Compiler/TypeType):
type Kind = Type
Basic kinds are
represented using type constructors, e.g. the kind
* is represented as
liftedTypeKind :: Kind liftedTypeKind = TyConApp liftedTypeKindTyCon 
liftedTypeKindTyCon is a built-in
PrimTyCon. The arrow type
constructor is used as the arrow kind constructor, e.g. the kind
* -> *
is represented internally as
FunTy liftedTypeKind liftedTypeKind
It's easy to extract the kind of a type, or the sort of a kind:
typeKind :: Type -> Kind
The "sort" of a kind is always one of the
TY (for kinds that classify normal types) or
CO (for kinds that
classify coercion evidence). The coercion kind,
T1 :=: T2, is
PredTy (EqPred T1 T2).
There is a small amount of sub-typing in kinds. Suppose you see
(t1 -> t2). What kind must
t2 have? It could be
#. So we have a single kind
OpenKind, which is a super-kind of both, with this simple lattice:
(You can edit this picture here.)