6.11.3. Explicitly-kinded quantification¶
-
KindSignatures
¶ Implied by: TypeFamilies
,PolyKinds
Since: 6.8.1 Status: Included in GHC2024
,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]
newtype
declarations:newtype 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.