Commit 6a25e927 authored by's avatar

Update user's guide for kind inference for closed type families.

parent 9b456df4
......@@ -5813,7 +5813,7 @@ very convenient, and it is not clear what the syntax for explicit quantification
<sect2> <title>Polymorphic kind recursion and complete kind signatures</title>
<sect2 id="complete-kind-signatures"> <title>Polymorphic kind recursion and complete kind signatures</title>
Just as in type inference, kind inference for recursive types can only use <emphasis>monomorphic</emphasis> recursion.
......@@ -5858,14 +5858,21 @@ you must use GADT syntax.
A type or data family declaration <emphasis>always</emphasis> have a
An open type or data family declaration <emphasis>always</emphasis> has a
complete user-specified kind signature; no "<literal>::</literal>" 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 -> *
class C a where -- C :: k -> Constraint
type AT a b -- AT :: k -> * -> *
In the last example, the variable <literal>a</literal> has an implicit kind
variable annotation from the class declaration. It keeps its polymorphic kind
in the associated type declaration. The variable <literal>b</literal>, however,
gets defaulted to <literal>*</literal>.
In a complete user-specified kind signature, any un-decorated type variable to the
......@@ -5873,6 +5880,39 @@ left of the "<literal>::</literal>" is considered to have kind "<literal>*</lite
If you want kind polymorphism, specify a kind variable.
<sect2><title>Kind inference in closed type families</title>
<para>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 a kind for any type variable in a closed type family when that kind is
never used in pattern-matching. If you want a kind variable to be used in
pattern-matching, you must declare it explicitly.
Here are some examples (assuming <literal>-XDataKinds</literal> is enabled):
type family Not a where -- Not :: Bool -> Bool
Not False = True
Not True = False
type family F a where -- ERROR: requires pattern-matching on a kind variable
F Int = Bool
F Maybe = Char
type family G (a :: k) where -- G :: k -> *
G Int = Bool
G Maybe = Char
type family SafeHead where -- SafeHead :: [k] -> Maybe k
SafeHead '[] = Nothing -- note that k is not required for pattern-matching
SafeHead (h ': t) = Just h
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment