Improve documentation of instances

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 4e50b5c..1b7bb64 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1183,7 +1183,11 @@ checkValidInstance tyvars theta clas inst_tys
                         undecidableMsg])
 \end{code}
 
                         undecidableMsg])
 \end{code}
 

-Termination test: each assertion in the context satisfies
+Termination test: the so-called "Paterson conditions" (see Section 5 of
+"Understanding functionsl dependencies via Constraint Handling Rules, 
+JFP Jan 2007).
+
+We check that each assertion in the context satisfies:

  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.

diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 4475af4..d9a6198 100644 (file)
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -2546,7 +2546,7 @@ the context and head of the instance declaration can each consist of arbitrary
 following rules:
 <orderedlist>
 <listitem><para>
 following rules:
 <orderedlist>
 <listitem><para>

-For each assertion in the context:
+The Paterson Conditions: for each assertion in the context

 <orderedlist>
 <listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
 <listitem><para>The assertion has fewer constructors and variables (taken together
 <orderedlist>
 <listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
 <listitem><para>The assertion has fewer constructors and variables (taken together

@@ -2554,7 +2554,7 @@ For each assertion in the context:
 </orderedlist>
 </para></listitem>
 
 </orderedlist>
 </para></listitem>
 

-<listitem><para>The coverage condition.  For each functional dependency,
+<listitem><para>The Coverage Condition.  For each functional dependency,

 <replaceable>tvs</replaceable><subscript>left</subscript> <literal>-&gt;</literal>
 <replaceable>tvs</replaceable><subscript>right</subscript>,  of the class,
 every type variable in
 <replaceable>tvs</replaceable><subscript>left</subscript> <literal>-&gt;</literal>
 <replaceable>tvs</replaceable><subscript>right</subscript>,  of the class,
 every type variable in

@@ -2566,11 +2566,15 @@ corresponding type in the instance declaration.
 </orderedlist>
 These restrictions ensure that context reduction terminates: each reduction
 step makes the problem smaller by at least one
 </orderedlist>
 These restrictions ensure that context reduction terminates: each reduction
 step makes the problem smaller by at least one

-constructor.  For example, the following would make the type checker
-loop if it wasn't excluded:
-<programlisting>
-  instance C a => C a where ...
-</programlisting>
+constructor.  Both the Paterson Conditions and the Coverage Condition are lifted 
+if you give the <option>-fallow-undecidable-instances</option> 
+flag (<xref linkend="undecidable-instances"/>).
+You can find lots of background material about the reason for these
+restrictions in the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
+Understanding functional dependencies via Constraint Handling Rules</ulink>.
+</para>
+<para>

 For example, these are OK:
 <programlisting>
   instance C Int [a]          -- Multiple parameters
 For example, these are OK:
 <programlisting>
   instance C Int [a]          -- Multiple parameters

@@ -2622,11 +2626,6 @@ something more specific does not:
     op = ... -- Default
 </programlisting>
 </para>
     op = ... -- Default
 </programlisting>
 </para>

-<para>You can find lots of background material about the reason for these
-restrictions in the paper <ulink
-url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
-Understanding functional dependencies via Constraint Handling Rules</ulink>.
-</para>

 </sect3>
 
 <sect3 id="undecidable-instances">
 </sect3>
 
 <sect3 id="undecidable-instances">

@@ -2691,8 +2690,8 @@ makes instance inference go into a loop, because it requires the constraint
 Nevertheless, GHC allows you to experiment with more liberal rules.  If you use
 the experimental flag <option>-fallow-undecidable-instances</option>
 <indexterm><primary>-fallow-undecidable-instances
 Nevertheless, GHC allows you to experiment with more liberal rules.  If you use
 the experimental flag <option>-fallow-undecidable-instances</option>
 <indexterm><primary>-fallow-undecidable-instances

-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head.  Termination is ensured by having a
+option</primary></indexterm>, both the Paterson Conditions and the Coverage Condition
+(described in <xref linkend="instance-rules"/>) are lifted.  Termination is ensured by having a

 fixed-depth recursion stack.  If you exceed the stack depth you get a
 sort of backtrace, and the opportunity to increase the stack depth
 with <option>-fcontext-stack=</option><emphasis>N</emphasis>.
 fixed-depth recursion stack.  If you exceed the stack depth you get a
 sort of backtrace, and the opportunity to increase the stack depth
 with <option>-fcontext-stack=</option><emphasis>N</emphasis>.