Standard Haskell has a rich type language. Types classify terms and serve to avoid many common programming mistakes. The kind language, however, is relatively simple, distinguishing only lifted types (kind *), type constructors (eg. kind * -> * -> *), and unlifted types (Section 7.2.1, “Unboxed types”). In particular when using advanced type system features, such as type families (Section 7.7, “Type families”) or GADTs (Section 7.4.7, “Generalised Algebraic Data Types (GADTs)”), this simple kind system is insufficient, and fails to prevent simple errors. Consider the example of type-level natural numbers, and length-indexed vectors:

data Ze
data Su n

data Vec :: * -> * -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

The kind of Vec is * -> * -> *. This means that eg. Vec Int Char is a well-kinded type, even though this is not what we intend when defining length-indexed vectors.

With -XDataKinds, the example above can then be rewritten to:

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

With the improved kind of Vec, things like Vec Int Char are now ill-kinded, and GHC will report an error.

With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors. The following types

data Nat = Ze | Su Nat

data List a = Nil | Cons a (List a)

data Pair a b = Pair a b
 
data Sum a b = L a | R b

give rise to the following kinds and type constructors:

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

List k :: BOX
Nil  :: List k
Cons :: k -> List k -> List k

Pair k1 k2 :: BOX
Pair :: k1 -> k2 -> Pair k1 k2

Sum k1 k2 :: BOX
L :: k1 -> Sum k1 k2
R :: k2 -> Sum k1 k2

where BOX is the (unique) sort that classifies kinds. Note that List, for instance, does not get sort BOX -> BOX, because we do not further classify kinds; all kinds have sort BOX.

The following restrictions apply to promotion:

Since constructors and types share the same namespace, with promotion you can get ambiguous type names:

data P          -- 1

data Prom = P   -- 2

type T = P      -- 1 or promoted 2?

In these cases, if you want to refer to the promoted constructor, you should prefix its name with a quote:

type T1 = P     -- 1

type T2 = 'P    -- promoted 2

Note that promoted datatypes give rise to named kinds. Since these can never be ambiguous, we do not allow quotes in kind names.

Just as in the case of Template Haskell (Section 7.14.1, “Syntax”), there is no way to quote a data constructor or type constructor whose second character is a single quote.

Haskell's list and tuple types are natively promoted to kinds, and enjoy the same convenient syntax at the type level, albeit prefixed with a quote:

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (*,*) -> * where
  Tuple :: a -> b -> Tuple '(a,b)

Note that this requires -XTypeOperators.

Numeric and string literals are promoted to the type level, giving convenient access to a large number of predefined type-level constants. Numeric literals are of kind Nat, while string literals are of kind Symbol. These kinds are defined in the module GHC.TypeLits.

Here is an exampe of using type-level numeric literals to provide a safe interface to a low-level function:

import GHC.TypeLits
import Data.Word
import Foreign

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

clearPage :: ArrPtr 4096 Word8 -> IO ()
clearPage (ArrPtr p) = ...

Here is an example of using type-level string literals to simulate simple record operations:

data Label (l :: Symbol) = Get

class Has a l b | a l -> b where
  from :: a -> Label l -> b

data Point = Point Int Int deriving Show

instance Has Point "x" Int where from (Point x _) _ = x
instance Has Point "y" Int where from (Point _ y) _ = y

example = from (Point 1 2) (Get :: Label "x")

Note that we do promote existential data constructors that are otherwise suitable. For example, consider the following:

data Ex :: * where
  MkEx :: forall a. a -> Ex

Both the type Ex and the data constructor MkEx get promoted, with the polymorphic kind 'MkEx :: forall k. k -> Ex. Somewhat surprisingly, you can write a type family to extract the member of a type-level existential:

type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x

At first blush, UnEx seems poorly-kinded. The return kind k is not mentioned in the arguments, and thus it would seem that an instance would have to return a member of k for any k. However, this is not the case. The type family UnEx is a kind-indexed type family. The return kind k is an implicit parameter to UnEx. The elaborated definitions are as follows:

type family UnEx (k :: BOX) (ex :: Ex) :: k
type instance UnEx k (MkEx k x) = x

Thus, the instance triggers only when the implicit parameter to UnEx matches the implicit parameter to MkEx. Because k is actually a parameter to UnEx, the kind is not escaping the existential, and the above code is valid.

See also Trac #7347.