[project @ 2002-11-28 01:00:44 by mthomas]
[ghc-hetmet.git] / ghc / docs / users_guide / glasgow_exts.sgml
index 3669baa..4d1ee17 100644 (file)
@@ -16,160 +16,15 @@ performance because of the implementation costs of Haskell's
 </para>
 
 <para>
 </para>
 
 <para>
-Executive summary of our extensions:
-</para>
-
-  <variablelist>
-
-    <varlistentry>
-      <term>Unboxed types and primitive operations:</Term>
-      <listitem>
-       <para>You can get right down to the raw machine types and
-        operations; included in this are &ldquo;primitive
-        arrays&rdquo; (direct access to Big Wads of Bytes).  Please
-        see <XRef LinkEnd="glasgow-unboxed"> and following.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Type system extensions:</term>
-      <listitem>
-       <para> GHC supports a large number of extensions to Haskell's
-        type system.  Specifically:</para>
-
-       <variablelist>
-         <varlistentry>
-           <term>Multi-parameter type classes:</term>
-           <listitem>
-             <para><xref LinkEnd="multi-param-type-classes"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Functional dependencies:</term>
-           <listitem>
-             <para><xref LinkEnd="functional-dependencies"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Implicit parameters:</term>
-           <listitem>
-             <para><xref LinkEnd="implicit-parameters"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Linear implicit parameters:</term>
-           <listitem>
-             <para><xref LinkEnd="linear-implicit-parameters"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Local universal quantification:</term>
-           <listitem>
-             <para><xref LinkEnd="universal-quantification"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Extistentially quantification in data types:</term>
-           <listitem>
-             <para><xref LinkEnd="existential-quantification"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Scoped type variables:</term>
-           <listitem>
-             <para>Scoped type variables enable the programmer to
-              supply type signatures for some nested declarations,
-              where this would not be legal in Haskell 98.  Details in
-              <xref LinkEnd="scoped-type-variables">.</para>
-           </listitem>
-         </varlistentry>
-       </variablelist>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Pattern guards</term>
-      <listitem>
-       <para>Instead of being a boolean expression, a guard is a list
-       of qualifiers, exactly as in a list comprehension. See <xref
-       LinkEnd="pattern-guards">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Data types with no constructors</term>
-      <listitem>
-       <para>See <xref LinkEnd="nullary-types">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Parallel list comprehensions</term>
-      <listitem>
-       <para>An extension to the list comprehension syntax to support
-       <literal>zipWith</literal>-like functionality.  See <xref
-       linkend="parallel-list-comprehensions">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Foreign calling:</term>
-      <listitem>
-       <para>Just what it sounds like.  We provide
-        <emphasis>lots</emphasis> of rope that you can dangle around
-        your neck.  Please see <xref LinkEnd="ffi">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Pragmas</term>
-      <listitem>
-       <para>Pragmas are special instructions to the compiler placed
-        in the source file.  The pragmas GHC supports are described in
-        <xref LinkEnd="pragmas">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Rewrite rules:</term>
-      <listitem>
-       <para>The programmer can specify rewrite rules as part of the
-        source program (in a pragma).  GHC applies these rewrite rules
-        wherever it can.  Details in <xref
-        LinkEnd="rewrite-rules">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Generic classes:</term>
-      <listitem>
-       <para>(Note: support for generic classes is currently broken
-        in GHC 5.02).</para>
-
-       <para>Generic class declarations allow you to define a class
-        whose methods say how to work over an arbitrary data type.
-        Then it's really easy to make any new type into an instance of
-        the class.  This generalises the rather ad-hoc "deriving"
-        feature of Haskell 98.  Details in <xref
-        LinkEnd="generic-classes">.</para>
-      </listitem>
-    </varlistentry>
-  </variablelist>
-
-<para>
 Before you get too carried away working at the lowest level (e.g.,
 sloshing <literal>MutableByteArray&num;</literal>s around your
 program), you may wish to check if there are libraries that provide a
 Before you get too carried away working at the lowest level (e.g.,
 sloshing <literal>MutableByteArray&num;</literal>s around your
 program), you may wish to check if there are libraries that provide a
-&ldquo;Haskellised veneer&rdquo; over the features you want.  See
-<xref linkend="book-hslibs">.
+&ldquo;Haskellised veneer&rdquo; over the features you want.  The
+separate libraries documentation describes all the libraries that come
+with GHC.
 </para>
 
 </para>
 
+<!-- LANGUAGE OPTIONS -->
   <sect1 id="options-language">
     <title>Language options</title>
 
   <sect1 id="options-language">
     <title>Language options</title>
 
@@ -198,6 +53,30 @@ program), you may wish to check if there are libraries that provide a
       </varlistentry>
 
       <varlistentry>
       </varlistentry>
 
       <varlistentry>
+       <term><option>-ffi</option> and <option>-fffi</option>:</term>
+       <indexterm><primary><option>-ffi</option></primary></indexterm>
+       <indexterm><primary><option>-fffi</option></primary></indexterm>
+       <listitem>
+         <para>This option enables the language extension defined in the
+         Haskell 98 Foreign Function Interface Addendum plus deprecated
+         syntax of previous versions of the FFI for backwards
+         compatibility.</para> 
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term><option>-fwith</option>:</term>
+       <indexterm><primary><option>-fwith</option></primary></indexterm>
+       <listitem>
+         <para>This option enables the deprecated <literal>with</literal>
+         keyword for implicit parameters; it is merely provided for backwards
+         compatibility.
+          It is independent of the <option>-fglasgow-exts</option>
+          flag. </para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
        <term><option>-fno-monomorphism-restriction</option>:</term>
        <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
        <listitem>
        <term><option>-fno-monomorphism-restriction</option>:</term>
        <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
        <listitem>
@@ -210,6 +89,7 @@ program), you may wish to check if there are libraries that provide a
       <varlistentry>
        <term><option>-fallow-overlapping-instances</option></term>
        <term><option>-fallow-undecidable-instances</option></term>
       <varlistentry>
        <term><option>-fallow-overlapping-instances</option></term>
        <term><option>-fallow-undecidable-instances</option></term>
+       <term><option>-fallow-incoherent-instances</option></term>
        <term><option>-fcontext-stack</option></term>
        <indexterm><primary><option>-fallow-overlapping-instances</option></primary></indexterm>
        <indexterm><primary><option>-fallow-undecidable-instances</option></primary></indexterm>
        <term><option>-fcontext-stack</option></term>
        <indexterm><primary><option>-fallow-overlapping-instances</option></primary></indexterm>
        <indexterm><primary><option>-fallow-undecidable-instances</option></primary></indexterm>
@@ -251,7 +131,7 @@ program), you may wish to check if there are libraries that provide a
             module namespace is flat, and you must not conflict with
             any Prelude module.)</para>
 
             module namespace is flat, and you must not conflict with
             any Prelude module.)</para>
 
-           <para>Even though you have not imported the Prelude, all
+           <para>Even though you have not imported the Prelude, most of
             the built-in syntax still refers to the built-in Haskell
             Prelude types and values, as specified by the Haskell
             Report.  For example, the type <literal>[Int]</literal>
             the built-in syntax still refers to the built-in Haskell
             Prelude types and values, as specified by the Haskell
             Report.  For example, the type <literal>[Int]</literal>
@@ -260,51 +140,9 @@ program), you may wish to check if there are libraries that provide a
             translation for list comprehensions continues to use
             <literal>Prelude.map</literal> etc.</para>
 
             translation for list comprehensions continues to use
             <literal>Prelude.map</literal> etc.</para>
 
-           <para> With one group of exceptions!  You may want to
-            define your own numeric class hierarchy.  It completely
-            defeats that purpose if the literal "1" means
-            "<literal>Prelude.fromInteger 1</literal>", which is what
-            the Haskell Report specifies.  So the
-            <option>-fno-implicit-prelude</option> flag causes the
-            following pieces of built-in syntax to refer to <emphasis>whatever
-            is in scope</emphasis>, not the Prelude versions:</para>
-
-           <itemizedlist>
-             <listitem>
-               <para>Integer and fractional literals mean
-                "<literal>fromInteger 1</literal>" and
-                "<literal>fromRational 3.2</literal>", not the
-                Prelude-qualified versions; both in expressions and in
-                patterns.</para>
-             </listitem>
-
-             <listitem>
-               <para>Negation (e.g. "<literal>- (f x)</literal>")
-               means "<literal>negate (f x)</literal>" (not
-               <literal>Prelude.negate</literal>).</para>
-             </listitem>
-
-             <listitem>
-               <para>In an n+k pattern, the standard Prelude
-                <literal>Ord</literal> class is still used for comparison,
-                but the necessary subtraction uses whatever
-                "<literal>(-)</literal>" is in scope (not
-                "<literal>Prelude.(-)</literal>").</para>
-             </listitem>
-           </itemizedlist>
-
-            <para>Note: Negative literals, such as <literal>-3</literal>, are
-             specified by (a careful reading of) the Haskell Report as 
-             meaning <literal>Prelude.negate (Prelude.fromInteger 3)</literal>.
-             However, GHC deviates from this slightly, and treats them as meaning
-             <literal>fromInteger (-3)</literal>.  One particular effect of this
-             slightly-non-standard reading is that there is no difficulty with
-             the literal <literal>-2147483648</literal> at type <literal>Int</literal>;
-             it means <literal>fromInteger (-2147483648)</literal>.  The strict interpretation
-             would be <literal>negate (fromInteger 2147483648)</literal>,
-             and the call to <literal>fromInteger</literal> would overflow
-             (at type <literal>Int</literal>, remember).
-             </para>
+           <para>However, <option>-fno-implicit-prelude</option> does
+           change the handling of certain built-in syntax: see
+           <xref LinkEnd="rebindable-syntax">.</para>
 
          </listitem>
        </varlistentry>
 
          </listitem>
        </varlistentry>
@@ -313,144 +151,279 @@ program), you may wish to check if there are libraries that provide a
   </sect1>
 
 <!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
   </sect1>
 
 <!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
-&primitives;
+<!--    included from primitives.sgml  -->
+<!-- &primitives; -->
+<sect1 id="primitives">
+  <title>Unboxed types and primitive operations</title>
+
+<para>GHC is built on a raft of primitive data types and operations.
+While you really can use this stuff to write fast code,
+  we generally find it a lot less painful, and more satisfying in the
+  long run, to use higher-level language features and libraries.  With
+  any luck, the code you write will be optimised to the efficient
+  unboxed version in any case.  And if it isn't, we'd like to know
+  about it.</para>
+
+<para>We do not currently have good, up-to-date documentation about the
+primitives, perhaps because they are mainly intended for internal use.
+There used to be a long section about them here in the User Guide, but it
+became out of date, and wrong information is worse than none.</para>
+
+<para>The Real Truth about what primitive types there are, and what operations
+work over those types, is held in the file
+<filename>fptools/ghc/compiler/prelude/primops.txt</filename>.
+This file is used directly to generate GHC's primitive-operation definitions, so
+it is always correct!  It is also intended for processing into text.</para>
+
+<para> Indeed,
+the result of such processing is part of the description of the 
+ <ulink
+      url="http://haskell.cs.yale.edu/ghc/docs/papers/core.ps.gz">External
+        Core language</ulink>.
+So that document is a good place to look for a type-set version.
+We would be very happy if someone wanted to volunteer to produce an SGML
+back end to the program that processes <filename>primops.txt</filename> so that
+we could include the results here in the User Guide.</para>
+
+<para>What follows here is a brief summary of some main points.</para>
+  
+<sect2 id="glasgow-unboxed">
+<title>Unboxed types
+</title>
 
 
-<sect1 id="glasgow-ST-monad">
-<title>Primitive state-transformer monad</title>
+<para>
+<indexterm><primary>Unboxed types (Glasgow extension)</primary></indexterm>
+</para>
+
+<para>Most types in GHC are <firstterm>boxed</firstterm>, which means
+that values of that type are represented by a pointer to a heap
+object.  The representation of a Haskell <literal>Int</literal>, for
+example, is a two-word heap object.  An <firstterm>unboxed</firstterm>
+type, however, is represented by the value itself, no pointers or heap
+allocation are involved.
+</para>
 
 <para>
 
 <para>
