Improve documentation for the 7.8 release

* Document ExplicitNamespaces
* Improve documentation of ambiguity, and AllowAmbiguousTypes
* Improve documentation of overlapping/incoherent instance rules
* List language extensions in alphabetical order

2 files changed, 259 insertions, 212 deletions

diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml
index 648180c184..ee577e6ead 100644
--- a/docs/users_guide/flags.xml
+++ b/docs/users_guide/flags.xml
@@ -699,23 +699,10 @@
             <entry><option>-fno-glasgow-exts</option></entry>
           </row>
           <row>
-            <entry><option>-XOverlappingInstances</option></entry>
-            <entry>Enable <link linkend="instance-overlap">overlapping instances</link></entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoOverlappingInstances</option></entry>
-          </row>
-          <row>
-            <entry><option>-XIncoherentInstances</option></entry>
-            <entry>Enable <link linkend="instance-overlap">incoherent instances</link>.
-              Implies <option>-XOverlappingInstances</option> </entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoIncoherentInstances</option></entry>
-          </row>
-          <row>
-            <entry><option>-XUndecidableInstances</option></entry>
-            <entry>Enable <link linkend="undecidable-instances">undecidable instances</link></entry>
+            <entry><option>-firrefutable-tuples</option></entry>
+            <entry>Make tuple pattern matching irrefutable</entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoUndecidableInstances</option></entry>
+            <entry><option>-fno-irrefutable-tuples</option></entry>
           </row>
           <row>
             <entry><option>-fcontext-stack=N</option><replaceable>n</replaceable></entry>
@@ -724,6 +711,14 @@
             <entry></entry>
           </row>
           <row>
+            <entry><option>-XAllowAmbiguousTypes</option></entry>
+            <entry>Allow the user to write <link linkend="ambiguity">ambiguous types</link>, 
+                   and the type inference engine to infer them.
+                </entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoAllowAmbiguousTypes</option></entry>
+          </row>
+          <row>
             <entry><option>-XArrows</option></entry>
             <entry>Enable <link linkend="arrow-notation">arrow
                 notation</link> extension</entry>
@@ -731,6 +726,43 @@
             <entry><option>-XNoArrows</option></entry>
           </row>
           <row>
+            <entry><option>-XAutoDeriveTypeable</option></entry>
+            <entry>Automatically <link linkend="auto-derive-typeable">derive Typeable instances for every datatype and type class declaration</link>.
+            Implies <option>-XDeriveDataTypeable</option>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoAutoDeriveTypeable</option></entry>
+          </row>
+          <row>
+            <entry><option>-XConstraintKinds</option></entry>
+            <entry>Enable a <link linkend="constraint-kind">kind of constraints</link>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoConstraintKinds</option></entry>
+          </row>
+          <row>
+            <entry><option>-XDataKinds</option></entry>
+            <entry>Enable <link linkend="promotion">datatype promotion</link>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoDataKinds</option></entry>
+          </row>
+          <row>
+            <entry><option>-XDeriveDataTypeable</option></entry>
+            <entry>Enable <link linkend="deriving-typeable">deriving for the Data and Typeable classes</link>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoDeriveDataTypeable</option></entry>
+          </row>
+          <row>
+            <entry><option>-XDeriveGeneric</option></entry>
+            <entry>Enable <link linkend="deriving-typeable">deriving for the Generic class</link>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoDeriveGeneric</option></entry>
+          </row>
+          <row>
+            <entry><option>-XGeneralizedNewtypeDeriving</option></entry>
+            <entry>Enable <link linkend="newtype-deriving">newtype deriving</link>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoGeneralizedNewtypeDeriving</option></entry>
+          </row>
+          <row>
             <entry><option>-XDisambiguateRecordFields</option></entry>
             <entry>Enable <link linkend="disambiguate-fields">record
                 field disambiguation</link></entry>
@@ -738,6 +770,19 @@
             <entry><option>-XNoDisambiguateRecordFields</option></entry>
           </row>
           <row>
+            <entry><option>-XEmptyCase</option></entry>
+            <entry>Allow <link linkend="empty-case">empty case alternatives</link>
+                  </entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoEmptyCase</option></entry>
+          </row>
+          <row>
+            <entry><option>-XExtendedDefaultRules</option></entry>
+            <entry>Use GHCi's <link linkend="extended-default-rules">extended default rules</link> in a normal module</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoExtendedDefaultRules</option></entry>
+          </row>
+          <row>
             <entry><option>-XForeignFunctionInterface</option></entry>
             <entry>Enable <link linkend="ffi">foreign function interface</link> (implied by
               <option>-fglasgow-exts</option>)</entry>
@@ -745,6 +790,20 @@
             <entry><option>-XNoForeignFunctionInterface</option></entry>
           </row>
           <row>
+            <entry><option>-XGADTs</option></entry>
+            <entry>Enable <link linkend="gadt">generalised algebraic data types</link>.
+            </entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoGADTs</option></entry>
+          </row>
+          <row>
+            <entry><option>-XGADTSyntax</option></entry>
+            <entry>Enable <link linkend="gadt-style">generalised algebraic data type syntax</link>.
+            </entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoGADTSyntax</option></entry>
+          </row>
+          <row>
             <entry><option>-XGenerics</option></entry>
             <entry>Deprecated, does nothing. No longer enables <link linkend="generic-classes">generic classes</link>.
               See also GHC's support for
@@ -760,22 +819,17 @@
             <entry><option>-XNoImplicitParams</option></entry>
           </row>
           <row>
-            <entry><option>-firrefutable-tuples</option></entry>
-            <entry>Make tuple pattern matching irrefutable</entry>
-            <entry>dynamic</entry>
-            <entry><option>-fno-irrefutable-tuples</option></entry>
-          </row>
-          <row>
             <entry><option>-XNoImplicitPrelude</option></entry>
             <entry>Don't implicitly <literal>import Prelude</literal></entry>
             <entry>dynamic</entry>
             <entry><option>-XImplicitPrelude</option></entry>
           </row>
           <row>
-            <entry><option>-XRebindableSyntax</option></entry>
-            <entry>Employ <link linkend="rebindable-syntax">rebindable syntax</link></entry>
+            <entry><option>-XIncoherentInstances</option></entry>
+            <entry>Enable <link linkend="instance-overlap">incoherent instances</link>.
+              Implies <option>-XOverlappingInstances</option> </entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoRebindableSyntax</option></entry>
+            <entry><option>-XNoIncoherentInstances</option></entry>
           </row>
           <row>
             <entry><option>-XNoMonomorphismRestriction</option></entry>
@@ -784,16 +838,16 @@
             <entry><option>-XMonomorphismRrestriction</option></entry>
           </row>
           <row>
-            <entry><option>-XNoNPlusKPatterns</option></entry>
-            <entry>Disable support for <literal>n+k</literal> patterns</entry>
+            <entry><option>-XNegativeLiterals</option></entry>
+            <entry>Enable support for <link linkend="negative-literals">negative literals</link></entry>
             <entry>dynamic</entry>
-            <entry><option>-XNPlusKPatterns</option></entry>
+            <entry><option>-XNoNegativeLiterals</option></entry>
           </row>
           <row>
-            <entry><option>-XNegativeLiterals</option></entry>
-            <entry>Enable support for negative literals</entry>
+            <entry><option>-XNoNPlusKPatterns</option></entry>
+            <entry>Disable support for <literal>n+k</literal> patterns</entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoNegativeLiterals</option></entry>
+            <entry><option>-XNPlusKPatterns</option></entry>
           </row>
           <row>
             <entry><option>-XNumDecimals</option></entry>
@@ -802,22 +856,17 @@
             <entry><option>-XNoNumDecimals</option></entry>
           </row>
           <row>
-            <entry><option>-XNoTraditionalRecordSyntax</option></entry>
-            <entry>Disable support for traditional record syntax (as supported by Haskell 98) <literal>C {f = x}</literal></entry>
-            <entry>dynamic</entry>
-            <entry><option>-XTraditionalRecordSyntax</option></entry>
-          </row>
-          <row>
-            <entry><option>-XRelaxedPolyRec</option></entry>
-            <entry>Relaxed checking for <link linkend="typing-binds">mutually-recursive polymorphic functions</link></entry>
+            <entry><option>-XOverlappingInstances</option></entry>
+            <entry>Enable <link linkend="instance-overlap">overlapping instances</link></entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoRelaxedPolyRec</option></entry>
+            <entry><option>-XNoOverlappingInstances</option></entry>
           </row>
           <row>
-            <entry><option>-XExtendedDefaultRules</option></entry>
-            <entry>Use GHCi's <link linkend="extended-default-rules">extended default rules</link> in a normal module</entry>
+            <entry><option>-XOverloadedLists</option></entry>
+            <entry>Enable <link linkend="overloaded-lists">overloaded lists</link>.
+            </entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoExtendedDefaultRules</option></entry>
+            <entry><option>-XNoOverloadedLists</option></entry>
           </row>
           <row>
             <entry><option>-XOverloadedStrings</option></entry>
@@ -827,25 +876,22 @@
             <entry><option>-XNoOverloadedStrings</option></entry>
           </row>
           <row>
-            <entry><option>-XOverloadedLists</option></entry>
-            <entry>Enable <link linkend="overloaded-lists">overloaded lists</link>.
-            </entry>
+            <entry><option>-XQuasiQuotes</option></entry>
+            <entry>Enable <link linkend="th-quasiquotation">quasiquotation</link>.</entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoOverloadedLists</option></entry>
+            <entry><option>-XNoQuasiQuotes</option></entry>
           </row>
           <row>
-            <entry><option>-XGADTs</option></entry>
-            <entry>Enable <link linkend="gadt">generalised algebraic data types</link>.
-            </entry>
+            <entry><option>-XRelaxedPolyRec</option></entry>
+            <entry>Relaxed checking for <link linkend="typing-binds">mutually-recursive polymorphic functions</link></entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoGADTs</option></entry>
+            <entry><option>-XNoRelaxedPolyRec</option></entry>
           </row>
           <row>
-            <entry><option>-XGADTSyntax</option></entry>
-            <entry>Enable <link linkend="gadt-style">generalised algebraic data type syntax</link>.
-            </entry>
+            <entry><option>-XNoTraditionalRecordSyntax</option></entry>
+            <entry>Disable support for traditional record syntax (as supported by Haskell 98) <literal>C {f = x}</literal></entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoGADTSyntax</option></entry>
+            <entry><option>-XTraditionalRecordSyntax</option></entry>
           </row>
           <row>
             <entry><option>-XTypeFamilies</option></entry>
@@ -854,16 +900,10 @@
             <entry><option>-XNoTypeFamilies</option></entry>
           </row>
           <row>
-            <entry><option>-XConstraintKinds</option></entry>
-            <entry>Enable a <link linkend="constraint-kind">kind of constraints</link>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoConstraintKinds</option></entry>
-          </row>
-          <row>
-            <entry><option>-XDataKinds</option></entry>
-            <entry>Enable <link linkend="promotion">datatype promotion</link>.</entry>
+            <entry><option>-XUndecidableInstances</option></entry>
+            <entry>Enable <link linkend="undecidable-instances">undecidable instances</link></entry>
             <entry>dynamic</entry>
-            <entry><option>-XNoDataKinds</option></entry>
+            <entry><option>-XNoUndecidableInstances</option></entry>
           </row>
           <row>
             <entry><option>-XPolyKinds</option></entry>
@@ -873,13 +913,6 @@
             <entry><option>-XNoPolyKinds</option></entry>
           </row>
           <row>
-            <entry><option>-XScopedTypeVariables</option></entry>
-            <entry>Enable <link linkend="scoped-type-variables">lexically-scoped type variables</link>.
-              Implied by <option>-fglasgow-exts</option>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoScopedTypeVariables</option></entry>
-          </row>
-          <row>
             <entry><option>-XMonoLocalBinds</option></entry>
             <entry>Enable <link linkend="mono-local-binds">do not generalise local bindings</link>.
               Implied by <option>-XTypeFamilies</option> and <option>-XGADTs</option>.
@@ -888,6 +921,19 @@
             <entry><option>-XNoMonoLocalBinds</option></entry>
           </row>
           <row>
+            <entry><option>-XRebindableSyntax</option></entry>
+            <entry>Employ <link linkend="rebindable-syntax">rebindable syntax</link></entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoRebindableSyntax</option></entry>
+          </row>
+          <row>
+            <entry><option>-XScopedTypeVariables</option></entry>
+            <entry>Enable <link linkend="scoped-type-variables">lexically-scoped type variables</link>.
+              Implied by <option>-fglasgow-exts</option>.</entry>
+            <entry>dynamic</entry>
+            <entry><option>-XNoScopedTypeVariables</option></entry>
+          </row>
+          <row>
             <entry><option>-XTemplateHaskell</option></entry>
             <entry>Enable <link linkend="template-haskell">Template Haskell</link>.
               No longer implied by <option>-fglasgow-exts</option>.</entry>
@@ -895,12 +941,6 @@
             <entry><option>-XNoTemplateHaskell</option></entry>
           </row>
           <row>
-            <entry><option>-XQuasiQuotes</option></entry>
-            <entry>Enable <link linkend="th-quasiquotation">quasiquotation</link>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoQuasiQuotes</option></entry>
-          </row>
-          <row>
             <entry><option>-XBangPatterns</option></entry>
             <entry>Enable <link linkend="bang-patterns">bang patterns</link>.</entry>
             <entry>dynamic</entry>
@@ -1033,7 +1073,9 @@
           </row>
           <row>
             <entry><option>-XExplicitNamespaces</option></entry>
-            <entry>Enable using the keyword <literal>type</literal> to specify the namespace of entries in imports and exports.</entry>
+            <entry>Enable using the keyword <literal>type</literal> to specify the namespace of 
+                   entries in imports and exports (<xref linkend="explicit-namespaces"/>).
+                   Implied by <option>-XTypeOperators</option> and <option>-XTypeFamilies</option>.</entry>
             <entry>dynamic</entry>
             <entry><option>-XNoExplicitNamespaces</option></entry>
           </row>
@@ -1080,31 +1122,6 @@
             <entry><option>-XNoStandaloneDeriving</option></entry>
           </row>
           <row>
-            <entry><option>-XDeriveDataTypeable</option></entry>
-            <entry>Enable <link linkend="deriving-typeable">deriving for the Data and Typeable classes</link>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoDeriveDataTypeable</option></entry>
-          </row>
-          <row>
-            <entry><option>-XAutoDeriveTypeable</option></entry>
-            <entry>Automatically <link linkend="auto-derive-typeable">derive Typeable instances for every datatype and type class declaration</link>.
-            Implies <option>-XDeriveDataTypeable</option>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoAutoDeriveTypeable</option></entry>
-          </row>
-          <row>
-            <entry><option>-XDeriveGeneric</option></entry>
-            <entry>Enable <link linkend="deriving-typeable">deriving for the Generic class</link>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoDeriveGeneric</option></entry>
-          </row>
-          <row>
-            <entry><option>-XGeneralizedNewtypeDeriving</option></entry>
-            <entry>Enable <link linkend="newtype-deriving">newtype deriving</link>.</entry>
-            <entry>dynamic</entry>
-            <entry><option>-XNoGeneralizedNewtypeDeriving</option></entry>
-          </row>
-          <row>
             <entry><option>-XTypeSynonymInstances</option></entry>
             <entry>Enable <link linkend="flexible-instance-head">type synonyms in instance heads</link>.</entry>
             <entry>dynamic</entry>
@@ -1190,14 +1207,14 @@
             <entry><option>-</option></entry>
           </row>
           <row>
-            <entry><option>-fpackage-trust</option></entry>
-            <entry>Enable <link linkend="safe-haskell">Safe Haskell</link> trusted package requirement for trustworty modules.</entry>
+            <entry><option>-XTypeHoles</option></entry>
+            <entry>Enable <link linkend="type-holes">holes</link> in expressions.</entry>
             <entry>dynamic</entry>
-            <entry><option>-</option></entry>
+            <entry><option>--XNoTypeHoles</option></entry>
           </row>
           <row>
-            <entry><option>-XTypeHoles</option></entry>
-            <entry>Enable <link linkend="type-holes">holes</link> in expressions.</entry>
+            <entry><option>-fpackage-trust</option></entry>
+            <entry>Enable <link linkend="safe-haskell">Safe Haskell</link> trusted package requirement for trustworty modules.</entry>
             <entry>dynamic</entry>
             <entry><option>-</option></entry>
           </row>
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 46e4cbdb01..c825da90c7 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -2112,6 +2112,36 @@ import safe qualified Network.Socket as NS
 
 </sect2>
 
