Improve documentation of data type declarations (Trac #1901)

[ghc-hetmet.git] / docs / users_guide / glasgow_exts.xml

diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 4f02239..a01dea4 100644 (file)
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -1689,8 +1689,8 @@ adding a new existential quantification construct.
 
 </sect3>
 
-<sect3>
-<title>Type classes</title>
+<sect3 id="existential-with-context">
+<title>Existentials and type classes</title>
 
 <para>
 An easy extension is to allow
@@ -2016,19 +2016,8 @@ In the example, the equality dictionary is used to satisfy the equality constrai
 generated by the call to <literal>elem</literal>, so that the type of
 <literal>insert</literal> itself has no <literal>Eq</literal> constraint.
 </para>
-<para>This behaviour contrasts with Haskell 98's peculiar treatment of 
-contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
-In Haskell 98 the definition
-<programlisting>
-  data Eq a => Set' a = MkSet' [a]
-</programlisting>
-gives <literal>MkSet'</literal> the same type as <literal>MkSet</literal> above.  But instead of 
-<emphasis>making available</emphasis> an <literal>(Eq a)</literal> constraint, pattern-matching
-on <literal>MkSet'</literal> <emphasis>requires</emphasis> an <literal>(Eq a)</literal> constraint!
-GHC faithfully implements this behaviour, odd though it is.  But for GADT-style declarations,
-GHC's behaviour is much more useful, as well as much more intuitive.</para>
 <para>
-For example, a possible application of GHC's behaviour is to reify dictionaries:
+For example, one possible application is to reify dictionaries:
 <programlisting>
    data NumInst a where
      MkNumInst :: Num a => NumInst a
@@ -2042,6 +2031,38 @@ For example, a possible application of GHC's behaviour is to reify dictionaries:
 Here, a value of type <literal>NumInst a</literal> is equivalent 
 to an explicit <literal>(Num a)</literal> dictionary.
 </para>
+<para>
+All this applies to constructors declared using the syntax of <xref linkend="existential-with-context"/>.
+For example, the <literal>NumInst</literal> data type above could equivalently be declared 
+like this:
+<programlisting>
+   data NumInst a 
+      = Num a => MkNumInst (NumInst a)
+</programlisting>
+Notice that, unlike the situation when declaring an existental, there is 
+no <literal>forall</literal>, because the <literal>Num</literal> constrains the
+data type's univerally quantified type variable <literal>a</literal>.  
+A constructor may have both universal and existential type variables: for example,
+the following two declarations are equivalent:
+<programlisting>
+   data T1 a 
+       = forall b. (Num a, Eq b) => MkT1 a b
+   data T2 a where
+       MkT2 :: (Num a, Eq b) => a -> b -> T2 a
+</programlisting>
+</para>
+<para>All this behaviour contrasts with Haskell 98's peculiar treatment of 
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
+In Haskell 98 the definition
+<programlisting>
+  data Eq a => Set' a = MkSet' [a]
+</programlisting>
+gives <literal>MkSet'</literal> the same type as <literal>MkSet</literal> above.  But instead of 
+<emphasis>making available</emphasis> an <literal>(Eq a)</literal> constraint, pattern-matching
+on <literal>MkSet'</literal> <emphasis>requires</emphasis> an <literal>(Eq a)</literal> constraint!
+GHC faithfully implements this behaviour, odd though it is.  But for GADT-style declarations,
+GHC's behaviour is much more useful, as well as much more intuitive.
+</para>
 
 <para>
 The rest of this section gives further details about GADT-style data