-<indexterm><primary>state transformers (Glasgow extensions)</primary></indexterm>
-<indexterm><primary>ST monad (Glasgow extension)</primary></indexterm>
+Unboxed types correspond to the &ldquo;raw machine&rdquo; types you
+would use in C: <literal>Int&num;</literal> (long int),
+<literal>Double&num;</literal> (double), <literal>Addr&num;</literal>
+(void *), etc.  The <emphasis>primitive operations</emphasis>
+(PrimOps) on these types are what you might expect; e.g.,
+<literal>(+&num;)</literal> is addition on
+<literal>Int&num;</literal>s, and is the machine-addition that we all
+know and love&mdash;usually one instruction.
 </para>
 
 <para>
 </para>
 
 <para>
-This monad underlies our implementation of arrays, mutable and
-immutable, and our implementation of I/O, including &ldquo;C calls&rdquo;.
+Primitive (unboxed) types cannot be defined in Haskell, and are
+therefore built into the language and compiler.  Primitive types are
+always unlifted; that is, a value of a primitive type cannot be
+bottom.  We use the convention that primitive types, values, and
+operations have a <literal>&num;</literal> suffix.
 </para>
 
 <para>
 </para>
 
 <para>
-The <literal>ST</literal> library, which provides access to the
-<function>ST</function> monad, is described in <xref
-linkend="sec-ST">.
+Primitive values are often represented by a simple bit-pattern, such
+as <literal>Int&num;</literal>, <literal>Float&num;</literal>,
+<literal>Double&num;</literal>.  But this is not necessarily the case:
+a primitive value might be represented by a pointer to a
+heap-allocated object.  Examples include
+<literal>Array&num;</literal>, the type of primitive arrays.  A
+primitive array is heap-allocated because it is too big a value to fit
+in a register, and would be too expensive to copy around; in a sense,
+it is accidental that it is represented by a pointer.  If a pointer
+represents a primitive value, then it really does point to that value:
+no unevaluated thunks, no indirections&hellip;nothing can be at the
+other end of the pointer than the primitive value.
 </para>
 
 </para>
 
-</sect1>
+<para>
+There are some restrictions on the use of primitive types, the main
+one being that you can't pass a primitive value to a polymorphic
+function or store one in a polymorphic data type.  This rules out
+things like <literal>[Int&num;]</literal> (i.e. lists of primitive
+integers).  The reason for this restriction is that polymorphic
+arguments and constructor fields are assumed to be pointers: if an
+unboxed integer is stored in one of these, the garbage collector would
+attempt to follow it, leading to unpredictable space leaks.  Or a
+<function>seq</function> operation on the polymorphic component may
+attempt to dereference the pointer, with disastrous results.  Even
+worse, the unboxed value might be larger than a pointer
+(<literal>Double&num;</literal> for instance).
+</para>
 
 
-<sect1 id="glasgow-prim-arrays">
-<title>Primitive arrays, mutable and otherwise
+<para>
+Nevertheless, A numerically-intensive program using unboxed types can
+go a <emphasis>lot</emphasis> faster than its &ldquo;standard&rdquo;
+counterpart&mdash;we saw a threefold speedup on one example.
+</para>
+
+</sect2>
+
+<sect2 id="unboxed-tuples">
+<title>Unboxed Tuples
 </title>
 
 <para>
 </title>
 
 <para>
-<indexterm><primary>primitive arrays (Glasgow extension)</primary></indexterm>
-<indexterm><primary>arrays, primitive (Glasgow extension)</primary></indexterm>
+Unboxed tuples aren't really exported by <literal>GHC.Exts</literal>,
+they're available by default with <option>-fglasgow-exts</option>.  An
+unboxed tuple looks like this:
 </para>
 
 <para>
 </para>
 
 <para>