+<sect2 id="explicit-namespaces">
+<title>Explicit namespaces in import/export</title>
+
+<para> In an import or export list, such as 
+<programlisting>
+  module M( f, (++) ) where ...
+    import N( f, (++) ) 
+    ...
+</programlisting>
+the entities <literal>f</literal> and <literal>(++)</literal> are <emphasis>values</emphasis>.
+However, with type operators (<xref linkend="type-operators"/>) it becomes possible
+to declare <literal>(++)</literal> as a <emphasis>type constructor</emphasis>.  In that
+case, how would you export or import it?
+</para>
+<para>
+The <option>-XExplicitNamespaces</option> extension allows you to prefix the name of 
+a type constructor in an import or export list with "<literal>type</literal>" to 
+disambiguate this case, thus:
+<programlisting>
+  module M( f, type (++) ) where ...
+    import N( f, type (++) ) 
+    ...
+  module N( f, type (++) ) where
+    data family a ++ b = L a | R b
+</programlisting>
+The extension <option>-XExplicitNamespaces</option>
+is implied by <option>-XTypeOperators</option> and (for some reason) by <option>-XTypeFamilies</option>.
+</para>
+</sect2>
+
 <sect2 id="syntax-stolen">
 <title>Summary of stolen syntax</title>
 
@@ -2385,11 +2415,13 @@ There is now some potential ambiguity in import and export lists; for example
 if you write <literal>import M( (+) )</literal> do you mean the 
 <emphasis>function</emphasis> <literal>(+)</literal> or the 
 <emphasis>type constructor</emphasis> <literal>(+)</literal>?
-The default is the former, but GHC allows you to specify the latter
+The default is the former, but with <option>-XExplicitNamespaces</option> (which is implied
+by <option>-XExplicitTypeOperators</option>) GHC allows you to specify the latter
 by preceding it with the keyword <literal>type</literal>, thus:
 <programlisting>
 import M( type (+) )
 </programlisting>
+See <xref linkend="explicit-namespaces"/>.
 </para></listitem>
 <listitem><para>
 The fixity of a type operator may be set using the usual fixity declarations
@@ -4642,30 +4674,44 @@ The willingness to be overlapped or incoherent is a property of
 the <emphasis>instance declaration</emphasis> itself, controlled by the
 presence or otherwise of the <option>-XOverlappingInstances</option>
 and <option>-XIncoherentInstances</option> flags when that module is
-being defined.  Specifically, during the lookup process:
+being defined.  Suppose we are searching for an instance of the 
+<emphasis>target constraint</emphasis> <literal>(C ty1 .. tyn)</literal>.
+The search works like this.
 <itemizedlist>
 <listitem><para>
-If the constraint being looked up matches two instance declarations IA and IB,
-and
-<itemizedlist>
-<listitem><para>IB is a substitution instance of IA (but not vice versa);
-that is, IB is strictly more specific than IA</para></listitem>
-<listitem><para>either IA or IB was compiled with <option>-XOverlappingInstances</option></para></listitem>
-</itemizedlist>
-then the less-specific instance IA is ignored.
+Find all instances I that <emphasis>match</emphasis> the target constraint;
+that is, the target constraint is a substitution instance of I.  These
+instance declarations are the <emphasis>candidates</emphasis>.
 </para></listitem>
+
+<listitem><para>
+Find all <emphasis>non-candidate</emphasis> instances 
+that <emphasis>unify</emphasis> with the target constraint.
+Such non-candidates instances might match when the target constraint is further
+instantiated.  If all of them were compiled with
+<option>-XIncoherentInstances</option>, proceed; if not, the search fails.
+</para></listitem>
+
 <listitem><para>
