User manual update, as prodded by #10760.
authorRichard Eisenberg <eir@cis.upenn.edu>
Tue, 11 Aug 2015 13:05:30 +0000 (09:05 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Tue, 11 Aug 2015 13:05:30 +0000 (09:05 -0400)
This clarifies that kind variables are inputs to type families
and can be used to distinguish instances.

docs/users_guide/glasgow_exts.xml

index d1a908e..8b597da 100644 (file)
@@ -6247,7 +6247,18 @@ F Char [Int] Bool  -- OK!  Kind: *
 F IO Bool          -- WRONG: kind mismatch in the first argument
 F Bool             -- WRONG: unsaturated application
 </programlisting>
-      </para>
+    </para>
+
+    <para>
+      The result kind annotation is optional and defaults to
+      <literal>*</literal> (like argument kinds) if
+      omitted. Polykinded type families can be
+      declared using a parameter in the kind annotation:
+<programlisting>
+type family F a :: k
+</programlisting>
+In this case the kind parameter <literal>k</literal> is actually an implicit
+parameter of the type family.
     </sect3>
 
   <sect3 id="type-instance-declarations">
@@ -6365,7 +6376,7 @@ type instance G Int Char Float = Double  -- WRONG: must be two type parameters
        are restricted to be <firstterm>compatible</firstterm>. Two type patterns
        are compatible if
 <orderedlist>
-<listitem><para>all corresponding types in the patterns are <firstterm>apart</firstterm>, or</para></listitem>
+<listitem><para>all corresponding types and implicit kinds in the patterns are <firstterm>apart</firstterm>, or</para></listitem>
 <listitem><para>the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.</para></listitem>
 </orderedlist>
         Two types are considered <firstterm>apart</firstterm> if, for all possible
@@ -6392,7 +6403,17 @@ type instance G (Char, a) = [a]  -- ILLEGAL overlap, as [Char] /= [Int]
 </programlisting>
        Note that this compatibility condition is independent of whether the type family
        is associated or not, and it is not only a matter of consistency, but
-       one of type safety. </para>
+      one of type safety. </para>
+
+      <para>For a polykinded type family, the kinds are checked for
+      apartness just like types. For example, the following is accepted:
+<programlisting>
+type family J a :: k
+type instance J Int = Bool
+type instance J Int = Maybe
+</programlisting>
+      These instances are compatible because they differ in their implicit kind parameter; the first uses <literal>*</literal> while the second uses <literal>* -> *</literal>.</para>
+
 
        <para>
          The definition for "compatible" uses a notion of "apart", whose definition