</title>
<para> The recursive do-notation (also known as mdo-notation) is implemented as described in
-"A recursive do for Haskell",
-Levent Erkok, John Launchbury",
+<ulink url="http://citeseer.ist.psu.edu/erk02recursive.html">A recursive do for Haskell</ulink>,
+by Levent Erkok, John Launchbury,
Haskell Workshop 2002, pages: 29-37. Pittsburgh, Pennsylvania.
+This paper is essential reading for anyone making non-trivial use of mdo-notation,
+and we do not repeat it here.
</para>
<para>
The do-notation of Haskell does not allow <emphasis>recursive bindings</emphasis>,
</programlisting>
<para>
The function <literal>mfix</literal>
-dictates how the required recursion operation should be performed. If recursive bindings are required for a monad,
-then that monad must be declared an instance of the <literal>MonadFix</literal> class.
-For details, see the above mentioned reference.
+dictates how the required recursion operation should be performed. For example,
+<literal>justOnes</literal> desugars as follows:
+<programlisting>
+justOnes = mfix (\xs' -> do { xs <- Just (1:xs'); return xs }
+</programlisting>
+For full details of the way in which mdo is typechecked and desugared, see
+the paper <ulink url="http://citeseer.ist.psu.edu/erk02recursive.html">A recursive do for Haskell</ulink>.
+In particular, GHC implements the segmentation technique described in Section 3.2 of the paper.
</para>
<para>
+If recursive bindings are required for a monad,
+then that monad must be declared an instance of the <literal>MonadFix</literal> class.
The following instances of <literal>MonadFix</literal> are automatically provided: List, Maybe, IO.
Furthermore, the Control.Monad.ST and Control.Monad.ST.Lazy modules provide the instances of the MonadFix class
for Haskell's internal state monad (strict and lazy, respectively).
GHC does not commit to instance (C), because in a particular
call of <literal>f</literal>, <literal>b</literal> might be instantiate
to <literal>Int</literal>, in which case instance (D) would be more specific still.
-So GHC rejects the program. If you add the flag <option>-XIncoherentInstances</option>,
+So GHC rejects the program.
+(If you add the flag <option>-XIncoherentInstances</option>,
GHC will instead pick (C), without complaining about
-the problem of subsequent instantiations.
+the problem of subsequent instantiations.)
+</para>
+<para>
+Notice that we gave a type signature to <literal>f</literal>, so GHC had to
+<emphasis>check</emphasis> that <literal>f</literal> has the specified type.
+Suppose instead we do not give a type signature, asking GHC to <emphasis>infer</emphasis>
+it instead. In this case, GHC will refrain from
+simplifying the constraint <literal>C Int [Int]</literal> (for the same reason
+as before) but, rather than rejecting the program, it will infer the type
+<programlisting>
+ f :: C Int b => [b] -> [b]
+</programlisting>
+That postpones the question of which instance to pick to the
+call site for <literal>f</literal>
+by which time more is known about the type <literal>b</literal>.
</para>
<para>
The willingness to be overlapped or incoherent is a property of