-Suppose an instance declaration does not match the constraint being looked up, but
-does <emphasis>unify</emphasis> with it, so that it might match when the constraint is further
-instantiated.  Usually GHC will regard this as a reason for not committing to
-some other constraint.  But if the instance declaration was compiled with
-<option>-XIncoherentInstances</option>, GHC will skip the "does-it-unify?"
-check for that declaration.
+Eliminate any candidate IX for which both of the following hold:
+
+<itemizedlist>
+<listitem><para>There is another candidate IY that is strictly more specific;
+that is, IY is a substitution instance of IX but not vice versa.
+</para></listitem>
+<listitem><para>Either IX or IY was compiled with 
+<option>-XOverlappingInstances</option>.
 </para></listitem>
+</itemizedlist>
+
+</para></listitem>
+
 <listitem><para>
-If two instance declarations are matched and either is compiled with
-<option>-XIncoherentInstances</option>, then that declaration is ignored.
+If only one candidate remains, pick it.
+Otherwise if all remaining candidates were compiled with
+<option>-XInccoherentInstances</option>, pick an arbitrary candidate.
 </para></listitem>
+
 </itemizedlist>
 These rules make it possible for a library author to design a library that relies on
 overlapping instances without the library client having to know.
@@ -6386,106 +6432,91 @@ The flag <option>-XFlexibleContexts</option> also lifts the corresponding
 restriction on class declarations (<xref linkend="superclass-rules"/>) and instance declarations
 (<xref linkend="instance-rules"/>).
 </para>
+</sect2>
 
-<para>
-GHC imposes the following restrictions on the constraints in a type signature.
-Consider the type:
+<sect2 id="ambiguity"><title>Ambiguous types and the ambiguity check</title>
 
+<para>
+Each user-written type signature is subjected to an
+<emphasis>ambiguity check</emphasis>.  
+The ambiguity check rejects functions that can never be called; for example:
 <programlisting>
-  forall tv1..tvn (c1, ...,cn) => type
+   f :: C a => Int
 </programlisting>
-
-(Here, we write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 98, all the free type variables of an
-explicit source-language type signature are universally quantified,
-except for the class type variables in a class declaration.  However,
-in GHC, you can give the foralls if you want.  See <xref linkend="explicit-foralls"/>).
+The idea is there can be no legal calls to <literal>f</literal> because every call will
+give rise to an ambiguous constraint.  
 </para>
-
 <para>
-
-<orderedlist>
-<listitem>
-
+The <emphasis>only</emphasis> purpose of the
+ambiguity check is to report functions that cannot possibly be called.
+We could soundly omit the
+ambiguity check on type signatures entirely, at the expense of
+delaying ambiguity errors to call sites.  Indeed, the language extension
+<option>-XAllowAmbiguousTypes</option> switches off the ambiguity check.
+</para>
 <para>
- <emphasis>Each universally quantified type variable
-<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
-
-A type variable <literal>a</literal> is "reachable" if it appears
-in the same constraint as either a type variable free in
-<literal>type</literal>, or another reachable type variable.
-A value with a type that does not obey
-this reachability restriction cannot be used without introducing
-ambiguity; that is why the type is rejected.
-Here, for example, is an illegal type:
-
-
+Ambiguity can be subtle.  Consider this example which uses functional dependencies:
 <programlisting>
-  forall a. Eq a => Int
+   class D a b | a -> b where ..
+   h :: D Int b => Int 
 </programlisting>
-
-
-When a value with this type was used, the constraint <literal>Eq tv</literal>
-would be introduced where <literal>tv</literal> is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
-can never know which instance of <literal>Eq</literal> to use because we never
-get any more information about <literal>tv</literal>.
-</para>
-<para>
-Note
-that the reachability condition is weaker than saying that <literal>a</literal> is
-functionally dependent on a type variable free in
-<literal>type</literal> (see <xref
-linkend="functional-dependencies"/>).  The reason for this is there
-might be a "hidden" dependency, in a superclass perhaps.  So
-"reachable" is a conservative approximation to "functionally dependent".
-For example, consider:
+The <literal>Int</literal> may well fix <literal>b</literal> at the call site, so that signature should
+not be rejected.  Moreover, the dependencies might be hidden. Consider
+<programlisting>
+   class X a b where ...
+   class D a b | a -> b where ...
+   instance D a b => X [a] b where...
+   h :: X a b => a -> a
+</programlisting>
+Here <literal>h</literal>'s type looks ambiguous in <literal>b</literal>, but here's a legal call:
 <programlisting>
