This section describes *kind polymorphism*, and extension
enabled by `-XPolyKinds`

.
It is described in more detail in the paper
Giving Haskell a
Promotion, which appeared at TLDI 2012.

Currently there is a lot of code duplication in the way Typeable is implemented
(Section 7.5.3, “Deriving clause for extra classes (`Typeable`

, `Data`

, etc)”):

class Typeable (t :: *) where typeOf :: t -> TypeRep class Typeable1 (t :: * -> *) where typeOf1 :: t a -> TypeRep class Typeable2 (t :: * -> * -> *) where typeOf2 :: t a b -> TypeRep

Kind polymorphism (with `-XPolyKinds`

)
allows us to merge all these classes into one:

data Proxy t = Proxy class Typeable t where typeOf :: Proxy t -> TypeRep instance Typeable Int where typeOf _ = TypeRep instance Typeable [] where typeOf _ = TypeRep

Note that the datatype `Proxy`

has kind
`forall k. k -> *`

(inferred by GHC), and the new
`Typeable`

class has kind
`forall k. k -> Constraint`

.

Generally speaking, with `-XPolyKinds`

, GHC will infer a polymorphic
kind for un-decorated declarations, whenever possible. For example:

data T m a = MkT (m a) -- GHC infers kind T :: forall k. (k -> *) -> k -> *

Just as in the world of terms, you can restrict polymorphism using a
kind signature (sometimes called a kind annotation)
(`-XPolyKinds`

implies `-XKindSignatures`

):

data T m (a :: *) = MkT (m a) -- GHC now infers kind T :: (* -> *) -> * -> *

There is no "forall" for kind variables. Instead, when binding a type variable, you can simply mention a kind variable in a kind annotation for that type-variable binding, thus:

data T (m :: k -> *) a = MkT (m a) -- GHC now infers kind T :: forall k. (k -> *) -> k -> *

The kind "forall" is placed just outside the outermost type-variable binding whose kind annotation mentions the kind variable. For example

f1 :: (forall a m. m a -> Int) -> Int -- f1 :: forall (k:BOX). -- (forall (a:k) (m:k->*). m a -> Int) -- -> Int f2 :: (forall (a::k) m. m a -> Int) -> Int -- f2 :: (forall (k:BOX) (a:k) (m:k->*). m a -> Int) -- -> Int

Here in `f1`

there is no kind annotation mentioning the polymorphic
kind variable, so `k`

is generalised at the top
level of the signature for `f1`

,
making the signature for `f1`

is as polymorphic as possible.
But in the case of of `f2`

we give a kind annotation in the `forall (a:k)`

binding, and GHC therefore puts the kind `forall`

right there too.

(Note: These rules are a bit indirect and clumsy. Perhaps GHC should allow explicit kind quantification. But the implicit quantification (e.g. in the declaration for data type T above) is certainly very convenient, and it is not clear what the syntax for explicit quantification should be.)

Just as in type inference, kind inference for recursive types can only use *monomorphic* recursion.
Consider this (contrived) example:

data T m a = MkT (m a) (T Maybe (m a)) -- GHC infers kind T :: (* -> *) -> * -> *

The recursive use of `T`

forced the second argument to have kind `*`

.
However, just as in type inference, you can achieve polymorphic recursion by giving a
*complete kind signature* for `T`

. The way to give
a complete kind signature for a data type is to use a GADT-style declaration with an
explicit kind signature thus:

data T :: (k -> *) -> k -> * where MkT :: m a -> T Maybe (m a) -> T m a

The complete user-supplied kind signature specifies the polymorphic kind for `T`

,
and this signature is used for all the calls to `T`

including the recursive ones.
In particular, the recursive use of `T`

is at kind `*`

.

What exactly is considered to be a "complete user-supplied kind signature" for a type constructor? These are the forms:

A GADT-style data type declaration, with an explicit "

`::`

" in the header. For example:data T1 :: (k -> *) -> k -> * where ... -- Yes T1 :: forall k. (k->*) -> k -> * data T2 (a :: k -> *) :: k -> * where ... -- Yes T2 :: forall k. (k->*) -> k -> * data T3 (a :: k -> *) (b :: k) :: * where ... -- Yes T3 :: forall k. (k->*) -> k -> * data T4 a (b :: k) :: * where ... -- YES T4 :: forall k. * -> k -> * data T5 a b where ... -- NO kind is inferred data T4 (a :: k -> *) (b :: k) where ... -- NO kind is inferred

It makes no difference where you put the "

`::`

" but it must be there. You cannot give a complete kind signature using a Haskell-98-style data type declaration; you must use GADT syntax.An open type or data family declaration

*always*has a complete user-specified kind signature; no "`::`

" is required:data family D1 a -- D1 :: * -> * data family D2 (a :: k) -- D2 :: forall k. k -> * data family D3 (a :: k) :: * -- D3 :: forall k. k -> * type family S1 a :: k -> * -- S1 :: forall k. * -> k -> * class C a where -- C :: k -> Constraint type AT a b -- AT :: k -> * -> *

In the last example, the variable

`a`

has an implicit kind variable annotation from the class declaration. It keeps its polymorphic kind in the associated type declaration. The variable`b`

, however, gets defaulted to`*`

.

In a complete user-specified kind signature, any un-decorated type variable to the
left of the "`::`

" is considered to have kind "`*`

".
If you want kind polymorphism, specify a kind variable.

Although all open type families are considered to have a complete user-specified kind signature, we can relax this condition for closed type families, where we have equations on which to perform kind inference. GHC will infer a kind for any type variable in a closed type family when that kind is never used in pattern-matching. If you want a kind variable to be used in pattern-matching, you must declare it explicitly.

Here are some examples (assuming `-XDataKinds`

is enabled):

type family Not a where -- Not :: Bool -> Bool Not False = True Not True = False type family F a where -- ERROR: requires pattern-matching on a kind variable F Int = Bool F Maybe = Char type family G (a :: k) where -- G :: k -> * G Int = Bool G Maybe = Char type family SafeHead where -- SafeHead :: [k] -> Maybe k SafeHead '[] = Nothing -- note that k is not required for pattern-matching SafeHead (h ': t) = Just h

Consider the following example of a poly-kinded class and an instance for it:

class C a where type F a instance C b where type F b = b -> b

In the class declaration, nothing constrains the kind of the type
`a`

, so it becomes a poly-kinded type variable `(a :: k)`

.
Yet, in the instance declaration, the right-hand side of the associated type instance
`b -> b`

says that `b`

must be of kind `*`

. GHC could theoretically propagate this information back into the instance head, and
make that instance declaration apply only to type of kind `*`

, as opposed
to types of any kind. However, GHC does *not* do this.

In short: GHC does *not* propagate kind information from
the members of a class instance declaration into the instance declaration head.

This lack of kind inference is simply an engineering problem within GHC, but
getting it to work would make a substantial change to the inference infrastructure,
and it's not clear the payoff is worth it. If you want to restrict `b`

's
kind in the instance above, just use a kind signature in the instance head.