6.11.3. Explicitly-kinded quantification¶

KindSignatures¶

Implied by:	`TypeFamilies`, `PolyKinds`
Since:	6.8.1
Status:	Included in `GHC2021`

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.