-  class C a b | a -> b where ...
-  class C a b => D a b where ...
-  f :: forall a b. D a b => a -> a
+   ...(h [True])...
 </programlisting>
-This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
-but that is not immediately apparent from <literal>f</literal>'s type.
+That gives rise to a <literal>(X [Bool] beta)</literal> constraint, and using the
+instance means we need <literal>(D Bool beta)</literal> and that 
+fixes <literal>beta</literal> via <literal>D</literal>'s
+fundep!
 </para>
-</listitem>
-<listitem>
-
 <para>
- <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
-universally quantified type variables <literal>tvi</literal></emphasis>.
-
-For example, this type is OK because <literal>C a b</literal> mentions the
-universally quantified type variable <literal>b</literal>:
-
-
+Behind all these special cases there is a simple guiding principle. 
+Consider
 <programlisting>
-  forall a. C a b => burble
-</programlisting>
+  f :: <replaceable>type</replaceable>
+  f = ...blah...
 
-
-The next type is illegal because the constraint <literal>Eq b</literal> does not
-mention <literal>a</literal>:
-
-
-<programlisting>
-  forall a. Eq b => burble
+  g :: <replaceable>type</replaceable>
+  g = f
 </programlisting>
-
-
-The reason for this restriction is milder than the other one.  The
-excluded types are never useful or necessary (because the offending
-context doesn't need to be witnessed at this point; it can be floated
-out).  Furthermore, floating them out increases sharing. Lastly,
-excluding them is a conservative choice; it leaves a patch of
-territory free in case we need it later.
-
+You would think that the definition of <literal>g</literal> would surely typecheck!
+After all <literal>f</literal> has exactly the same type, and <literal>g=f</literal>. 
+But in fact <literal>f</literal>'s type
+is instantiated and the instantiated constraints are solved against
+the constraints bound by <literal>g</literal>'s signature.  So, in the case an ambiguous type, solving will fail.
+For example, consider the earlier definition <literal>f :: C a => Int</literal>.  Then in <literal>g</literal>'s definition,
+we'll instantiate to <literal>(C alpha)</literal> and try to 
+deduce <literal>(C alpha)</literal> from <literal>(C a)</literal>,
+and fail.  
+</para>
+<para>
+So in fact we use this as our <emphasis>definition</emphasis> of ambiguity: a type 
+<literal><replaceable>ty</replaceable></literal> is
+ambiguious if and only if <literal>((undefined :: <replaceable>ty</replaceable>) 
+:: <replaceable>ty</replaceable>)</literal> would fail to typecheck.  We use a
+very similar test for <emphasis>inferred</emphasis> types, to ensure that they too are
+unambiguous. 
 </para>
-</listitem>
-
-</orderedlist>
 
+<para>
+<emphasis>A historical note.</emphasis>
+GHC used to impose some more restrictive and less principled conditions
+on type signatures. For type type
+<literal>forall tv1..tvn (c1, ...,cn) => type</literal>
+GHC used to require (a) that each universally quantified type variable
+<literal>tvi</literal> must be "reachable" from <literal>type</literal>, 
+and (b) that every constraint <literal>ci</literal> mentions at least one of the
+universally quantified type variables <literal>tvi</literal>.
+These ad-hoc restrictions are completely subsumed by the new ambiguity check.
+<emphasis>End of historical note.</emphasis>
 </para>
 
 </sect2>
@@ -6498,9 +6529,7 @@ territory free in case we need it later.
 J Lewis, MB Shields, E Meijer, J Launchbury,
 27th ACM Symposium on Principles of Programming Languages (POPL'00),
 Boston, Jan 2000.
-</para>
-
-<para>(Most of the following, still rather incomplete, documentation is
+(Most of the following, still rather incomplete, documentation is
 due to Jeff Lewis.)</para>
 
 <para>Implicit parameter support is enabled with the option
@@ -7612,8 +7641,9 @@ Failed, modules loaded: none.
 This ensures that an unbound identifier is never reported with a too polymorphic type, like
 <literal>forall a. a</literal>, when used multiple times for types that can not be unified.
 </para>
-
 </sect2>
+
+
 </sect1>
 <!-- ==================== End of type system extensions =================  -->