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

1 files changed, 42 insertions, 2 deletions

diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 0c4c890ada..57f94b4a76 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -5813,7 +5813,7 @@ very convenient, and it is not clear what the syntax for explicit quantification
 </para>
 </sect2>
 
-<sect2> <title>Polymorphic kind recursion and complete kind signatures</title>
+<sect2 id="complete-kind-signatures"> <title>Polymorphic kind recursion and complete kind signatures</title>
 
 <para>
 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.
 </para></listitem>
 
 <listitem><para>
-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:
 <programlisting>
 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 -> * -> *
 </programlisting>
+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>.
 </para></listitem>
 </itemizedlist>
 In a complete user-specified kind signature, any un-decorated type variable to the
@@ -5874,6 +5881,39 @@ If you want kind polymorphism, specify a kind variable.
 </para>
 
 </sect2>
+
+<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.
+</para>
+
+<para>
+Here are some examples (assuming <literal>-XDataKinds</literal> is enabled):
+<programlisting>
+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
+</programlisting>
+</para>
+
+</sect2>
 </sect1>
 
 <sect1 id="promotion">