-GHC knows about quite a few flavours of Large Swathes of Bytes.
+
+<programlisting>
+(# e_1, ..., e_n #)
+</programlisting>
+
 </para>
 
 <para>
 </para>
 
 <para>
-First, GHC distinguishes between primitive arrays of (boxed) Haskell
-objects (type <literal>Array&num; obj</literal>) and primitive arrays of bytes (type
-<literal>ByteArray&num;</literal>).
+where <literal>e&lowbar;1..e&lowbar;n</literal> are expressions of any
+type (primitive or non-primitive).  The type of an unboxed tuple looks
+the same.
 </para>
 
 <para>
 </para>
 
 <para>
-Second, it distinguishes between&hellip;
-<variablelist>
+Unboxed tuples are used for functions that need to return multiple
+values, but they avoid the heap allocation normally associated with
+using fully-fledged tuples.  When an unboxed tuple is returned, the
+components are put directly into registers or on the stack; the
+unboxed tuple itself does not have a composite representation.  Many
+of the primitive operations listed in this section return unboxed
+tuples.
+</para>
 
 
-<varlistentry>
-<term>Immutable:</term>
-<listitem>
 <para>
 <para>
-Arrays that do not change (as with &ldquo;standard&rdquo; Haskell arrays); you
-can only read from them.  Obviously, they do not need the care and
-attention of the state-transformer monad.
+There are some pretty stringent restrictions on the use of unboxed tuples:
 </para>
 </para>
-</listitem>
-</varlistentry>
-<varlistentry>
-<term>Mutable:</term>
+
+<para>
+
+<itemizedlist>
 <listitem>
 <listitem>
+
 <para>
 <para>
-Arrays that may be changed or &ldquo;mutated.&rdquo;  All the operations on them
-live within the state-transformer monad and the updates happen
-<emphasis>in-place</emphasis>.
+ Unboxed tuple types are subject to the same restrictions as
+other unboxed types; i.e. they may not be stored in polymorphic data
+structures or passed to polymorphic functions.
+
 </para>
 </listitem>
 </para>
 </listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Static&rdquo; (in C land):</term>
 <listitem>
 <listitem>
+
 <para>
 <para>
-A C routine may pass an <literal>Addr&num;</literal> pointer back into Haskell land.  There
-are then primitive operations with which you may merrily grab values
-over in C land, by indexing off the &ldquo;static&rdquo; pointer.
+ Unboxed tuples may only be constructed as the direct result of
+a function, and may only be deconstructed with a <literal>case</literal> expression.
+eg. the following are valid:
+
+
+<programlisting>
+f x y = (# x+1, y-1 #)
+g x = case f x x of { (# a, b #) -&#62; a + b }
+</programlisting>
+
+
+but the following are invalid:
+
+
+<programlisting>
+f x y = g (# x, y #)
+g (# x, y #) = x + y
+</programlisting>
+
+
 </para>
 </listitem>
 </para>
 </listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Stable&rdquo; pointers:</term>
 <listitem>
 <listitem>
-<para>
-If, for some reason, you wish to hand a Haskell pointer (i.e.,
-<emphasis>not</emphasis> an unboxed value) to a C routine, you first make the
-pointer &ldquo;stable,&rdquo; so that the garbage collector won't forget that it
-exists.  That is, GHC provides a safe way to pass Haskell pointers to
-C.
-</para>
 
 <para>
 
 <para>
-Please see <xref LinkEnd="sec-stable-pointers"> for more details.
+ No variable can have an unboxed tuple type.  This is illegal:
+
+
+<programlisting>
+f :: (# Int, Int #) -&#62; (# Int, Int #)
+f x = x
+</programlisting>
+
+
+because <literal>x</literal> has an unboxed tuple type.
+
 </para>
 </listitem>
 </para>
 </listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Foreign objects&rdquo;:</term>
-<listitem>
-<para>
-A &ldquo;foreign object&rdquo; is a safe way to pass an external object (a
-C-allocated pointer, say) to Haskell and have Haskell do the Right
-Thing when it no longer references the object.  So, for example, C
-could pass a large bitmap over to Haskell and say &ldquo;please free this
-memory when you're done with it.&rdquo;
+
+</itemizedlist>
+
 </para>
 
 <para>
 </para>
 
 <para>
-Please see <xref LinkEnd="sec-ForeignObj"> for more details.
-</para>
-</listitem>
-</varlistentry>
-</variablelist>
+Note: we may relax some of these restrictions in the future.
 </para>
 
 <para>
 </para>
 
 <para>
-The libraries documentatation gives more details on all these
-&ldquo;primitive array&rdquo; types and the operations on them.
+The <literal>IO</literal> and <literal>ST</literal> monads use unboxed
+tuples to avoid unnecessary allocation during sequences of operations.
 </para>
 
 </para>
 
+</sect2>
 </sect1>
 
 
 </sect1>
 
 
-<sect1 id="nullary-types">
-<title>Data types with no constructors</title>
+<!-- ====================== SYNTACTIC EXTENSIONS =======================  -->
+
+<sect1 id="syntax-extns">
+<title>Syntactic extensions</title>
+    <!-- ====================== HIERARCHICAL MODULES =======================  -->
+
+    <sect2 id="hierarchical-modules">
+      <title>Hierarchical Modules</title>
+
+      <para>GHC supports a small extension to the syntax of module
+      names: a module name is allowed to contain a dot
+      <literal>&lsquo;.&rsquo;</literal>.  This is also known as the
+      &ldquo;hierarchical module namespace&rdquo; extension, because
+      it extends the normally flat Haskell module namespace into a
+      more flexible hierarchy of modules.</para>
+
+      <para>This extension has very little impact on the language
+      itself; modules names are <emphasis>always</emphasis> fully
+      qualified, so you can just think of the fully qualified module
+      name as <quote>the module name</quote>.  In particular, this
+      means that the full module name must be given after the
+      <literal>module</literal> keyword at the beginning of the
+      module; for example, the module <literal>A.B.C</literal> must
+      begin</para>
+
+<programlisting>module A.B.C</programlisting>
+
+
+      <para>It is a common strategy to use the <literal>as</literal>
+      keyword to save some typing when using qualified names with
+      hierarchical modules.  For example:</para>
 
 
-<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
-a data type with no constructors.  For example:</para>
 <programlisting>
 <programlisting>
-  data S      -- S :: *
-  data T a    -- T :: * -> *
+import qualified Control.Monad.ST.Strict as ST
 </programlisting>
 </programlisting>
-<para>Syntactically, the declaration lacks the "= constrs" part.  The 
-type can be parameterised, but only over ordinary types, of kind *; since
-Haskell does not have kind signatures, you cannot parameterise over higher-kinded
-types.</para>
 
 
-<para>Such data types have only one value, namely bottom.
-Nevertheless, they can be useful when defining "phantom types".</para>
-</sect1>
+      <para>Hierarchical modules have an impact on the way that GHC
+      searches for files.  For a description, see <xref
+      linkend="finding-hierarchical-modules">.</para>
+
+      <para>GHC comes with a large collection of libraries arranged
+      hierarchically; see the accompanying library documentation.
+      There is an ongoing project to create and maintain a stable set
+      of <quote>core</quote> libraries used by several Haskell
+      compilers, and the libraries that GHC comes with represent the
+      current status of that project.  For more details, see <ulink
+      url="http://www.haskell.org/~simonmar/libraries/libraries.html">Haskell
+      Libraries</ulink>.</para>
 
 
-<sect1 id="pattern-guards">
+    </sect2>
+
+    <!-- ====================== PATTERN GUARDS =======================  -->
+
+<sect2 id="pattern-guards">
 <title>Pattern guards</title>
 
 <para>
 <title>Pattern guards</title>
 
 <para>
@@ -575,9 +548,122 @@ f x | [y] <- x
 Haskell's current guards therefore emerge as a special case, in which the
 qualifier list has just one element, a boolean expression.
 </para>
 Haskell's current guards therefore emerge as a special case, in which the
 qualifier list has just one element, a boolean expression.
 </para>
-</sect1>
+</sect2>
+
+    <!-- ===================== Recursive do-notation ===================  -->
+
+<sect2 id="mdo-notation">
+<title>The recursive do-notation
+</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",
+Haskell Workshop 2002, pages: 29-37. Pittsburgh, Pennsylvania. 
+</para>
+<para>
+The do-notation of Haskell does not allow <emphasis>recursive bindings</emphasis>,
+that is, the variables bound in a do-expression are visible only in the textually following 
+code block. Compare this to a let-expression, where bound variables are visible in the entire binding
+group. It turns out that several applications can benefit from recursive bindings in
+the do-notation, and this extension provides the necessary syntactic support.
+</para>
+<para>
+Here is a simple (yet contrived) example:
+</para>
+<programlisting>
+import Control.Monad.Fix
+
+justOnes = mdo xs <- Just (1:xs)
+               return xs
+</programlisting>
+<para>
+As you can guess <literal>justOnes</literal> will evaluate to <literal>Just [1,1,1,...</literal>.
+</para>
+
+<para>
+The Control.Monad.Fix library introduces the <literal>MonadFix</literal> class. It's definition is:
+</para>
+<programlisting>
+class Monad m => MonadFix m where
+   mfix :: (a -> m a) -> m a
+</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.
+</para>
+<para>
+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).
+</para>
+<para>
+There are three important points in using the recursive-do notation:
+<itemizedlist>
+<listitem><para>
+The recursive version of the do-notation uses the keyword <literal>mdo</literal> (rather
+than <literal>do</literal>).
+</para></listitem>
+
+<listitem><para>
+You should <literal>import Control.Monad.Fix</literal>.
+(Note: Strictly speaking, this import is required only when you need to refer to the name
+<literal>MonadFix</literal> in your program, but the import is always safe, and the programmers
+are encouraged to always import this module when using the mdo-notation.)
+</para></listitem>
+
+<listitem><para>
+As with other extensions, ghc should be given the flag <literal>-fglasgow-exts</literal>
+</para></listitem>
+</itemizedlist>
+</para>
+
+<para>
+The web page: <ulink url="http://www.cse.ogi.edu/PacSoft/projects/rmb">http://www.cse.ogi.edu/PacSoft/projects/rmb</ulink>
+contains up to date information on recursive monadic bindings.
+</para>
+
+<para>
+Historical note: The old implementation of the mdo-notation (and most
+of the existing documents) used the name
+<literal>MonadRec</literal> for the class and the corresponding library.
+This name is not supported by GHC.
+</para>
+
+</sect2>
+
+
+<sect2> <title> Infix type constructors </title>
+
+<para>GHC supports infix type constructors, much as it supports infix data constructors.  For example:
+<programlisting>
+  infixl 5 :+:
+
+  data a :+: b = Inl a | Inr b
+
+  f :: a `Either` b -> a :+: b
+  f (Left x) = Inl x
+</programlisting>
+</para>
+<para>The lexical 
+syntax of an infix type constructor is just like that of an infix data constructor: either
+it's an operator beginning with ":", or it is an ordinary (alphabetic) type constructor enclosed in
+back-quotes.</para>
+
+<para>
+When you give a fixity declaration, the fixity applies to both the data constructor and the
+type constructor with the specified name.  You cannot give different fixities to the type constructor T
+and the data constructor T.
+</para>
+
 
 
-  <sect1 id="parallel-list-comprehensions">
+</sect2>
+
+   <!-- ===================== PARALLEL LIST COMPREHENSIONS ===================  -->
+
+  <sect2 id="parallel-list-comprehensions">
     <title>Parallel List Comprehensions</title>
     <indexterm><primary>list comprehensions</primary><secondary>parallel</secondary>
     </indexterm>
     <title>Parallel List Comprehensions</title>
     <indexterm><primary>list comprehensions</primary><secondary>parallel</secondary>
     </indexterm>
@@ -625,9 +711,243 @@ qualifier list has just one element, a boolean expression.
     <para>where `zipN' is the appropriate zip for the given number of
     branches.</para>
 
     <para>where `zipN' is the appropriate zip for the given number of
     branches.</para>
 
-  </sect1>
+  </sect2>
+
+<sect2 id="rebindable-syntax">
+<title>Rebindable syntax</title>
+
+
+      <para>GHC allows most kinds of built-in syntax to be rebound by
+      the user, to facilitate replacing the <literal>Prelude</literal>
+      with a home-grown version, for example.</para>
+
+            <para>You may want to define your own numeric class
+            hierarchy.  It completely defeats that purpose if the
+            literal "1" means "<literal>Prelude.fromInteger
+            1</literal>", which is what the Haskell Report specifies.
+            So the <option>-fno-implicit-prelude</option> flag causes
+            the following pieces of built-in syntax to refer to
+            <emphasis>whatever is in scope</emphasis>, not the Prelude
+            versions:</para>
+
+           <itemizedlist>
+             <listitem>
+               <para>Integer and fractional literals mean
+                "<literal>fromInteger 1</literal>" and
+                "<literal>fromRational 3.2</literal>", not the
+                Prelude-qualified versions; both in expressions and in
+                patterns. </para>
+               <para>However, the standard Prelude <literal>Eq</literal> class
+               is still used for the equality test necessary for literal patterns.</para>
+             </listitem>
+
+             <listitem>
+               <para>Negation (e.g. "<literal>- (f x)</literal>")
+               means "<literal>negate (f x)</literal>" (not
+               <literal>Prelude.negate</literal>).</para>
+             </listitem>
+
+             <listitem>
+               <para>In an n+k pattern, the standard Prelude
+                <literal>Ord</literal> class is still used for comparison,
+                but the necessary subtraction uses whatever
+                "<literal>(-)</literal>" is in scope (not
+                "<literal>Prelude.(-)</literal>").</para>
+             </listitem>
+
+             <listitem>
+         <para>"Do" notation is translated using whatever
+             functions <literal>(>>=)</literal>,
+             <literal>(>>)</literal>, <literal>fail</literal>, and
+             <literal>return</literal>, are in scope (not the Prelude
+             versions).  List comprehensions, and parallel array
+             comprehensions, are unaffected.  </para></listitem>
+           </itemizedlist>
+
+            <para>Be warned: this is an experimental facility, with fewer checks than
+            usual.  In particular, it is essential that the functions GHC finds in scope
+            must have the appropriate types, namely:
+            <screen>
+               fromInteger  :: forall a. (...) => Integer  -> a
+               fromRational :: forall a. (...) => Rational -> a
+               negate       :: forall a. (...) => a -> a
+               (-)          :: forall a. (...) => a -> a -> a
+               (>>=)        :: forall m a. (...) => m a -> (a -> m b) -> m b
+               (>>)         :: forall m a. (...) => m a -> m b -> m b
+               return       :: forall m a. (...) => a      -> m a
+               fail         :: forall m a. (...) => String -> m a
+            </screen>
+            (The (...) part can be any context including the empty context; that part 
+            is up to you.)
+            If the functions don't have the right type, very peculiar things may 
+            happen.  Use <literal>-dcore-lint</literal> to
+            typecheck the desugared program.  If Core Lint is happy you should be all right.</para>
+
+</sect2>
+</sect1>
+
+
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="type-extensions">
+<title>Type system extensions</title>
+
+<sect2 id="nullary-types">
+<title>Data types with no constructors</title>
+
+<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
+a data type with no constructors.  For example:</para>
+
+<programlisting>
+  data S      -- S :: *
+  data T a    -- T :: * -> *
+</programlisting>
+
+<para>Syntactically, the declaration lacks the "= constrs" part.  The 
+type can be parameterised over types of any kind, but if the kind is
+not <literal>*</literal> then an explicit kind annotation must be used
+(see <xref linkend="sec-kinding">).</para>
+
+<para>Such data types have only one value, namely bottom.
+Nevertheless, they can be useful when defining "phantom types".</para>
+</sect2>
+
+<sect2 id="infix-tycons">
+<title>Infix type constructors</title>
+
+<para>
+GHC allows type constructors to be operators, and to be written infix, very much 
+like expressions.  More specifically:
+<itemizedlist>
+<listitem><para>
+  A type constructor can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
+  The lexical syntax is the same as that for data constructors.
+  </para></listitem>
+<listitem><para>
+  Types can be written infix.  For example <literal>Int :*: Bool</literal>.  
+  </para></listitem>
+<listitem><para>
+  Back-quotes work
+  as for expressions, both for type constructors and type variables;  e.g. <literal>Int `Either` Bool</literal>, or
+  <literal>Int `a` Bool</literal>.  Similarly, parentheses work the same; e.g.  <literal>(:*:) Int Bool</literal>.
+  </para></listitem>
+<listitem><para>
+  Fixities may be declared for type constructors just as for data constructors.  However,
+  one cannot distinguish between the two in a fixity declaration; a fixity declaration
+  sets the fixity for a data constructor and the corresponding type constructor.  For example:
+<screen>
+  infixl 7 T, :*:
+</screen>
+  sets the fixity for both type constructor <literal>T</literal> and data constructor <literal>T</literal>,
+  and similarly for <literal>:*:</literal>.
+  <literal>Int `a` Bool</literal>.
+  </para></listitem>
+<listitem><para>
+  Function arrow is <literal>infixr</literal> with fixity 0.  (This might change; I'm not sure what it should be.)
+  </para></listitem>
+<listitem><para>
+  Data type and type-synonym declarations can be written infix.  E.g.
+<screen>
+  data a :*: b = Foo a b
+  type a :+: b = Either a b
+</screen>
+  </para></listitem>
+<listitem><para>
+  The only thing that differs between operators in types and operators in expressions is that
+  ordinary non-constructor operators, such as <literal>+</literal> and <literal>*</literal>
+  are not allowed in types. Reason: the uniform thing to do would be to make them type
+  variables, but that's not very useful.  A less uniform but more useful thing would be to
+  allow them to be type <emphasis>constructors</emphasis>.  But that gives trouble in export
+  lists.  So for now we just exclude them.
+  </para></listitem>
+
+</itemizedlist>
+</para>
+</sect2>
+
+<sect2 id="sec-kinding">
+<title>Explicitly-kinded quantification</title>
+
+<para>
+Haskell infers the kind of each type variable.  Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation, 
+just as it is nice to give a type signature for a function.  On some occasions,
+it is essential to do so.  For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+<Screen>
+     data Set cxt a = Set [a]
+                    | Unused (cxt a -> ())
+</Screen>
+The only use for the <literal>Unused</literal> constructor was to force the correct
+kind for the type variable <literal>cxt</literal>.
+</para>
+<para>
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound.  Namely:
+<itemizedlist>
+<listitem><para><literal>data</literal> declarations:
+<Screen>
+  data Set (cxt :: * -> *) a = Set [a]
+</Screen></para></listitem>
+<listitem><para><literal>type</literal> declarations:
+<Screen>
+  type T (f :: * -> *) = f Int
+</Screen></para></listitem>
+<listitem><para><literal>class</literal> declarations:
+<Screen>
+  class (Eq a) => C (f :: * -> *) a where ...
+</Screen></para></listitem>
+<listitem><para><literal>forall</literal>'s in type signatures:
+<Screen>
+  f :: forall (cxt :: * -> *). Set cxt Int
+</Screen></para></listitem>
+</itemizedlist>
+</para>
+
+<para>
+The parentheses are required.  Some of the spaces are required too, to
+separate the lexemes.  If you write <literal>(f::*->*)</literal> you
+will get a parse error, because "<literal>::*->*</literal>" is a
+single lexeme in Haskell.
+</para>
+
+<para>
+As part of the same extension, you can put kind annotations in types
+as well.  Thus:
+<Screen>
+   f :: (Int :: *) -> Int
+   g :: forall a. a -> (a :: *)
+</Screen>
+The syntax is
+<Screen>
+   atype ::= '(' ctype '::' kind ')
+</Screen>
+The parentheses are required.
+</para>
+</sect2>
+
+
+<sect2 id="class-method-types">
+<title>Class method types
+</title>
+<para>
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
+<programlisting>
+  class Seq s a where
+    fromList :: [a] -> s a
+    elem     :: Eq a => a -> s a -> Bool
+</programlisting>
+The type of <literal>elem</literal> is illegal in Haskell 98, because it
+contains the constraint <literal>Eq a</literal>, constrains only the 
+class type variable (in this case <literal>a</literal>).
+</para>
+<para>
+With the <option>-fglasgow-exts</option> GHC lifts this restriction.
+</para>
+
+</sect2>
 
 
-<sect1 id="multi-param-type-classes">
+<sect2 id="multi-param-type-classes">
 <title>Multi-parameter type classes
 </title>
 
 <title>Multi-parameter type classes
 </title>
 
@@ -654,7 +974,7 @@ Thanks to him, and to many others who have offered very useful
 feedback.
 </para>
 
 feedback.
 </para>
 
-<sect2>
+<sect3>
 <title>Types</title>
 
 <para>
 <title>Types</title>
 
 <para>
@@ -768,9 +1088,9 @@ are perfectly OK
 This choice recovers principal types, a property that Haskell 1.4 does not have.
 </para>
 
 This choice recovers principal types, a property that Haskell 1.4 does not have.
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Class declarations</title>
 
 <para>
 <title>Class declarations</title>
 
 <para>
@@ -930,9 +1250,9 @@ class like this:
 
 </para>
 
 
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2 id="instance-decls">
+<sect3 id="instance-decls">
 <title>Instance declarations</title>
 
 <para>
 <title>Instance declarations</title>
 
 <para>
@@ -955,9 +1275,9 @@ declarations
 
 However, if you give the command line option
 <option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
 
 However, if you give the command line option
 <option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
-option</primary></indexterm> then two overlapping instance declarations are permitted
-iff
-
+option</primary></indexterm> then overlapping instance declarations are permitted.
+However, GHC arranges never to commit to using an instance declaration
+if another instance declaration also applies, either now or later.
 
 <itemizedlist>
 <listitem>
 
 <itemizedlist>
 <listitem>
@@ -970,22 +1290,11 @@ iff
 
 <para>
  OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
 
 <para>
  OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
-(but not identical to <literal>type1</literal>)
+(but not identical to <literal>type1</literal>), or vice versa.
 </para>
 </listitem>
 </para>
 </listitem>
-<listitem>
-
-<para>
- OR vice versa
-</para>
-</listitem>
-
 </itemizedlist>
 </itemizedlist>
-
-
 Notice that these rules
 Notice that these rules
-
-
 <itemizedlist>
 <listitem>
 
 <itemizedlist>
 <listitem>
 
@@ -1005,8 +1314,34 @@ Reason: you can pick which instance decl
 </listitem>
 
 </itemizedlist>
 </listitem>
 
 </itemizedlist>
-
-
+However the rules are over-conservative.  Two instance declarations can overlap,
+but it can still be clear in particular situations which to use.  For example:
+<programlisting>
+  instance C (Int,a) where ...
+  instance C (a,Bool) where ...
+</programlisting>
+These are rejected by GHC's rules, but it is clear what to do when trying
+to solve the constraint <literal>C (Int,Int)</literal> because the second instance
+cannot apply.  Yell if this restriction bites you.
+</para>
+<para>
+GHC is also conservative about committing to an overlapping instance.  For example:
+<programlisting>
+  class C a where { op :: a -> a }
+  instance C [Int] where ...
+  instance C a => C [a] where ...
+  
+  f :: C b => [b] -> [b]
+  f x = op x
+</programlisting>
+From the RHS of f we get the constraint <literal>C [b]</literal>.  But
+GHC does not commit to the second instance declaration, because in a paricular
+call of f, b might be instantiate to Int, so the first instance declaration
+would be appropriate.  So GHC rejects the program.  If you add <option>-fallow-incoherent-instances</option>
+GHC will instead silently pick the second instance, without complaining about 
+the problem of subsequent instantiations.
+</para>
+<para>
 Regrettably, GHC doesn't guarantee to detect overlapping instance
 declarations if they appear in different modules.  GHC can "see" the
 instance declarations in the transitive closure of all the modules
 Regrettably, GHC doesn't guarantee to detect overlapping instance
 declarations if they appear in different modules.  GHC can "see" the
 instance declarations in the transitive closure of all the modules
@@ -1180,11 +1515,11 @@ with <option>-fcontext-stack</option><emphasis>N</emphasis>.
 
 </para>
 
 
 </para>
 
-</sect2>
+</sect3>
 
 
-</sect1>
+</sect2>
 
 
-<sect1 id="implicit-parameters">
+<sect2 id="implicit-parameters">
 <title>Implicit parameters
 </title>
 
 <title>Implicit parameters
 </title>
 
@@ -1194,12 +1529,75 @@ J Lewis, MB Shields, E Meijer, J Launchbury,
 27th ACM Symposium on Principles of Programming Languages (POPL'00),
 Boston, Jan 2000.
 </para>
 27th ACM Symposium on Principles of Programming Languages (POPL'00),
 Boston, Jan 2000.
 </para>
+<para>(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.)</para>
+<para>
+A variable is called <emphasis>dynamically bound</emphasis> when it is bound by the calling
+context of a function and <emphasis>statically bound</emphasis> when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic
+binding of variables is a notion that goes back to Lisp, but was later
+discarded in more modern incarnations, such as Scheme. Dynamic binding
+can be very confusing in an untyped language, and unfortunately, typed
+languages, in particular Hindley-Milner typed languages like Haskell,
+only support static scoping of variables.
+</para>
+<para>
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form <literal>(?x::t') => t</literal>, which says "this
+function uses a dynamically-bound variable <literal>?x</literal> 
+of type <literal>t'</literal>". For
+example, the following expresses the type of a sort function,
+implicitly parameterized by a comparison function named <literal>cmp</literal>.
+<programlisting>
+  sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+</programlisting>
+The dynamic binding constraints are just a new form of predicate in the type class system.
+</para>
+<para>
+An implicit parameter occurs in an expression using the special form <literal>?x</literal>, 
+where <literal>x</literal> is
+any valid identifier (e.g. <literal>ord ?x</literal> is a valid expression). 
+Use of this construct also introduces a new
+dynamic-binding constraint in the type of the expression. 
+For example, the following definition
+shows how we can define an implicitly parameterized sort function in
+terms of an explicitly parameterized <literal>sortBy</literal> function:
+<programlisting>
+  sortBy :: (a -> a -> Bool) -> [a] -> [a]
 
 
+  sort   :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+  sort    = sortBy ?cmp
+</programlisting>
+</para>
+
+<sect3>
+<title>Implicit-parameter type constraints</title>
 <para>
 <para>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the
+function that called it. For example, our <literal>sort</literal> function might be used
+to pick out the least value in a list:
+<programlisting>
+  least   :: (?cmp :: a -> a -> Bool) => [a] -> a
+  least xs = fst (sort xs)
+</programlisting>
+Without lifting a finger, the <literal>?cmp</literal> parameter is
+propagated to become a parameter of <literal>least</literal> as well. With explicit
+parameters, the default is that parameters must always be explicit
+propagated. With implicit parameters, the default is to always
+propagate them.
 </para>
 </para>
-<itemizedlist>
-<listitem>
+<para>
+An implicit-parameter type constraint differs from other type class constraints in the
+following way: All uses of a particular implicit parameter must have
+the same type. This means that the type of <literal>(?x, ?x)</literal> 
+is <literal>(?x::a) => (a,a)</literal>, and not 
+<literal>(?x::a, ?x::b) => (a, b)</literal>, as would be the case for type
+class constraints.
+</para>
+
 <para> You can't have an implicit parameter in the context of a class or instance
 declaration.  For example, both these declarations are illegal:
 <programlisting>
 <para> You can't have an implicit parameter in the context of a class or instance
 declaration.  For example, both these declarations are illegal:
 <programlisting>
@@ -1210,13 +1608,78 @@ Reason: exactly which implicit parameter you pick up depends on exactly where
 you invoke a function. But the ``invocation'' of instance declarations is done
 behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
 Easiest thing is to outlaw the offending types.</para>
 you invoke a function. But the ``invocation'' of instance declarations is done
 behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
 Easiest thing is to outlaw the offending types.</para>
-</listitem>
+<para>
+Implicit-parameter constraints do not cause ambiguity.  For example, consider:
+<programlisting>
+   f :: (?x :: [a]) => Int -> Int
+   f n = n + length ?x
+
+   g :: (Read a, Show a) => String -> String
+   g s = show (read s)
+</programlisting>
+Here, <literal>g</literal> has an ambiguous type, and is rejected, but <literal>f</literal>
+is fine.  The binding for <literal>?x</literal> at <literal>f</literal>'s call site is 
+quite unambiguous, and fixes the type <literal>a</literal>.
+</para>
+</sect3>
+
+<sect3>
+<title>Implicit-parameter bindings</title>
+
+<para>
+An implicit parameter is <emphasis>bound</emphasis> using the standard
+<literal>let</literal> or <literal>where</literal> binding forms.
+For example, we define the <literal>min</literal> function by binding
+<literal>cmp</literal>.
+<programlisting>
+  min :: [a] -> a
+  min  = let ?cmp = (<=) in least
+</programlisting>
+</para>
+<para>
+A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
+bindings can occur, except at top level.  That is, they can occur in a <literal>let</literal> 
+(including in a list comprehension, or do-notation, or pattern guards), 
+or a <literal>where</literal> clause.
+Note the following points:
+<itemizedlist>
+<listitem><para>
+An implicit-parameter binding group must be a
+collection of simple bindings to implicit-style variables (no
+function-style bindings, and no type signatures); these bindings are
+neither polymorphic or recursive.  
+</para></listitem>
+<listitem><para>
+You may not mix implicit-parameter bindings with ordinary bindings in a 
+single <literal>let</literal>
+expression; use two nested <literal>let</literal>s instead.
+(In the case of <literal>where</literal> you are stuck, since you can't nest <literal>where</literal> clauses.)
+</para></listitem>
 
 
+<listitem><para>
+You may put multiple implicit-parameter bindings in a
+single binding group; but they are <emphasis>not</emphasis> treated
+as a mutually recursive group (as ordinary <literal>let</literal> bindings are).
+Instead they are treated as a non-recursive group, simultaneously binding all the implicit
+parameter.  The bindings are not nested, and may be re-ordered without changing
+the meaning of the program.
+For example, consider:
+<programlisting>
+  f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
+</programlisting>
+The use of <literal>?x</literal> in the binding for <literal>?y</literal> does not "see"
+the binding for <literal>?x</literal>, so the type of <literal>f</literal> is
+<programlisting>
+  f :: (?x::Int) => Int -> Int
+</programlisting>
+</para></listitem>
 </itemizedlist>
 </itemizedlist>
+</para>
 
 
-</sect1>
+</sect3>
+</sect2>
 
 
-<sect1 id="linear-implicit-parameters">
+<sect2 id="linear-implicit-parameters">
 <title>Linear implicit parameters
 </title>
 <para>
 <title>Linear implicit parameters
 </title>
 <para>
@@ -1240,12 +1703,14 @@ written '<literal>%x</literal>' instead of '<literal>?x</literal>'.
 <para>
 For example:
 <programlisting>
 <para>
 For example:
 <programlisting>
+    import GHC.Exts( Splittable )
+
     data NameSupply = ...
     
     splitNS :: NameSupply -> (NameSupply, NameSupply)
     newName :: NameSupply -> Name
 
     data NameSupply = ...
     
     splitNS :: NameSupply -> (NameSupply, NameSupply)
     newName :: NameSupply -> Name
 
-    instance PrelSplit.Splittable NameSupply where
+    instance Splittable NameSupply where
        split = splitNS
 
 
        split = splitNS
 
 
@@ -1276,7 +1741,7 @@ the parameter explicit:
 Notice the call to 'split' introduced by the type checker.
 How did it know to use 'splitNS'?  Because what it really did
 was to introduce a call to the overloaded function 'split',
 Notice the call to 'split' introduced by the type checker.
 How did it know to use 'splitNS'?  Because what it really did
 was to introduce a call to the overloaded function 'split',
-defined by
+defined by the class <literal>Splittable</literal>:
 <programlisting>
        class Splittable a where
          split :: a -> (a,a)
 <programlisting>
        class Splittable a where
          split :: a -> (a,a)
@@ -1290,8 +1755,8 @@ and GHC will infer
 <programlisting>
        g :: (Splittable a, %ns :: a) => b -> (b,a,a)
 </programlisting>
 <programlisting>
        g :: (Splittable a, %ns :: a) => b -> (b,a,a)
 </programlisting>
-The <literal>Splittable</literal> class is built into GHC.  It's defined in <literal>PrelSplit</literal>,
-and exported by <literal>GlaExts</literal>.
+The <literal>Splittable</literal> class is built into GHC.  It's exported by module 
+<literal>GHC.Exts</literal>.
 </para>
 <para>
 Other points:
 </para>
 <para>
 Other points:
@@ -1308,7 +1773,7 @@ are entirely distinct implicit parameters: you
 </itemizedlist>
 </para>
 
 </itemizedlist>
 </para>
 
-<sect2><title>Warnings</title>
+<sect3><title>Warnings</title>
 
 <para>
 The monomorphism restriction is even more important than usual.
 
 <para>
 The monomorphism restriction is even more important than usual.
@@ -1340,81 +1805,145 @@ parameters we have already lost beta reduction anyway, and
 Haskell programs without knowing their typing.
 </para>
 
 Haskell programs without knowing their typing.
 </para>
 
-</sect2>
+</sect3>
 
 
-</sect1>
+<sect3><title>Recursive functions</title>
+<para>Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
+<programlisting>
+        foo :: %x::T => Int -> [Int]
+        foo 0 = []
+        foo n = %x : foo (n-1)
+</programlisting>
+where T is some type in class Splittable.</para>
+<para>
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+</para><para>
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect.  Here's the
+translated term, where the implicit param is made explicit:
+<programlisting>
+        foo x 0 = []
+        foo x n = let (x1,x2) = split x
+                  in x1 : foo x2 (n-1)
+</programlisting>
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work.  So the translation becomes
+<programlisting>
+        foo x = let
+                  foom 0 = []
+                  foom n = x : foom (n-1)
+                in
+                foom
+</programlisting>
+Result: 'x' is not split, and you get a list of identical T's.  So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+</para><para>
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right.  That is why they are an experimental feature. 
+</para>
+</sect3>
+
+</sect2>
 
 
-<sect1 id="functional-dependencies">
+<sect2 id="functional-dependencies">
 <title>Functional dependencies
 </title>
 
 <para> Functional dependencies are implemented as described by Mark Jones
 <title>Functional dependencies
 </title>
 
 <para> Functional dependencies are implemented as described by Mark Jones
-in "Type Classes with Functional Dependencies", Mark P. Jones, 
+in &ldquo;<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>&rdquo;, Mark P. Jones, 
 In Proceedings of the 9th European Symposium on Programming, 
 In Proceedings of the 9th European Symposium on Programming, 
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782.
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
 </para>
 
 <para>
 There should be more documentation, but there isn't (yet).  Yell if you need it.
 </para>
 </para>
 
 <para>
 There should be more documentation, but there isn't (yet).  Yell if you need it.
 </para>
-</sect1>
+</sect2>
 
 
 
 
-<sect1 id="universal-quantification">
-<title>Explicit universal quantification
+<sect2 id="universal-quantification">
+<title>Arbitrary-rank polymorphism
 </title>
 
 <para>
 </title>
 
 <para>
-GHC's type system supports explicit universal quantification in
-constructor fields and function arguments.  This is useful for things
-like defining <literal>runST</literal> from the state-thread world. 
-GHC's syntax for this now agrees with Hugs's, namely:
+Haskell type signatures are implicitly quantified.  The new keyword <literal>forall</literal>
+allows us to say exactly what this means.  For example:
 </para>
 </para>
-
 <para>
 <para>
-
 <programlisting>
 <programlisting>
-        forall a b. (Ord a, Eq  b) => a -> b -> a
+        g :: b -> b
 </programlisting>
 </programlisting>
-
-</para>
-
-<para>
-The context is, of course, optional.  You can't use <literal>forall</literal> as
-a type variable any more!
+means this:
+<programlisting>
+        g :: forall b. (b -> b)
+</programlisting>
+The two are treated identically.
 </para>
 
 <para>
 </para>
 
 <para>
-Haskell type signatures are implicitly quantified.  The <literal>forall</literal>
-allows us to say exactly what this means.  For example:
-</para>
+However, GHC's type system supports <emphasis>arbitrary-rank</emphasis> 
+explicit universal quantification in
+types. 
+For example, all the following types are legal:
+<programlisting>
+    f1 :: forall a b. a -> b -> a
+    g1 :: forall a b. (Ord a, Eq  b) => a -> b -> a
 
 
-<para>
+    f2 :: (forall a. a->a) -> Int -> Int
+    g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
 
 
-<programlisting>
-        g :: b -> b
+    f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
 </programlisting>
 </programlisting>
-
+Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
+can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
+The <literal>forall</literal> makes explicit the universal quantification that
+is implicitly added by Haskell.
 </para>
 </para>
-
 <para>
 <para>
-means this:
+The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
+the <literal>forall</literal> is on the left of a function arrrow.  As <literal>g2</literal>
+shows, the polymorphic type on the left of the function arrow can be overloaded.
 </para>
 </para>
-
 <para>
 <para>
-
+The functions <literal>f3</literal> and <literal>g3</literal> have rank-3 types;
+they have rank-2 types on the left of a function arrow.
+</para>
+<para>
+GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
+arbitrarily deep in function arrows.   (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+<itemizedlist>
+<listitem> <para> On the left of a function arrow </para> </listitem>
+<listitem> <para> On the right of a function arrow (see <xref linkend="hoist">) </para> </listitem>
+<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the <literal>f1,f2,f3,g1,g2,g3</literal> above would be valid
+field type signatures.</para> </listitem>
+<listitem> <para> As the type of an implicit parameter </para> </listitem>
+<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables">) </para> </listitem>
+</itemizedlist>
+There is one place you cannot put a <literal>forall</literal>:
+you cannot instantiate a type variable with a forall-type.  So you cannot 
+make a forall-type the argument of a type constructor.  So these types are illegal:
 <programlisting>
 <programlisting>
-        g :: forall b. (b -> b)
+    x1 :: [forall a. a->a]
+    x2 :: (forall a. a->a, Int)
+    x3 :: Maybe (forall a. a->a)
 </programlisting>
 </programlisting>
-
+Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
+a type variable any more!
 </para>
 
 </para>
 
-<para>
-The two are treated identically.
-</para>
 
 
-<sect2 id="univ">
-<title>Universally-quantified data type fields
+<sect3 id="univ">
+<title>Examples
 </title>
 
 <para>
 </title>
 
 <para>
@@ -1437,8 +1966,7 @@ newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
 </para>
 
 <para>
 </para>
 
 <para>
-The constructors now have so-called <emphasis>rank 2</emphasis> polymorphic
-types, in which there is a for-all in the argument types.:
+The constructors have rank-2 types:
 </para>
 
 <para>
 </para>
 
 <para>
@@ -1482,11 +2010,6 @@ to <emphasis>require</emphasis> explicit quantification on constructor arguments
 where that is what is wanted.  Feedback welcomed.)
 </para>
 
 where that is what is wanted.  Feedback welcomed.)
 </para>
 
-</sect2>
-
-<sect2>
-<title>Construction </title>
-
 <para>
 You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
 the constructor to suitable values, just as usual.  For example,
 <para>
 You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
 the constructor to suitable values, just as usual.  For example,
@@ -1495,17 +2018,23 @@ the constructor to suitable values, just as usual.  For example,
 <para>
 
 <programlisting>
 <para>
 
 <programlisting>
-(T1 (\xy->x) 3) :: T Int
-
-(MkSwizzle sort)    :: Swizzle
-(MkSwizzle reverse) :: Swizzle
+    a1 :: T Int
+    a1 = T1 (\xy->x) 3
+    
+    a2, a3 :: Swizzle
+    a2 = MkSwizzle sort
+    a3 = MkSwizzle reverse
+    
+    a4 :: MonadT Maybe
+    a4 = let r x = Just x
+            b m k = case m of
+                      Just y -> k y
+                      Nothing -> Nothing
+         in
+         MkMonad r b
 
 
-(let r x = Just x
-     b m k = case m of
-                Just y -> k y
-                Nothing -> Nothing
-  in
-  MkMonad r b) :: MonadT Maybe
+    mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+    mkTs f x y = [T1 f x, T1 f y]
 </programlisting>
 
 </para>
 </programlisting>
 
 </para>
@@ -1516,11 +2045,6 @@ required, as <literal>(MkSwizzle reverse)</literal> shows.  (<function>reverse</
 does not need the <literal>Ord</literal> constraint.)
 </para>
 
 does not need the <literal>Ord</literal> constraint.)
 </para>
 
-</sect2>
-
-<sect2>
-<title>Pattern matching</title>
-
 <para>
 When you use pattern matching, the bound variables may now have
 polymorphic types.  For example:
 <para>
 When you use pattern matching, the bound variables may now have
 polymorphic types.  For example:
@@ -1529,17 +2053,17 @@ polymorphic types.  For example:
 <para>
 
 <programlisting>
 <para>
 
 <programlisting>
-        f :: T a -> a -> (a, Char)
-        f (T1 f k) x = (f k x, f 'c' 'd')
+    f :: T a -> a -> (a, Char)
+    f (T1 w k) x = (w k x, w 'c' 'd')
 
 
-        g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
-        g (MkSwizzle s) xs f = s (map f (s xs))
+    g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+    g (MkSwizzle s) xs f = s (map f (s xs))
 
 
-        h :: MonadT m -> [m a] -> m [a]
-        h m [] = return m []
-        h m (x:xs) = bind m x           $ \y ->
-                      bind m (h m xs)   $ \ys ->
-                      return m (y:ys)
+    h :: MonadT m -> [m a] -> m [a]
+    h m [] = return m []
+    h m (x:xs) = bind m x          $ \y ->
+                 bind m (h m xs)   $ \ys ->
+                 return m (y:ys)
 </programlisting>
 
 </para>
 </programlisting>
 
 </para>
@@ -1550,205 +2074,200 @@ and <literal>bind</literal> to extract the polymorphic bind and return functions
 from the <literal>MonadT</literal> data structure, rather than using pattern
 matching.
 </para>
 from the <literal>MonadT</literal> data structure, rather than using pattern
 matching.
 </para>
+</sect3>
 
 
-<para>
-You cannot pattern-match against an argument that is polymorphic.
-For example:
-
-<programlisting>
-        newtype TIM s a = TIM (ST s (Maybe a))
-
-        runTIM :: (forall s. TIM s a) -> Maybe a
-        runTIM (TIM m) = runST m
-</programlisting>
-
-</para>
+<sect3>
+<title>Type inference</title>
 
 <para>
 
 <para>
-Here the pattern-match fails, because you can't pattern-match against
-an argument of type <literal>(forall s. TIM s a)</literal>.  Instead you
-must bind the variable and pattern match in the right hand side:
-
-<programlisting>
-        runTIM :: (forall s. TIM s a) -> Maybe a
-        runTIM tm = case tm of { TIM m -> runST m }
-</programlisting>
-
-The <literal>tm</literal> on the right hand side is (invisibly) instantiated, like
-any polymorphic value at its occurrence site, and now you can pattern-match
-against it.
+In general, type inference for arbitrary-rank types is undecideable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
 </para>
 </para>
-
-</sect2>
-
-<sect2>
-<title>The partial-application restriction</title>
-
 <para>
 <para>
-There is really only one way in which data structures with polymorphic
-components might surprise you: you must not partially apply them.
-For example, this is illegal:
+<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it</emphasis>.
 </para>
 </para>
-
 <para>
 <para>
-
+What does it mean to "provide" an explicit type for x?  You can do that by 
+giving a type signature for x directly, using a pattern type signature
+(<xref linkend="scoped-type-variables">), thus:
 <programlisting>
 <programlisting>
-        map MkSwizzle [sort, reverse]
+     \ f :: (forall a. a->a) -> (f True, f 'c')
 </programlisting>
 </programlisting>
-
-</para>
-
-<para>
-The restriction is this: <emphasis>every subexpression of the program must
-have a type that has no for-alls, except that in a function
-application (f e1&hellip;en) the partial applications are not subject to
-this rule</emphasis>.  The restriction makes type inference feasible.
-</para>
-
-<para>
-In the illegal example, the sub-expression <literal>MkSwizzle</literal> has the
-polymorphic type <literal>(Ord b => [b] -> [b]) -> Swizzle</literal> and is not
-a sub-expression of an enclosing application.  On the other hand, this
-expression is OK:
-</para>
-
-<para>
-
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
 <programlisting>
 <programlisting>
-        map (T1 (\a b -> a)) [1,2,3]
+     (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
 </programlisting>
 </programlisting>
-
-</para>
-
-<para>
-even though it involves a partial application of <function>T1</function>, because
-the sub-expression <literal>T1 (\a b -> a)</literal> has type <literal>Int -> T
-Int</literal>.
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f.  Similarly, and more commonly,
+one can give a type signature for the function itself:
+<programlisting>
+     h :: (forall a. a->a) -> (Bool,Char)
+     h f = (f True, f 'c')
+</programlisting>
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument.  Here is an example we saw earlier:
+<programlisting>
+    f :: T a -> a -> (a, Char)
+    f (T1 w k) x = (w k x, w 'c' 'd')
+</programlisting>
+Here we do not need to give a type signature to <literal>w</literal>, because
+it is an argument of constructor <literal>T1</literal> and that tells GHC all
+it needs to know.
 </para>
 
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2 id="sigs">
-<title>Type signatures
-</title>
 
 
-<para>
-Once you have data constructors with universally-quantified fields, or
-constants such as <Constant>runST</Constant> that have rank-2 types, it isn't long
-before you discover that you need more!  Consider:
-</para>
+<sect3 id="implicit-quant">
+<title>Implicit quantification</title>
 
 <para>
 
 <para>
-
+GHC performs implicit quantification as follows.  <emphasis>At the top level (only) of 
+user-written types, if and only if there is no explicit <literal>forall</literal>,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them.</emphasis>  For example, the following pairs are 
+equivalent:
 <programlisting>
 <programlisting>
-  mkTs f x y = [T1 f x, T1 f y]
-</programlisting>
-
-</para>
-
-<para>
-<function>mkTs</function> is a fuction that constructs some values of type
-<literal>T</literal>, using some pieces passed to it.  The trouble is that since
-<literal>f</literal> is a function argument, Haskell assumes that it is
-monomorphic, so we'll get a type error when applying <function>T1</function> to
-it.  This is a rather silly example, but the problem really bites in
-practice.  Lots of people trip over the fact that you can't make
-"wrappers functions" for <Constant>runST</Constant> for exactly the same reason.
-In short, it is impossible to build abstractions around functions with
-rank-2 types.
-</para>
+  f :: a -> a
+  f :: forall a. a -> a
 
 
-<para>
-The solution is fairly clear.  We provide the ability to give a rank-2
-type signature for <emphasis>ordinary</emphasis> functions (not only data
-constructors), thus:
+  g (x::a) = let
+                h :: a -> b -> b
+                h x y = y
+             in ...
+  g (x::a) = let
+                h :: forall b. a -> b -> b
+                h x y = y
+             in ...
+</programlisting>
 </para>
 </para>
-
 <para>
 <para>
-
+Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
+point.  For example:
 <programlisting>
 <programlisting>
-  mkTs :: (forall b. b -> b -> b) -> a -> [T a]
-  mkTs f x y = [T1 f x, T1 f y]
-</programlisting>
+  f :: (a -> a) -> Int
+           -- MEANS
+  f :: forall a. (a -> a) -> Int
+           -- NOT
+  f :: (forall a. a -> a) -> Int
 
 
-</para>
 
 
-<para>
-This type signature tells the compiler to attribute <literal>f</literal> with
-the polymorphic type <literal>(forall b. b -> b -> b)</literal> when type
-checking the body of <function>mkTs</function>, so now the application of
-<function>T1</function> is fine.
+  g :: (Ord a => a -> a) -> Int
+           -- MEANS the illegal type
+  g :: forall a. (Ord a => a -> a) -> Int
+           -- NOT
+  g :: (forall a. Ord a => a -> a) -> Int
+</programlisting>
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple.  If you want the latter type, you
+can write your for-alls explicitly.  Indeed, doing so is strongly advised
+for rank-2 types.
 </para>
 </para>
+</sect3>
+</sect2>
 
 
-<para>
-There are two restrictions:
-</para>
+<sect2 id="type-synonyms">
+<title>Liberalised type synonyms 
+</title>
 
 <para>
 
 <para>
-
+Type synonmys are like macros at the type level, and
+GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
+That means that GHC can be very much more liberal about type synonyms than Haskell 98:
 <itemizedlist>
 <itemizedlist>
-<listitem>
-
-<para>
- You can only define a rank 2 type, specified by the following
-grammar:
-
-
+<listitem> <para>You can write a <literal>forall</literal> (including overloading)
+in a type synonym, thus:
 <programlisting>
 <programlisting>
-rank2type ::= [forall tyvars .] [context =>] funty
-funty     ::= ([forall tyvars .] [context =>] ty) -> funty
-            | ty
-ty        ::= ...current Haskell monotype syntax...
-</programlisting>
-
+  type Discard a = forall b. Show b => a -> b -> (a, String)
 
 
-Informally, the universal quantification must all be right at the beginning,
-or at the top level of a function argument.
+  f :: Discard a
+  f x y = (x, show y)
 
 
+  g :: Discard Int -> (Int,Bool)    -- A rank-2 type
+  g f = f Int True
+</programlisting>
 </para>
 </listitem>
 </para>
 </listitem>
-<listitem>
 
 
-<para>
- There is a restriction on the definition of a function whose
-type signature is a rank-2 type: the polymorphic arguments must be
-matched on the left hand side of the "<literal>=</literal>" sign.  You can't
-define <function>mkTs</function> like this:
+<listitem><para>
+You can write an unboxed tuple in a type synonym:
+<programlisting>
+  type Pr = (# Int, Int #)
 
 
+  h :: Int -> Pr
+  h x = (# x, x #)
+</programlisting>
+</para></listitem>
 
 
+<listitem><para>
+You can apply a type synonym to a forall type:
 <programlisting>
 <programlisting>
-mkTs :: (forall b. b -> b -> b) -> a -> [T a]
-mkTs = \ f x y -> [T1 f x, T1 f y]
+  type Foo a = a -> a -> Bool
+  f :: Foo (forall b. b->b)
 </programlisting>
 </programlisting>
+After expanding the synonym, <literal>f</literal> has the legal (in GHC) type:
+<programlisting>
+  f :: (forall b. b->b) -> (forall b. b->b) -> Bool
+</programlisting>
+</para></listitem>
 
 
+<listitem><para>
+You can apply a type synonym to a partially applied type synonym:
+<programlisting>
+  type Generic i o = forall x. i x -> o x
+  type Id x = x
+  
+  foo :: Generic Id []
+</programlisting>
+After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+<programlisting>
+  foo :: forall x. x -> [x]
+</programlisting>
+</para></listitem>
 
 
-
-The same partial-application rule applies to ordinary functions with
-rank-2 types as applied to data constructors.
-
+</itemizedlist>
 </para>
 </para>
-</listitem>
 
 
+<para>
+GHC currently does kind checking before expanding synonyms (though even that
+could be changed.)
+</para>
+<para>
+After expanding type synonyms, GHC does validity checking on types, looking for
+the following mal-formedness which isn't detected simply by kind checking:
+<itemizedlist>
+<listitem><para>
+Type constructor applied to a type involving for-alls.
+</para></listitem>
+<listitem><para>
+Unboxed tuple on left of an arrow.
+</para></listitem>
+<listitem><para>
+Partially-applied type synonym.
+</para></listitem>
 </itemizedlist>
 </itemizedlist>
+So, for example,
+this will be rejected:
+<programlisting>
+  type Pr = (# Int, Int #)
 
 
+  h :: Pr -> Int
+  h x = ...
+</programlisting>
+because GHC does not allow  unboxed tuples on the left of a function arrow.
 </para>
 </para>
-
 </sect2>
 
 </sect2>
 
-
 <sect2 id="hoist">
 <sect2 id="hoist">
-<title>Type synonyms and hoisting
-</title>
-
+<title>For-all hoisting</title>
 <para>
 <para>
-GHC also allows you to write a <literal>forall</literal> in a type synonym, thus:
-<programlisting>
-  type Discard a = forall b. a -> b -> a
-
-  f :: Discard a
-  f x y = x
-</programlisting>
-However, it is often convenient to use these sort of synonyms at the right hand
+It is often convenient to use generalised type synonyms at the right hand
 end of an arrow, thus:
 <programlisting>
   type Discard a = forall b. a -> b -> a
 end of an arrow, thus:
 <programlisting>
   type Discard a = forall b. a -> b -> a
@@ -1768,9 +2287,9 @@ In general, the rule is this: <emphasis>to determine the type specified by any e
 user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
 performs the transformation:</emphasis>
 <programlisting>
 user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
 performs the transformation:</emphasis>
 <programlisting>
-  <emphasis>type1</emphasis> -> forall a. <emphasis>type2</emphasis>
+  <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
 ==>
 ==>
-  forall a. <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
+  forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
 </programlisting>
 (In fact, GHC tries to retain as much synonym information as possible for use in
 error messages, but that is a usability issue.)  This rule applies, of course, whether
 </programlisting>
 (In fact, GHC tries to retain as much synonym information as possible for use in
 error messages, but that is a usability issue.)  This rule applies, of course, whether
@@ -1780,11 +2299,22 @@ valid way to write <literal>g</literal>'s type signature:
   g :: Int -> Int -> forall b. b -> Int
 </programlisting>
 </para>
   g :: Int -> Int -> forall b. b -> Int
 </programlisting>
 </para>
+<para>
+When doing this hoisting operation, GHC eliminates duplicate constraints.  For
+example:
+<programlisting>
+  type Foo a = (?x::Int) => Bool -> a
+  g :: Foo (Foo Int)
+</programlisting>
+means
+<programlisting>
+  g :: (?x::Int) => Bool -> Bool -> Int
+</programlisting>
+</para>
 </sect2>
 
 </sect2>
 
-</sect1>
 
 
-<sect1 id="existential-quantification">
+<sect2 id="existential-quantification">
 <title>Existentially quantified data constructors
 </title>
 
 <title>Existentially quantified data constructors
 </title>
 
@@ -1874,7 +2404,7 @@ that collection of packages in a uniform manner.  You can express
 quite a bit of object-oriented-like programming this way.
 </para>
 
 quite a bit of object-oriented-like programming this way.
 </para>
 
-<sect2 id="existential">
+<sect3 id="existential">
 <title>Why existential?
 </title>
 
 <title>Why existential?
 </title>
 
@@ -1897,9 +2427,9 @@ But Haskell programmers can safely think of the ordinary
 adding a new existential quantification construct.
 </para>
 
 adding a new existential quantification construct.
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Type classes</title>
 
 <para>
 <title>Type classes</title>
 
 <para>
@@ -1942,7 +2472,7 @@ So this program is legal:
   f :: Baz -> String
   f (Baz1 p q) | p == q    = "Yes"
                | otherwise = "No"
   f :: Baz -> String
   f (Baz1 p q) | p == q    = "Yes"
                | otherwise = "No"
-  f (Baz1 v fn)            = show (fn v)
+  f (Baz2 v fn)            = show (fn v)
 </programlisting>
 
 </para>
 </programlisting>
 
 </para>
@@ -1959,9 +2489,9 @@ Notice the way that the syntax fits smoothly with that used for
 universal quantification earlier.
 </para>
 
 universal quantification earlier.
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Restrictions</title>
 
 <para>
 <title>Restrictions</title>
 
 <para>
@@ -2032,8 +2562,13 @@ bindings. So this is illegal:
   f3 x = a==b where { Baz1 a b = x }
 </programlisting>
 
   f3 x = a==b where { Baz1 a b = x }
 </programlisting>
 
+Instead, use a <literal>case</literal> expression:
+
+<programlisting>
+  f3 x = case x of Baz1 a b -> a==b
+</programlisting>
 
 
-You can only pattern-match
+In general, you can only pattern-match
 on an existentially-quantified constructor in a <literal>case</literal> expression or
 in the patterns of a function definition.
 
 on an existentially-quantified constructor in a <literal>case</literal> expression or
 in the patterns of a function definition.
 
@@ -2105,92 +2640,12 @@ declarations.  Define your own instances!
 
 </para>
 
 
 </para>
 
-</sect2>
-
-</sect1>
-
-<sect1 id="sec-assertions">
-<title>Assertions
-<indexterm><primary>Assertions</primary></indexterm>
-</title>
-
-<para>
-If you want to make use of assertions in your standard Haskell code, you
-could define a function like the following:
-</para>
-
-<para>
-
-<programlisting>
-assert :: Bool -> a -> a
-assert False x = error "assertion failed!"
-assert _     x = x
-</programlisting>
-
-</para>
-
-<para>
-which works, but gives you back a less than useful error message --
-an assertion failed, but which and where?
-</para>
-
-<para>
-One way out is to define an extended <function>assert</function> function which also
-takes a descriptive string to include in the error message and
-perhaps combine this with the use of a pre-processor which inserts
-the source location where <function>assert</function> was used.
-</para>
-
-<para>
-Ghc offers a helping hand here, doing all of this for you. For every
-use of <function>assert</function> in the user's source:
-</para>
-
-<para>
-
-<programlisting>
-kelvinToC :: Double -> Double
-kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
-</programlisting>
-
-</para>
-
-<para>
-Ghc will rewrite this to also include the source location where the
-assertion was made,
-</para>
-
-<para>
-
-<programlisting>
-assert pred val ==> assertError "Main.hs|15" pred val
-</programlisting>
-
-</para>
-
-<para>
-The rewrite is only performed by the compiler when it spots
-applications of <function>Exception.assert</function>, so you can still define and
-use your own versions of <function>assert</function>, should you so wish. If not,
-import <literal>Exception</literal> to make use <function>assert</function> in your code.
-</para>
-
-<para>
-To have the compiler ignore uses of assert, use the compiler option
-<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts option</primary></indexterm> That is,
-expressions of the form <literal>assert pred e</literal> will be rewritten to <literal>e</literal>.
-</para>
-
-<para>
-Assertion failures can be caught, see the documentation for the
-<literal>Exception</literal> library (<xref linkend="sec-Exception">)
-for the details.
-</para>
+</sect3>
 
 
-</sect1>
+</sect2>
 
 
-<sect1 id="scoped-type-variables">
-<title>Scoped Type Variables
+<sect2 id="scoped-type-variables">
+<title>Scoped type variables
 </title>
 
 <para>
 </title>
 
 <para>
@@ -2240,7 +2695,7 @@ are noted.
 So much for the basic idea.  Here are the details.
 </para>
 
 So much for the basic idea.  Here are the details.
 </para>
 
-<sect2>
+<sect3>
 <title>What a pattern type signature means</title>
 <para>
 A type variable brought into scope by a pattern type signature is simply
 <title>What a pattern type signature means</title>
 <para>
 A type variable brought into scope by a pattern type signature is simply
@@ -2278,9 +2733,9 @@ For example, all of these are legal:</para>
   w (x::a) = x                  -- a unifies with [b]
 </programlisting>
 
   w (x::a) = x                  -- a unifies with [b]
 </programlisting>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Scope and implicit quantification</title>
 
 <para>
 <title>Scope and implicit quantification</title>
 
 <para>
@@ -2412,9 +2867,9 @@ scope over the methods defined in the <literal>where</literal> part.  For exampl
 
 </para>
 
 
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Result type signatures</title>
 
 <para>
 <title>Result type signatures</title>
 
 <para>
@@ -2455,9 +2910,9 @@ you want:
 Result type signatures are not yet implemented in Hugs.
 </para>
 
 Result type signatures are not yet implemented in Hugs.
 </para>
 
-</sect2>
+</sect3>
 
 
-<sect2>
+<sect3>
 <title>Where a pattern type signature can occur</title>
 
 <para>
 <title>Where a pattern type signature can occur</title>
 
 <para>
@@ -2569,11 +3024,443 @@ in <literal>f4</literal>'s scope.
 </itemizedlist>
 </para>
 
 </itemizedlist>
 </para>
 
+</sect3>
+</sect2>
+
+<sect2 id="newtype-deriving">
+<title>Generalised derived instances for newtypes</title>
+
+<para>
+When you define an abstract type using <literal>newtype</literal>, you may want
+the new type to inherit some instances from its representation. In
+Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
+other classes you have to write an explicit instance declaration. For
+example, if you define
+
+<programlisting> 
+  newtype Dollars = Dollars Int 
+</programlisting> 
+
+and you want to use arithmetic on <literal>Dollars</literal>, you have to
+explicitly define an instance of <literal>Num</literal>:
+
+<programlisting> 
+  instance Num Dollars where
+    Dollars a + Dollars b = Dollars (a+b)
+    ...
+</programlisting>
+All the instance does is apply and remove the <literal>newtype</literal>
+constructor. It is particularly galling that, since the constructor
+doesn't appear at run-time, this instance declaration defines a
+dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
+dictionary, only slower!
+</para>
+
+
+<sect3> <title> Generalising the deriving clause </title>
+<para>
+GHC now permits such instances to be derived instead, so one can write 
+<programlisting> 
+  newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+</programlisting> 
+
+and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
+for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
+derives an instance declaration of the form
+
+<programlisting> 
+  instance Num Int => Num Dollars
+</programlisting> 
+
+which just adds or removes the <literal>newtype</literal> constructor according to the type.
+</para>
+<para>
+
+We can also derive instances of constructor classes in a similar
+way. For example, suppose we have implemented state and failure monad
+transformers, such that
+
+<programlisting> 
+  instance Monad m => Monad (State s m) 
+  instance Monad m => Monad (Failure m)
+</programlisting> 
+In Haskell 98, we can define a parsing monad by 
+<programlisting> 
+  type Parser tok m a = State [tok] (Failure m) a
+</programlisting> 
+
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract,
+without needing to write an instance of class <literal>Monad</literal>, via
+
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving Monad
+</programlisting>
+In this case the derived instance declaration is of the form 
+<programlisting> 
+  instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) 
+</programlisting> 
+
+Notice that, since <literal>Monad</literal> is a constructor class, the
+instance is a <emphasis>partial application</emphasis> of the new type, not the
+entire left hand side. We can imagine that the type declaration is
+``eta-converted'' to generate the context of the instance
+declaration.
+</para>
+<para>
+
+We can even derive instances of multi-parameter classes, provided the
+newtype is the last class parameter. In this case, a ``partial
+application'' of the class appears in the <literal>deriving</literal>
+clause. For example, given the class
+
+<programlisting> 
+  class StateMonad s m | m -> s where ... 
+  instance Monad m => StateMonad s (State s m) where ... 
+</programlisting> 
+then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by 
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving (Monad, StateMonad [tok])
+</programlisting>
+
+The derived instance is obtained by completing the application of the
+class to the new type:
+
+<programlisting> 
+  instance StateMonad [tok] (State [tok] (Failure m)) =>
+           StateMonad [tok] (Parser tok m)
+</programlisting>
+</para>
+<para>
+
+As a result of this extension, all derived instances in newtype
+declarations are treated uniformly (and implemented just by reusing
+the dictionary for the representation type), <emphasis>except</emphasis>
+<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
+the newtype and its representation.
+</para>
+</sect3>
+
+<sect3> <title> A more precise specification </title>
+<para>
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
+
+<programlisting> 
+  newtype T v1...vn = T' (S t1...tk vk+1...vn) deriving (c1...cm) 
+</programlisting> 
+
+where <literal>S</literal> is a type constructor, <literal>t1...tk</literal> are 
+types,
+<literal>vk+1...vn</literal> are type variables which do not occur in any of
+the <literal>ti</literal>, and the <literal>ci</literal> are partial applications of
+classes of the form <literal>C t1'...tj'</literal>.  The derived instance
+declarations are, for each <literal>ci</literal>,
+
+<programlisting> 
+  instance ci (S t1...tk vk+1...v) => ci (T v1...vp)
+</programlisting>
+where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the 
+right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
+</para>
+<para>
+
+As an example which does <emphasis>not</emphasis> work, consider 
+<programlisting> 
+  newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
+</programlisting> 
+Here we cannot derive the instance 
+<programlisting> 
+  instance Monad (State s m) => Monad (NonMonad m) 
+</programlisting> 
+
+because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
+and so cannot be "eta-converted" away. It is a good thing that this
+<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
+not, in fact, a monad --- for the same reason. Try defining
+<literal>>>=</literal> with the correct type: you won't be able to.
+</para>
+<para>
+
+Notice also that the <emphasis>order</emphasis> of class parameters becomes
+important, since we can only derive instances for the last one. If the
+<literal>StateMonad</literal> class above were instead defined as
+
+<programlisting> 
+  class StateMonad m s | m -> s where ... 
+</programlisting>
+
+then we would not have been able to derive an instance for the
+<literal>Parser</literal> type above. We hypothesise that multi-parameter
+classes usually have one "main" parameter for which deriving new
+instances is most interesting.
+</para>
+</sect3>
+
+</sect2>
+
+
+</sect1>
+<!-- ==================== End of type system extensions =================  -->
+  
+<!-- ====================== TEMPLATE HASKELL =======================  -->
+
+<sect1 id="template-haskell">
+<title>Template Haskell</title>
+
+<para>Template Haskell allows you to do compile-time meta-programming in Haskell.  The background 
+the main technical innovations are discussed in "<ulink
+url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
+Template Meta-programming for Haskell</ulink>", in 
+Proc Haskell Workshop 2002.
+</para>
+
+<para> The first example from that paper is set out below as a worked example to help get you started. 
+</para>
+
+<para>
+The documentation here describes the realisation in GHC.  (It's rather sketchy just now;
+Tim Sheard is going to expand it.)
+</para>
+
+<sect2>  <title> Syntax </title>
+<para>
+    Template Haskell has the following new syntactic constructions.  You need to use the flag  
+               <literal>-fglasgow-exts</literal> to switch these syntactic extensions on.
+
+       <itemizedlist>
+             <listitem><para>
+                 A splice is written <literal>$x</literal>, where <literal>x</literal> is an
+                 identifier, or <literal>$(...)</literal>, where the "..." is an arbitrary expression.
+                 There must be no space between the "$" and the identifier or parenthesis.  This use
+                 of "$" overrides its meaning as an infix operator, just as "M.x" overrides the meaning
+                 of "." as an infix operator.  If you want the infix operator, put spaces around it.
+                 </para>
+             <para> A splice can occur in place of 
+                 <itemizedlist>
+                   <listitem><para> an expression; the spliced expression must have type <literal>Expr</literal></para></listitem>
+                   <listitem><para> a list of top-level declarations; ; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>
+                   <listitem><para> a type; the spliced expression must have type <literal>Type</literal>.</para></listitem>
+                   </itemizedlist>
+          (Note that the syntax for a declaration splice uses "<literal>$</literal>" not "<literal>splice</literal>" as in
+       the paper. Also the type of the enclosed expression must be  <literal>Q [Dec]</literal>, not  <literal>[Q Dec]</literal>
+       as in the paper.)
+               </para></listitem>
+
+
+             <listitem><para>
+                 A expression quotation is written in Oxford brackets, thus:
+                 <itemizedlist>
+                   <listitem><para> <literal>[| ... |]</literal>, where the "..." is an expression; 
+                             the quotation has type <literal>Expr</literal>.</para></listitem>
+                   <listitem><para> <literal>[d| ... |]</literal>, where the "..." is a list of top-level declarations;
+                             the quotation has type <literal>Q [Dec]</literal>.</para></listitem>
+                   <listitem><para> <literal>[t| ... |]</literal>, where the "..." is a type; 
+                             the quotation has type <literal>Type</literal>.</para></listitem>
+                 </itemizedlist></para></listitem>
+
+             <listitem><para>
+                 Reification is written thus:
+                 <itemizedlist>
+                   <listitem><para> <literal>reifyDecl T</literal>, where <literal>T</literal> is a type constructor; this expression
+                     has type <literal>Dec</literal>. </para></listitem>
+                   <listitem><para> <literal>reifyDecl C</literal>, where <literal>C</literal> is a class; has type <literal>Dec</literal>.</para></listitem>
+                   <listitem><para> <literal>reifyType f</literal>, where <literal>f</literal> is an identifier; has type <literal>Typ</literal>.</para></listitem>
+                   <listitem><para> Still to come: fixities </para></listitem>
+                   
+                 </itemizedlist></para>
+               </listitem>
+
+                 
+       </itemizedlist>
+</para>
+</sect2>
+
+<sect2>  <title> Using Template Haskell </title>
+<para>
+<itemizedlist>
+    <listitem><para>
+    The data types and monadic constructor functions for Template Haskell are in the library
+    <literal>Language.Haskell.THSyntax</literal>.
+    </para></listitem>
+
+    <listitem><para>
+    You can only run a function at compile time if it is imported from another module.  That is,
+           you can't define a function in a module, and call it from within a splice in the same module.
+           (It would make sense to do so, but it's hard to implement.)
+   </para></listitem>
+
+    <listitem><para>
+           The flag <literal>-ddump-splices</literal> shows the expansion of all top-level splices as they happen.
+   </para></listitem>
+</itemizedlist>
+</para>
+<para> Template Haskell works in any mode (<literal>--make</literal>, <literal>--interactive</literal>,
+       or file-at-a-time).  There used to be a restriction to the former two, but that restriction 
+       has been lifted.
+</para>
+</sect2>
+<sect2>  <title> A Template Haskell Worked Example </title>
+<para>To help you get over the confidence barrier, try out this skeletal worked example.
+  First cut and paste the two modules below into "Main.hs" and "Printf.hs":</para>
+
+<programlisting>
+{- Main.hs -}
+module Main where
+
+-- Import our template "pr"
+import Printf ( pr )
+
+-- The splice operator $ takes the Haskell source code
+-- generated at compile time by "pr" and splices it into
+-- the argument of "putStrLn".
+main = putStrLn ( $(pr "Hello") )
+</programlisting>
+
+<programlisting>
+{- Printf.hs -}
+module Printf where
+
+-- Skeletal printf from the paper.
+-- It needs to be in a separate module to the one where
+-- you intend to use it.
+
+-- Import some Template Haskell syntax
+import Language.Haskell.THSyntax
+
+-- Describe a format string
+data Format = D | S | L String
+
+-- Parse a format string.  This is left largely to you
+-- as we are here interested in building our first ever
+-- Template Haskell program and not in building printf.
+parse :: String -> [Format]
+parse s   = [ L s ]
+
+-- Generate Haskell source code from a parsed representation
+-- of the format string.  This code will be spliced into
+-- the module which calls "pr", at compile time.
+gen :: [Format] -> Expr
+gen [D]   = [| \n -> show n |]
+gen [S]   = [| \s -> s |]
+gen [L s] = string s
+
+-- Here we generate the Haskell code for the splice
+-- from an input format string.
+pr :: String -> Expr
+pr s      = gen (parse s)
+</programlisting>
+
+<para>Now run the compiler (here we are using a "stage three" build of GHC, at a Cygwin prompt on Windows):
+</para>
+<programlisting>
+stage3/ghc/compiler/ghc-inplace --make -fglasgow-exts -package haskell-src main.hs -o main.exe
+</programlisting>
+
+<para>Run "main.exe" and here is your output:
+</para>
+
+<programlisting>
+$ ./main
+Hello
+</programlisting>
+
 </sect2>
 </sect2>
+</sect1>
+
+<!-- ==================== ASSERTIONS =================  -->
+
+<sect1 id="sec-assertions">
+<title>Assertions
+<indexterm><primary>Assertions</primary></indexterm>
+</title>
+
+<para>
+If you want to make use of assertions in your standard Haskell code, you
+could define a function like the following:
+</para>
+
+<para>
+
+<programlisting>
+assert :: Bool -> a -> a
+assert False x = error "assertion failed!"
+assert _     x = x
+</programlisting>
+
+</para>
+
+<para>
+which works, but gives you back a less than useful error message --
+an assertion failed, but which and where?
+</para>
+
+<para>
+One way out is to define an extended <function>assert</function> function which also
+takes a descriptive string to include in the error message and
+perhaps combine this with the use of a pre-processor which inserts
+the source location where <function>assert</function> was used.
+</para>
+
+<para>
+Ghc offers a helping hand here, doing all of this for you. For every
+use of <function>assert</function> in the user's source:
+</para>
+
+<para>
+
+<programlisting>
+kelvinToC :: Double -> Double
+kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
+</programlisting>
+
+</para>
+
+<para>
+Ghc will rewrite this to also include the source location where the
+assertion was made,
+</para>
+
+<para>
+
+<programlisting>
+assert pred val ==> assertError "Main.hs|15" pred val
+</programlisting>
+
+</para>
 
 
+<para>
+The rewrite is only performed by the compiler when it spots
+applications of <function>Control.Exception.assert</function>, so you
+can still define and use your own versions of
+<function>assert</function>, should you so wish. If not, import
+<literal>Control.Exception</literal> to make use
+<function>assert</function> in your code.
+</para>
+
+<para>
+To have the compiler ignore uses of assert, use the compiler option
+<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts
+option</primary></indexterm> That is, expressions of the form
+<literal>assert pred e</literal> will be rewritten to
+<literal>e</literal>.
+</para>
+
+<para>
+Assertion failures can be caught, see the documentation for the
+<literal>Control.Exception</literal> library for the details.
+</para>
 
 </sect1>
 
 
 </sect1>
 
+
+<!-- =============================== PRAGMAS ===========================  -->
+
   <sect1 id="pragmas">
     <title>Pragmas</title>
 
   <sect1 id="pragmas">
     <title>Pragmas</title>
 
@@ -2856,6 +3743,8 @@ GHC will print the specified message.
 
 </sect1>
 
 
 </sect1>
 
+<!--  ======================= REWRITE RULES ======================== -->
+
 <sect1 id="rewrite-rules">
 <title>Rewrite rules
 
 <sect1 id="rewrite-rules">
 <title>Rewrite rules
 
@@ -3670,6 +4559,8 @@ Just to finish with, here's another example I rather like:
 </sect2>
 </sect1>
 
 </sect2>
 </sect1>
 
+
+
 <!-- Emacs stuff:
      ;;; Local Variables: ***
      ;;; mode: sgml ***
 <!-- Emacs stuff:
      ;;; Local Variables: ***
      ;;; mode: sgml ***