6.11.4. Explicitly-kinded quantification

KindSignatures

Since:6.8.1

Allow explicit kind signatures on type variables.

Haskell infers the kind of each type variable. Sometimes it is nice to be able to give the kind explicitly as (machine-checked) documentation, just as it is nice to give a type signature for a function. On some occasions, it is essential to do so. For example, in his paper “Restricted Data Types in Haskell” (Haskell Workshop 1999) John Hughes had to define the data type:

data Set cxt a = Set [a]
               | Unused (cxt a -> ())

The only use for the Unused constructor was to force the correct kind for the type variable cxt.

GHC now instead allows you to specify the kind of a type variable directly, wherever a type variable is explicitly bound, with the extension KindSignatures.

This extension enables kind signatures in the following places:

• data declarations:

  data Set (cxt :: Type -> Type) a = Set [a]
  

• type declarations:

  type T (f :: Type -> Type) = f Int
  

• class declarations:

  class (Eq a) => C (f :: Type -> Type) a where ...
  

• forall‘s in type signatures:

  f :: forall (cxt :: Type -> Type). Set cxt Int
  

The parentheses are required.

As part of the same extension, you can put kind annotations in types as well. Thus:

f :: (Int :: Type) -> Int
g :: forall a. a -> (a :: Type)

The syntax is

atype ::= '(' ctype '::' kind ')

The parentheses are required.