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 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 signature
(`-XPolyKinds`

implies `-XKindSignatures`

):

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

There is no "forall" for kind variables. Instead, you can simply mention a kind variable in a kind signature, thus:

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

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.A type or data family declaration

*always*have 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 -> *

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.