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.4, “Deriving `Typeable`

instances”):

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`

. A complete
kind signature is present when all argument kinds and the result kind are known, without
any need for inference. For example:

data T (m :: 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:

For a datatype, every type variable must be annotated with a kind. In a GADT-style declaration, there may also be a kind signature (with a top-level

`::`

in the header), but the presence or absence of this annotation does not affect whether or not the declaration has a complete signature.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 :: k -> *) (b :: k) where ... -- Yes T4 :: forall k. (k->*) -> k -> * data T5 a (b :: k) :: * where ... -- NO kind is inferred data T6 a b where ... -- NO kind is inferred

For a class, every type variable must be annotated with a kind.

For a type synonym, every type variable and the result type must all be annotated with kinds.

type S1 (a :: k) = (a :: k) -- Yes S1 :: forall k. k -> k type S2 (a :: k) = a -- No kind is inferred type S3 (a :: k) = Proxy a -- No kind is inferred

Note that in

`S2`

and`S3`

, the kind of the right-hand side is rather apparent, but it is still not considered to have a complete signature -- no inference can be done before detecting the signature.An open type or data family declaration

*always*has a complete user-specified kind signature; un-annotated type variables default to kind`*`

.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`*`

.A closed type familey has a complete signature when all of its type variables are annotated and a return kind (with a top-level

`::`

) is supplied.

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 kinds for the arguments and result types of a closed type family.

GHC supports *kind-indexed* type families, where the
family matches both on the kind and type. GHC will *not* infer
this behaviour without a complete user-supplied kind signature, as doing so would
sometimes infer non-principal types.

For example:

type family F1 a where F1 True = False F1 False = True F1 x = x -- F1 fails to compile: kind-indexing is not inferred type family F2 (a :: k) where F2 True = False F2 False = True F2 x = x -- F2 fails to compile: no complete signature type family F3 (a :: k) :: k where F3 True = False F3 False = True F3 x = x -- OK

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.