[Improve documentation of data type declarations (Trac #1901)
simonpj@microsoft.com**20071116081841] {
hunk ./docs/users_guide/glasgow_exts.xml 1692
-<sect3>
-<title>Type classes</title>
+<sect3 id="existential-with-context">
+<title>Existentials and type classes</title>
hunk ./docs/users_guide/glasgow_exts.xml 2019
-<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>
hunk ./docs/users_guide/glasgow_exts.xml 2020
-For example, a possible application of GHC's behaviour is to reify dictionaries:
+For example, one possible application is to reify dictionaries:
hunk ./docs/users_guide/glasgow_exts.xml 2034
+<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>
}