[project @ 2005-10-26 13:03:39 by simonpj]

[ghc-hetmet.git] / ghc / docs / users_guide / glasgow_exts.xml

diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index 5a22e7c..36b7bf8 100644 (file)
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -219,6 +219,28 @@ documentation</ulink> describes all the libraries that come with GHC.
       </varlistentry>
 
       <varlistentry>
       </varlistentry>
 
       <varlistentry>

+       <term><option>-fimplicit-params</option></term>
+       <listitem>
+         <para>Enables implicit parameters (see <xref
+         linkend="implicit-parameters"/>).  Currently also implied by 
+         <option>-fglasgow-exts</option>.</para>
+
+         <para>Syntax stolen:
+         <literal>?<replaceable>varid</replaceable></literal>,
+         <literal>%<replaceable>varid</replaceable></literal>.</para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term><option>-fscoped-type-variables</option></term>
+       <listitem>
+         <para>Enables lexically-scoped type variables (see <xref
+         linkend="scoped-type-variables"/>).  Implied by
+         <option>-fglasgow-exts</option>.</para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>

        <term><option>-fth</option></term>
        <listitem>
          <para>Enables Template Haskell (see <xref
        <term><option>-fth</option></term>
        <listitem>
          <para>Enables Template Haskell (see <xref

@@ -233,19 +255,6 @@ documentation</ulink> describes all the libraries that come with GHC.
        </listitem>
       </varlistentry>
 
        </listitem>
       </varlistentry>
 

-      <varlistentry>
-       <term><option>-fimplicit-params</option></term>
-       <listitem>
-         <para>Enables implicit parameters (see <xref
-         linkend="implicit-parameters"/>).  Currently also implied by 
-         <option>-fglasgow-exts</option>.</para>
-
-         <para>Syntax stolen:
-         <literal>?<replaceable>varid</replaceable></literal>,
-         <literal>%<replaceable>varid</replaceable></literal>.</para>
-       </listitem>
-      </varlistentry>
-

     </variablelist>
   </sect1>
 
     </variablelist>
   </sect1>
 

@@ -270,7 +279,7 @@ 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
 
 <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>.
+<filename>fptools/ghc/compiler/prelude/primops.txt.pp</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>
 
 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>
 

@@ -334,11 +343,16 @@ 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.
 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.

+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>
 
 <para>
 </para>
 
 <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
+There are some restrictions on the use of primitive types:
+<itemizedlist>
+<listitem><para>The main restriction
+is 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
 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

@@ -350,11 +364,33 @@ 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>
 worse, the unboxed value might be larger than a pointer
 (<literal>Double&num;</literal> for instance).
 </para>

+</listitem>
+<listitem><para> You cannot bind a variable with an unboxed type
+in a <emphasis>top-level</emphasis> binding.
+</para></listitem>
+<listitem><para> You cannot bind a variable with an unboxed type
+in a <emphasis>recursive</emphasis> binding.
+</para></listitem>
+<listitem><para> You may bind unboxed variables in a (non-recursive,
+non-top-level) pattern binding, but any such variable causes the entire
+pattern-match
+to become strict.  For example:
+<programlisting>
+  data Foo = Foo Int Int#

 
 

-<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.
+  f x = let (Foo a b, w) = ..rhs.. in ..body..
+</programlisting>
+Since <literal>b</literal> has type <literal>Int#</literal>, the entire pattern
+match
+is strict, and the program behaves as if you had written
+<programlisting>
+  data Foo = Foo Int Int#
+
+  f x = case ..rhs.. of { (Foo a b, w) -> ..body.. }
+</programlisting>
+</para>
+</listitem>
+</itemizedlist>

 </para>
 
 </sect2>
 </para>
 
 </sect2>

@@ -389,21 +425,19 @@ 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
 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
+of the primitive operations listed in <literal>primops.txt.pp</literal> return unboxed

 tuples.
 tuples.

+In particular, the <literal>IO</literal> and <literal>ST</literal> monads use unboxed
+tuples to avoid unnecessary allocation during sequences of operations.

 </para>
 
 <para>
 There are some pretty stringent restrictions on the use of unboxed tuples:
 </para>
 
 <para>
 There are some pretty stringent restrictions on the use of unboxed tuples:

-</para>
-
-<para>
-

 <itemizedlist>
 <listitem>
 
 <para>
 <itemizedlist>
 <listitem>
 
 <para>

- Unboxed tuple types are subject to the same restrictions as
+Values of 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.
 
 other unboxed types; i.e. they may not be stored in polymorphic data
 structures or passed to polymorphic functions.
 

@@ -412,56 +446,46 @@ structures or passed to polymorphic functions.
 <listitem>
 
 <para>
 <listitem>
 
 <para>

- 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:
+No variable can have an unboxed tuple type, nor may a constructor or function
+argument have an unboxed tuple type.  The following are all illegal:

 
 
 <programlisting>
 
 
 <programlisting>

-f x y = g (# x, y #)
-g (# x, y #) = x + y
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
+  data Foo = Foo (# Int, Int #)

 
 

-<para>
- No variable can have an unboxed tuple type.  This is illegal:
+  f :: (# Int, Int #) -&#62; (# Int, Int #)
+  f x = x

 
 

+  g :: (# Int, Int #) -&#62; Int
+  g (# a,b #) = a

 
 

-<programlisting>
-f :: (# Int, Int #) -&#62; (# Int, Int #)
-f x = x
+  h x = let y = (# x,x #) in ...

 </programlisting>
 </programlisting>

-
-
-because <literal>x</literal> has an unboxed tuple type.
-

 </para>
 </listitem>
 </para>
 </listitem>

-

 </itemizedlist>
 </itemizedlist>

-
-</para>
-
-<para>
-Note: we may relax some of these restrictions in the future.

 </para>
 </para>

-

 <para>
 <para>

-The <literal>IO</literal> and <literal>ST</literal> monads use unboxed
-tuples to avoid unnecessary allocation during sequences of operations.
+The typical use of unboxed tuples is simply to return multiple values,
+binding those multiple results with a <literal>case</literal> expression, thus:
+<programlisting>
+  f x y = (# x+1, y-1 #)
+  g x = case f x x of { (# a, b #) -&#62; a + b }
+</programlisting>
+You can have an unboxed tuple in a pattern binding, thus
+<programlisting>
+  f x = let (# p,q #) = h x in ..body..
+</programlisting>
+If the types of <literal>p</literal> and <literal>q</literal> are not unboxed,
+the resulting binding is lazy like any other Haskell pattern binding.  The 
+above example desugars like this:
+<programlisting>
+  f x = let t = case h x o f{ (# p,q #) -> (p,q)
+            p = fst t
+            q = snd t
+        in ..body..
+</programlisting>
+Indeed, the bindings can even be recursive.

 </para>
 
 </sect2>
 </para>
 
 </sect2>

@@ -619,7 +643,7 @@ clunky env var1 var1
 </programlisting>
 
 <para>
 </programlisting>
 
 <para>

-The semantics should be clear enough.  The qualifers are matched in order. 
+The semantics should be clear enough.  The qualifiers are matched in order. 

 For a <literal>&lt;-</literal> qualifier, which I call a pattern guard, the
 right hand side is evaluated and matched against the pattern on the left. 
 If the match fails then the whole guard fails and the next equation is
 For a <literal>&lt;-</literal> qualifier, which I call a pattern guard, the
 right hand side is evaluated and matched against the pattern on the left. 
 If the match fails then the whole guard fails and the next equation is

@@ -801,60 +825,72 @@ This name is not supported by GHC.
             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
             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>
+            versions:

 
            <itemizedlist>
              <listitem>
 
            <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>
+               <para>An integer literal <literal>368</literal> means
+                "<literal>fromInteger (368::Integer)</literal>", rather than
+                "<literal>Prelude.fromInteger (368::Integer)</literal>".
+</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>Fractional literals are handed in just the same way,
+         except that the translation is 
+             <literal>fromRational (3.68::Rational)</literal>.
+</para> </listitem>        
+
+         <listitem><para>The equality test in an overloaded numeric pattern
+             uses whatever <literal>(==)</literal> is in scope.
+</para> </listitem>        
+
+         <listitem><para>The subtraction operation, and the
+         greater-than-or-equal test, in <literal>n+k</literal> patterns
+             use whatever <literal>(-)</literal> and <literal>(>=)</literal> are in scope.
+             </para></listitem>

 
              <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>
+               <para>Negation (e.g. "<literal>- (f x)</literal>")
+               means "<literal>negate (f x)</literal>", both in numeric
+               patterns, and expressions.
+             </para></listitem>

 
              <listitem>
          <para>"Do" notation is translated using whatever
              functions <literal>(>>=)</literal>,
 
              <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
+             <literal>(>>)</literal>, and <literal>fail</literal>,
+             are in scope (not the Prelude
+             versions).  List comprehensions, mdo (<xref linkend="mdo-notation"/>), and parallel array

              comprehensions, are unaffected.  </para></listitem>
              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>
+             <listitem>
+               <para>Arrow
+               notation (see <xref linkend="arrow-notation"/>)
+               uses whatever <literal>arr</literal>,
+               <literal>(>>>)</literal>, <literal>first</literal>,
+               <literal>app</literal>, <literal>(|||)</literal> and
+               <literal>loop</literal> functions are in scope. But unlike the
+               other constructs, the types of these functions must match the
+               Prelude types very closely.  Details are in flux; if you want
+               to use this, ask!
+             </para></listitem>
+           </itemizedlist>
+In all cases (apart from arrow notation), the static semantics should be that of the desugared form,
+even if that is a little unexpected. For emample, the 
+static semantics of the literal <literal>368</literal>
+is exactly that of <literal>fromInteger (368::Integer)</literal>; it's fine for
+<literal>fromInteger</literal> to have any of the types:
+<programlisting>
+fromInteger :: Integer -> Integer
+fromInteger :: forall a. Foo a => Integer -> a
+fromInteger :: Num a => a -> Integer
+fromInteger :: Integer -> Bool -> Bool
+</programlisting>
+</para>
+               
+            <para>Be warned: this is an experimental facility, with
+            fewer checks than usual.  Use <literal>-dcore-lint</literal>
+            to typecheck the desugared program.  If Core Lint is happy
+            you should be all right.</para>

 
 </sect2>
 </sect1>
 
 </sect2>
 </sect1>

@@ -889,18 +925,49 @@ Nevertheless, they can be useful when defining "phantom types".</para>
 </sect3>
 
 <sect3 id="infix-tycons">
 </sect3>
 
 <sect3 id="infix-tycons">

-<title>Infix type constructors</title>
+<title>Infix type constructors, classes, and type variables</title>

 
 <para>
 
 <para>

-GHC allows type constructors to be operators, and to be written infix, very much 
-like expressions.  More specifically:
+GHC allows type constructors, classes, and type variables to be operators, and
+to be written infix, very much like expressions.  More specifically:

 <itemizedlist>
 <listitem><para>
 <itemizedlist>
 <listitem><para>

-  A type constructor can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
+  A type constructor or class 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>
   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>.  
+  Data type and type-synonym declarations can be written infix, parenthesised
+  if you want further arguments.  E.g.
+<screen>
+  data a :*: b = Foo a b
+  type a :+: b = Either a b
+  class a :=: b where ...
+
+  data (a :**: b) x = Baz a b x
+  type (a :++: b) y = Either (a,b) y
+</screen>
+  </para></listitem>
+<listitem><para>
+  Types, and class constraints, can be written infix.  For example
+  <screen>
+       x :: Int :*: Bool
+        f :: (a :=: b) => a -> b
+  </screen>
+  </para></listitem>
+<listitem><para>
+  A type variable can be an (unqualified) operator e.g. <literal>+</literal>.
+  The lexical syntax is the same as that for variable operators, excluding "(.)",
+  "(!)", and "(*)".  In a binding position, the operator must be
+  parenthesised.  For example:
+<programlisting>
+   type T (+) = Int + Int
+   f :: T Either
+   f = Left 3
+ 
+   liftA2 :: Arrow (~>)
+         => (a -> b -> c) -> (e ~> a) -> (e ~> b) -> (e ~> c)
+   liftA2 = ...
+</programlisting>

   </para></listitem>
 <listitem><para>
   Back-quotes work
   </para></listitem>
 <listitem><para>
   Back-quotes work

@@ -908,7 +975,7 @@ like expressions.  More specifically:
   <literal>Int `a` Bool</literal>.  Similarly, parentheses work the same; e.g.  <literal>(:*:) Int Bool</literal>.
   </para></listitem>
 <listitem><para>
   <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,
+  Fixities may be declared for type constructors, or classes, 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>
   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>

@@ -921,21 +988,6 @@ like expressions.  More specifically:
 <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>
   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>
 
 </itemizedlist>
 </para>

@@ -945,7 +997,7 @@ like expressions.  More specifically:
 <title>Liberalised type synonyms</title>
 
 <para>
 <title>Liberalised type synonyms</title>
 
 <para>

-Type synonmys are like macros at the type level, and
+Type synonyms 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>
 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>

@@ -994,7 +1046,7 @@ You can apply a type synonym to a partially applied type synonym:
   
   foo :: Generic Id []
 </programlisting>
   
   foo :: Generic Id []
 </programlisting>

-After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+After expanding the synonym, <literal>foo</literal> has the legal (in GHC) type:

 <programlisting>
   foo :: forall x. x -> [x]
 </programlisting>
 <programlisting>
   foo :: forall x. x -> [x]
 </programlisting>

@@ -1040,8 +1092,12 @@ because GHC does not allow  unboxed tuples on the left of a function arrow.
 
 <para>
 The idea of using existential quantification in data type declarations
 
 <para>
 The idea of using existential quantification in data type declarations

-was suggested by Laufer (I believe, thought doubtless someone will
-correct me), and implemented in Hope+. It's been in Lennart
+was suggested by Perry, and implemented in Hope+ (Nigel Perry, <emphasis>The Implementation
+of Practical Functional Programming Languages</emphasis>, PhD Thesis, University of
+London, 1991). It was later formalised by Laufer and Odersky
+(<emphasis>Polymorphic type inference and abstract data types</emphasis>,
+TOPLAS, 16(5), pp1411-1430, 1994).
+It's been in Lennart

 Augustsson's <command>hbc</command> Haskell compiler for several years, and
 proved very useful.  Here's the idea.  Consider the declaration:
 </para>
 Augustsson's <command>hbc</command> Haskell compiler for several years, and
 proved very useful.  Here's the idea.  Consider the declaration:
 </para>

@@ -1373,19 +1429,20 @@ declarations.  Define your own instances!
 <title>Class declarations</title>
 
 <para>
 <title>Class declarations</title>
 
 <para>

-This section documents GHC's implementation of multi-parameter type
-classes.  There's lots of background in the paper <ulink
-url="http://research.microsoft.com/~simonpj/multi.ps.gz" >Type
+This section, and the next one, documents GHC's type-class extensions.
+There's lots of background in the paper <ulink
+url="http://research.microsoft.com/~simonpj/Papers/type-class-design-space" >Type

 classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
 Jones, Erik Meijer).
 </para>
 <para>
 classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
 Jones, Erik Meijer).
 </para>
 <para>

-There are the following constraints on class declarations:
-<orderedlist>
-<listitem>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>

 
 

+<sect3>
+<title>Multi-parameter type classes</title>

 <para>
 <para>

- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+Multi-parameter type classes are permitted. For example:

 
 
 <programlisting>
 
 
 <programlisting>

@@ -1394,14 +1451,30 @@ There are the following constraints on class declarations:
     ...etc.
 </programlisting>
 
     ...etc.
 </programlisting>
 

+</para>
+</sect3>
+
+<sect3>
+<title>The superclasses of a class declaration</title>
+
+<para>
+There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic.  So these class declarations are OK:

 
 
 
 

-</para>
-</listitem>
-<listitem>
+<programlisting>
+  class Functor (m k) => FiniteMap m k where
+    ...
+
+  class (Monad m, Monad (t m)) => Transform t m where
+    lift :: m a -> (t m) a
+</programlisting>
+

 
 

+</para>

 <para>
 <para>

- <emphasis>The class hierarchy must be acyclic</emphasis>.  However, the definition
+As in Haskell 98, The class hierarchy must be acyclic.  However, the definition

 of "acyclic" involves only the superclass relationships.  For example,
 this is OK:
 
 of "acyclic" involves only the superclass relationships.  For example,
 this is OK:
 

@@ -1418,37 +1491,58 @@ this is OK:
 Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
 class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>.  (It
 would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
 Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
 class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>.  (It
 would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)

-

 </para>
 </para>

-</listitem>
-<listitem>
+</sect3>

 
 

-<para>
- <emphasis>There are no restrictions on the context in a class declaration
-(which introduces superclasses), except that the class hierarchy must
-be acyclic</emphasis>.  So these class declarations are OK:

 
 
 
 

-<programlisting>
-  class Functor (m k) => FiniteMap m k where
-    ...

 
 

-  class (Monad m, Monad (t m)) => Transform t m where
-    lift :: m a -> (t m) a
+<sect3 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>
 </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>).
+GHC lifts this restriction.
+</para>

 
 
 
 

-</para>
-</listitem>
+</sect3>

 
 

-<listitem>

 
 

+<sect3 id="functional-dependencies">
+<title>Functional dependencies
+</title>
+
+<para> Functional dependencies are implemented as described by Mark 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, 
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
+</para>

 <para>
 <para>

- <emphasis>All of the class type variables must be reachable (in the sense 
-mentioned in <xref linkend="type-restrictions"/>)
-from the free varibles of each method type
-</emphasis>.  For example:
+Functional dependencies are introduced by a vertical bar in the syntax of a 
+class declaration;  e.g. 
+<programlisting>
+  class (Monad m) => MonadState s m | m -> s where ...

 
 

+  class Foo a b c | a b -> c where ...
+</programlisting>
+There should be more documentation, but there isn't (yet).  Yell if you need it.
+</para>
+<para>
+In a class declaration, all of the class type variables must be reachable (in the sense 
+mentioned in <xref linkend="type-restrictions"/>)
+from the free variables of each method type.
+For example:

 
 <programlisting>
   class Coll s a where
 
 <programlisting>
   class Coll s a where

@@ -1456,14 +1550,16 @@ from the free varibles of each method type
     insert :: s -> a -> s
 </programlisting>
 
     insert :: s -> a -> s
 </programlisting>
 

-

 is not OK, because the type of <literal>empty</literal> doesn't mention
 is not OK, because the type of <literal>empty</literal> doesn't mention

-<literal>a</literal>.  This rule is a consequence of Rule 1(a), above, for
-types, and has the same motivation.
-
-Sometimes, offending class declarations exhibit misunderstandings.  For
-example, <literal>Coll</literal> might be rewritten
+<literal>a</literal>.  Functional dependencies can make the type variable
+reachable:
+<programlisting>
+  class Coll s a | s -> a where
+    empty  :: s
+    insert :: s -> a -> s
+</programlisting>

 
 

+Alternatively <literal>Coll</literal> might be rewritten

 
 <programlisting>
   class Coll s a where
 
 <programlisting>
   class Coll s a where

@@ -1485,299 +1581,135 @@ class like this:
   class CollE s => Coll s a where
     insert :: s -> a -> s
 </programlisting>
   class CollE s => Coll s a where
     insert :: s -> a -> s
 </programlisting>

-
-

 </para>
 </para>

-</listitem>
+</sect3>
+

 
 

-</orderedlist>
-</para>

 
 

-<sect3 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>

 
 

-</sect3>

 
 </sect2>
 
 
 </sect2>
 

-<sect2 id="type-restrictions">
-<title>Type signatures</title>
+<sect2 id="instance-decls">
+<title>Instance declarations</title>
+
+<sect3 id="instance-heads">
+<title>Instance heads</title>

 
 

-<sect3><title>The context of a type signature</title>

 <para>
 <para>

-Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variable)</emphasis> or
-<emphasis>(class (type-variable type-variable ...))</emphasis>.  Thus,
-these type signatures are perfectly OK
-<programlisting>
-  g :: Eq [a] => ...
-  g :: Ord (T a ()) => ...
-</programlisting>
+The <emphasis>head</emphasis> of an instance declaration is the part to the
+right of the "<literal>=&gt;</literal>".  In Haskell 98 the head of an instance
+declaration
+must be of the form <literal>C (T a1 ... an)</literal>, where
+<literal>C</literal> is the class, <literal>T</literal> is a type constructor,
+and the <literal>a1 ... an</literal> are distinct type variables.

 </para>
 <para>
 </para>
 <para>

-GHC imposes the following restrictions on the constraints in a type signature.
-Consider the type:
-
+The <option>-fglasgow-exts</option> flag lifts this restriction and allows the
+instance head to be of form <literal>C t1 ... tn</literal> where <literal>t1
+... tn</literal> are arbitrary types (provided, of course, everything is
+well-kinded).  In particular, types <literal>ti</literal> can be type variables
+or structured types, and can contain repeated occurrences of a single type
+variable.
+Examples:

 <programlisting>
 <programlisting>

-  forall tv1..tvn (c1, ...,cn) => type
-</programlisting>
+  instance Eq (T a a) where ...
+       -- Repeated type variable

 
 

-(Here, we write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 98, all the free type variables of an
-explicit source-language type signature are universally quantified,
-except for the class type variables in a class declaration.  However,
-in GHC, you can give the foralls if you want.  See <xref linkend="universal-quantification"/>).
+  instance Eq (S [a]) where ...
+       -- Structured type
+
+  instance C Int [a] where ...
+       -- Multiple parameters
+</programlisting>

 </para>
 </para>

+</sect3>

 
 

+<sect3 id="instance-overlap">
+<title>Overlapping instances</title>

 <para>
 <para>

-
-<orderedlist>
-<listitem>
-
+In general, <emphasis>GHC requires that that it be unambiguous which instance
+declaration
+should be used to resolve a type-class constraint</emphasis>. This behaviour
+can be modified by two flags: <option>-fallow-overlapping-instances</option>
+<indexterm><primary>-fallow-overlapping-instances
+</primary></indexterm> 
+and <option>-fallow-incoherent-instances</option>
+<indexterm><primary>-fallow-incoherent-instances
+</primary></indexterm>, as this section discusses.</para>
+<para>
+When GHC tries to resolve, say, the constraint <literal>C Int Bool</literal>,
+it tries to match every instance declaration against the
+constraint,
+by instantiating the head of the instance declaration.  For example, consider
+these declarations:
+<programlisting>
+  instance context1 => C Int a     where ...  -- (A)
+  instance context2 => C a   Bool  where ...  -- (B)
+  instance context3 => C Int [a]   where ...  -- (C)
+  instance context4 => C Int [Int] where ...  -- (D)
+</programlisting>
+The instances (A) and (B) match the constraint <literal>C Int Bool</literal>, 
+but (C) and (D) do not.  When matching, GHC takes
+no account of the context of the instance declaration
+(<literal>context1</literal> etc).
+GHC's default behaviour is that <emphasis>exactly one instance must match the
+constraint it is trying to resolve</emphasis>.  
+It is fine for there to be a <emphasis>potential</emphasis> of overlap (by
+including both declarations (A) and (B), say); an error is only reported if a 
+particular constraint matches more than one.
+</para>
+
+<para>
+The <option>-fallow-overlapping-instances</option> flag instructs GHC to allow
+more than one instance to match, provided there is a most specific one.  For
+example, the constraint <literal>C Int [Int]</literal> matches instances (A),
+(C) and (D), but the last is more specific, and hence is chosen.  If there is no
+most-specific match, the program is rejected.
+</para>
+<para>
+However, GHC is conservative about committing to an overlapping instance.  For example:
+<programlisting>
+  f :: [b] -> [b]
+  f x = ...
+</programlisting>
+Suppose that from the RHS of <literal>f</literal> we get the constraint
+<literal>C Int [b]</literal>.  But
+GHC does not commit to instance (C), because in a particular
+call of <literal>f</literal>, <literal>b</literal> might be instantiate 
+to <literal>Int</literal>, in which case instance (D) would be more specific still.
+So GHC rejects the program.  If you add the flag <option>-fallow-incoherent-instances</option>,
+GHC will instead pick (C), without complaining about 
+the problem of subsequent instantiations.
+</para>

 <para>
 <para>

- <emphasis>Each universally quantified type variable
-<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
-
-A type variable <literal>a</literal> is "reachable" if it it appears
-in the same constraint as either a type variable free in in
-<literal>type</literal>, or another reachable type variable.  
-A value with a type that does not obey 
-this reachability restriction cannot be used without introducing
-ambiguity; that is why the type is rejected.
-Here, for example, is an illegal type:
-
-
-<programlisting>
-  forall a. Eq a => Int
-</programlisting>
-
-
-When a value with this type was used, the constraint <literal>Eq tv</literal>
-would be introduced where <literal>tv</literal> is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
-can never know which instance of <literal>Eq</literal> to use because we never
-get any more information about <literal>tv</literal>.
-</para>
-<para>
-Note
-that the reachability condition is weaker than saying that <literal>a</literal> is
-functionally dependendent on a type variable free in
-<literal>type</literal> (see <xref
-linkend="functional-dependencies"/>).  The reason for this is there
-might be a "hidden" dependency, in a superclass perhaps.  So
-"reachable" is a conservative approximation to "functionally dependent".
-For example, consider:
-<programlisting>
-  class C a b | a -> b where ...
-  class C a b => D a b where ...
-  f :: forall a b. D a b => a -> a
-</programlisting>
-This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
-but that is not immediately apparent from <literal>f</literal>'s type.
-</para>
-</listitem>
-<listitem>
-
-<para>
- <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
-universally quantified type variables <literal>tvi</literal></emphasis>.
-
-For example, this type is OK because <literal>C a b</literal> mentions the
-universally quantified type variable <literal>b</literal>:
-
-
-<programlisting>
-  forall a. C a b => burble
-</programlisting>
-
-
-The next type is illegal because the constraint <literal>Eq b</literal> does not
-mention <literal>a</literal>:
-
-
-<programlisting>
-  forall a. Eq b => burble
-</programlisting>
-
-
-The reason for this restriction is milder than the other one.  The
-excluded types are never useful or necessary (because the offending
-context doesn't need to be witnessed at this point; it can be floated
-out).  Furthermore, floating them out increases sharing. Lastly,
-excluding them is a conservative choice; it leaves a patch of
-territory free in case we need it later.
-
-</para>
-</listitem>
-
-</orderedlist>
-
-</para>
-</sect3>
-
-<sect3 id="hoist">
-<title>For-all hoisting</title>
-<para>
-It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
-end of an arrow, thus:
-<programlisting>
-  type Discard a = forall b. a -> b -> a
-
-  g :: Int -> Discard Int
-  g x y z = x+y
-</programlisting>
-Simply expanding the type synonym would give
-<programlisting>
-  g :: Int -> (forall b. Int -> b -> Int)
-</programlisting>
-but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
-<programlisting>
-  g :: forall b. Int -> Int -> b -> Int
-</programlisting>
-In general, the rule is this: <emphasis>to determine the type specified by any explicit
-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 a1..an. <emphasis>context2</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
-or not the <literal>forall</literal> comes from a synonym. For example, here is another
-valid way to write <literal>g</literal>'s type signature:
-<programlisting>
-  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>
-</sect3>
-
-
-</sect2>
-
-<sect2 id="instance-decls">
-<title>Instance declarations</title>
-
-<sect3>
-<title>Overlapping instances</title>
-<para>
-In general, <emphasis>instance declarations may not overlap</emphasis>.  The two instance
-declarations
-
-
-<programlisting>
-  instance context1 => C type1 where ...
-  instance context2 => C type2 where ...
-</programlisting>
-
-"overlap" if <literal>type1</literal> and <literal>type2</literal> unify.
-</para>
-<para>
-However, if you give the command line option
-<option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
-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>
-
-<para>
- EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
-</para>
-</listitem>
-<listitem>
-
-<para>
- OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
-(but not identical to <literal>type1</literal>), or vice versa.
-</para>
-</listitem>
-</itemizedlist>
-Notice that these rules
+The willingness to be overlapped or incoherent is a property of 
+the <emphasis>instance declaration</emphasis> itself, controlled by the
+presence or otherwise of the <option>-fallow-overlapping-instances</option> 
+and <option>-fallow-incoherent-instances</option> flags when that mdodule is
+being defined.  Neither flag is required in a module that imports and uses the
+instance declaration.  Specifically, during the lookup process:

 <itemizedlist>
 <itemizedlist>

-<listitem>
-
-<para>
- make it clear which instance decl to use
-(pick the most specific one that matches)
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
-Reason: you can pick which instance decl
-"matches" based on the type.
-</para>
-</listitem>
-
+<listitem><para>
+An instance declaration is ignored during the lookup process if (a) a more specific
+match is found, and (b) the instance declaration was compiled with 
+<option>-fallow-overlapping-instances</option>.  The flag setting for the
+more-specific instance does not matter.
+</para></listitem>
+<listitem><para>
+Suppose an instance declaration does not matche the constraint being looked up, but
+does unify with it, so that it might match when the constraint is further 
+instantiated.  Usually GHC will regard this as a reason for not committing to
+some other constraint.  But if the instance declaration was compiled with
+<option>-fallow-incoherent-instances</option>, GHC will skip the "does-it-unify?" 
+check for that declaration.
+</para></listitem>

 </itemizedlist>
 </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.
+All this makes it possible for a library author to design a library that relies on 
+overlapping instances without the library client having to know.

 </para>
 </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
-imported by the one being compiled, so it can "see" all instance decls
-when it is compiling <literal>Main</literal>.  However, it currently chooses not
-to look at ones that can't possibly be of use in the module currently
-being compiled, in the interests of efficiency.  (Perhaps we should
-change that decision, at least for <literal>Main</literal>.)
+<para>The <option>-fallow-incoherent-instances</option> flag implies the
+<option>-fallow-overlapping-instances</option> flag, but not vice versa.

 </para>
 </sect3>
 
 </para>
 </sect3>
 

@@ -1843,7 +1775,7 @@ but this is not:
 <programlisting>
   instance F a where ...
 </programlisting>
 <programlisting>
   instance F a where ...
 </programlisting>

-Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
+Note that instance heads may contain repeated type variables (<xref linkend="instance-heads"/>).

 For example, this is OK:
 <programlisting>
   instance Stateful (ST s) (MutVar s) where ...
 For example, this is OK:
 <programlisting>
   instance Stateful (ST s) (MutVar s) where ...

@@ -1872,60 +1804,228 @@ context reduction terminates: each reduction step removes one type
 constructor.  For example, the following would make the type checker
 loop if it wasn't excluded:
 <programlisting>
 constructor.  For example, the following would make the type checker
 loop if it wasn't excluded:
 <programlisting>

-  instance C a => C a where ...
+  instance C a => C a where ...
+</programlisting>
+There are two situations in which the rule is a bit of a pain. First,
+if one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
+
+
+<programlisting>
+  instance C a where
+    op = ... -- Default
+</programlisting>
+
+
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
+
+
+<programlisting>
+  class (C1 a, C2 a, C3 a) => C a where { }
+
+  instance (C1 a, C2 a, C3 a) => C a where { }
+</programlisting>
+
+
+This allows you to write shorter signatures:
+
+
+<programlisting>
+  f :: C a => ...
+</programlisting>
+
+
+instead of
+
+
+<programlisting>
+  f :: (C1 a, C2 a, C3 a) => ...
+</programlisting>
+
+
+Voluminous correspondence on the Haskell mailing list has convinced me
+that it's worth experimenting with more liberal rules.  If you use
+the experimental flag <option>-fallow-undecidable-instances</option>
+<indexterm><primary>-fallow-undecidable-instances
+option</primary></indexterm>, you can use arbitrary
+types in both an instance context and instance head.  Termination is ensured by having a
+fixed-depth recursion stack.  If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with <option>-fcontext-stack</option><emphasis>N</emphasis>.
+</para>
+<para>
+I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
+allowing these idioms interesting idioms.  
+</para>
+</sect3>
+
+
+</sect2>
+
+<sect2 id="type-restrictions">
+<title>Type signatures</title>
+
+<sect3><title>The context of a type signature</title>
+<para>
+Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
+the form <emphasis>(class type-variable)</emphasis> or
+<emphasis>(class (type-variable type-variable ...))</emphasis>.  Thus,
+these type signatures are perfectly OK
+<programlisting>
+  g :: Eq [a] => ...
+  g :: Ord (T a ()) => ...
+</programlisting>
+</para>
+<para>
+GHC imposes the following restrictions on the constraints in a type signature.
+Consider the type:
+
+<programlisting>
+  forall tv1..tvn (c1, ...,cn) => type
+</programlisting>
+
+(Here, we write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 98, all the free type variables of an
+explicit source-language type signature are universally quantified,
+except for the class type variables in a class declaration.  However,
+in GHC, you can give the foralls if you want.  See <xref linkend="universal-quantification"/>).
+</para>
+
+<para>
+
+<orderedlist>
+<listitem>
+
+<para>
+ <emphasis>Each universally quantified type variable
+<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
+
+A type variable <literal>a</literal> is "reachable" if it it appears
+in the same constraint as either a type variable free in in
+<literal>type</literal>, or another reachable type variable.  
+A value with a type that does not obey 
+this reachability restriction cannot be used without introducing
+ambiguity; that is why the type is rejected.
+Here, for example, is an illegal type:
+
+
+<programlisting>
+  forall a. Eq a => Int
+</programlisting>
+
+
+When a value with this type was used, the constraint <literal>Eq tv</literal>
+would be introduced where <literal>tv</literal> is a fresh type variable, and
+(in the dictionary-translation implementation) the value would be
+applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
+can never know which instance of <literal>Eq</literal> to use because we never
+get any more information about <literal>tv</literal>.
+</para>
+<para>
+Note
+that the reachability condition is weaker than saying that <literal>a</literal> is
+functionally dependent on a type variable free in
+<literal>type</literal> (see <xref
+linkend="functional-dependencies"/>).  The reason for this is there
+might be a "hidden" dependency, in a superclass perhaps.  So
+"reachable" is a conservative approximation to "functionally dependent".
+For example, consider:
+<programlisting>
+  class C a b | a -> b where ...
+  class C a b => D a b where ...
+  f :: forall a b. D a b => a -> a

 </programlisting>
 </programlisting>

-There are two situations in which the rule is a bit of a pain. First,
-if one allows overlapping instance declarations then it's quite
-convenient to have a "default instance" declaration that applies if
-something more specific does not:
+This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
+but that is not immediately apparent from <literal>f</literal>'s type.
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
+universally quantified type variables <literal>tvi</literal></emphasis>.
+
+For example, this type is OK because <literal>C a b</literal> mentions the
+universally quantified type variable <literal>b</literal>:

 
 
 <programlisting>
 
 
 <programlisting>

-  instance C a where
-    op = ... -- Default
+  forall a. C a b => burble

 </programlisting>
 
 
 </programlisting>
 
 

-Second, sometimes you might want to use the following to get the
-effect of a "class synonym":
+The next type is illegal because the constraint <literal>Eq b</literal> does not
+mention <literal>a</literal>:

 
 
 <programlisting>
 
 
 <programlisting>

-  class (C1 a, C2 a, C3 a) => C a where { }
-
-  instance (C1 a, C2 a, C3 a) => C a where { }
+  forall a. Eq b => burble

 </programlisting>
 
 
 </programlisting>
 
 

-This allows you to write shorter signatures:
-
+The reason for this restriction is milder than the other one.  The
+excluded types are never useful or necessary (because the offending
+context doesn't need to be witnessed at this point; it can be floated
+out).  Furthermore, floating them out increases sharing. Lastly,
+excluding them is a conservative choice; it leaves a patch of
+territory free in case we need it later.

 
 

-<programlisting>
-  f :: C a => ...
-</programlisting>
+</para>
+</listitem>

 
 

+</orderedlist>

 
 

-instead of
+</para>
+</sect3>

 
 

+<sect3 id="hoist">
+<title>For-all hoisting</title>
+<para>
+It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
+end of an arrow, thus:
+<programlisting>
+  type Discard a = forall b. a -> b -> a

 
 

+  g :: Int -> Discard Int
+  g x y z = x+y
+</programlisting>
+Simply expanding the type synonym would give

 <programlisting>
 <programlisting>

-  f :: (C1 a, C2 a, C3 a) => ...
+  g :: Int -> (forall b. Int -> b -> Int)
+</programlisting>
+but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
+<programlisting>
+  g :: forall b. Int -> Int -> b -> Int
+</programlisting>
+In general, the rule is this: <emphasis>to determine the type specified by any explicit
+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 a1..an. <emphasis>context2</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
+or not the <literal>forall</literal> comes from a synonym. For example, here is another
+valid way to write <literal>g</literal>'s type signature:
+<programlisting>
+  g :: Int -> Int -> forall b. b -> Int

 </programlisting>
 </programlisting>

-
-
-Voluminous correspondence on the Haskell mailing list has convinced me
-that it's worth experimenting with more liberal rules.  If you use
-the experimental flag <option>-fallow-undecidable-instances</option>
-<indexterm><primary>-fallow-undecidable-instances
-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head.  Termination is ensured by having a
-fixed-depth recursion stack.  If you exceed the stack depth you get a
-sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack</option><emphasis>N</emphasis>.

 </para>
 <para>
 </para>
 <para>

-I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
-allowing these idioms interesting idioms.  
+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>
 </sect3>
 
 </para>
 </sect3>
 

@@ -1935,7 +2035,7 @@ allowing these idioms interesting idioms.
 <sect2 id="implicit-parameters">
 <title>Implicit parameters</title>
 
 <sect2 id="implicit-parameters">
 <title>Implicit parameters</title>
 

-<para> Implicit paramters are implemented as described in 
+<para> Implicit parameters are implemented as described in 

 "Implicit parameters: dynamic scoping with static types", 
 J Lewis, MB Shields, E Meijer, J Launchbury,
 27th ACM Symposium on Principles of Programming Languages (POPL'00),
 "Implicit parameters: dynamic scoping with static types", 
 J Lewis, MB Shields, E Meijer, J Launchbury,
 27th ACM Symposium on Principles of Programming Languages (POPL'00),

@@ -2095,6 +2195,68 @@ the binding for <literal>?x</literal>, so the type of <literal>f</literal> is
 </para>
 
 </sect3>
 </para>
 
 </sect3>

+
+<sect3><title>Implicit parameters and polymorphic recursion</title>
+
+<para>
+Consider these two definitions:
+<programlisting>
+  len1 :: [a] -> Int
+  len1 xs = let ?acc = 0 in len_acc1 xs
+
+  len_acc1 [] = ?acc
+  len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
+
+  ------------
+
+  len2 :: [a] -> Int
+  len2 xs = let ?acc = 0 in len_acc2 xs
+
+  len_acc2 :: (?acc :: Int) => [a] -> Int
+  len_acc2 [] = ?acc
+  len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
+</programlisting>
+The only difference between the two groups is that in the second group
+<literal>len_acc</literal> is given a type signature.
+In the former case, <literal>len_acc1</literal> is monomorphic in its own
+right-hand side, so the implicit parameter <literal>?acc</literal> is not
+passed to the recursive call.  In the latter case, because <literal>len_acc2</literal>
+has a type signature, the recursive call is made to the
+<emphasis>polymoprhic</emphasis> version, which takes <literal>?acc</literal>
+as an implicit parameter.  So we get the following results in GHCi:
+<programlisting>
+  Prog> len1 "hello"
+  0
+  Prog> len2 "hello"
+  5
+</programlisting>
+Adding a type signature dramatically changes the result!  This is a rather
+counter-intuitive phenomenon, worth watching out for.
+</para>
+</sect3>
+
+<sect3><title>Implicit parameters and monomorphism</title>
+
+<para>GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
+Haskell Report) to implicit parameters.  For example, consider:
+<programlisting>
+ f :: Int -> Int
+  f v = let ?x = 0     in
+        let y = ?x + v in
+        let ?x = 5     in
+        y
+</programlisting>
+Since the binding for <literal>y</literal> falls under the Monomorphism
+Restriction it is not generalised, so the type of <literal>y</literal> is
+simply <literal>Int</literal>, not <literal>(?x::Int) => Int</literal>.
+Hence, <literal>(f 9)</literal> returns result <literal>9</literal>.
+If you add a type signature for <literal>y</literal>, then <literal>y</literal>
+will get type <literal>(?x::Int) => Int</literal>, so the occurrence of
+<literal>y</literal> in the body of the <literal>let</literal> will see the
+inner binding of <literal>?x</literal>, so <literal>(f 9)</literal> will return
+<literal>14</literal>.
+</para>
+</sect3>

 </sect2>
 
 <sect2 id="linear-implicit-parameters">
 </sect2>
 
 <sect2 id="linear-implicit-parameters">

@@ -2106,7 +2268,7 @@ problem that monads seem over-kill for certain sorts of problem, notably:
 </para>
 <itemizedlist>
 <listitem> <para> distributing a supply of unique names </para> </listitem>
 </para>
 <itemizedlist>
 <listitem> <para> distributing a supply of unique names </para> </listitem>

-<listitem> <para> distributing a suppply of random numbers </para> </listitem>
+<listitem> <para> distributing a supply of random numbers </para> </listitem>

 <listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
 </itemizedlist>
 
 <listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
 </itemizedlist>
 

@@ -2267,30 +2429,6 @@ and you'd be right.  That is why they are an experimental feature.
 
 </sect2>
 
 
 </sect2>
 

-<sect2 id="functional-dependencies">
-<title>Functional dependencies
-</title>
-
-<para> Functional dependencies are implemented as described by Mark 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, 
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
-.
-</para>
-<para>
-Functional dependencies are introduced by a vertical bar in the syntax of a 
-class declaration;  e.g. 
-<programlisting>
-  class (Monad m) => MonadState s m | m -> s where ...
-
-  class Foo a b c | a b -> c where ...
-</programlisting>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
-</para>
-</sect2>
-
-
-

 <sect2 id="sec-kinding">
 <title>Explicitly-kinded quantification</title>
 
 <sect2 id="sec-kinding">
 <title>Explicitly-kinded quantification</title>
 

@@ -2393,7 +2531,7 @@ is implicitly added by Haskell.
 </para>
 <para>
 The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
 </para>
 <para>
 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>
+the <literal>forall</literal> is on the left of a function arrow.  As <literal>g2</literal>

 shows, the polymorphic type on the left of the function arrow can be overloaded.
 </para>
 <para>
 shows, the polymorphic type on the left of the function arrow can be overloaded.
 </para>
 <para>

@@ -2566,7 +2704,7 @@ matching.
 <title>Type inference</title>
 
 <para>
 <title>Type inference</title>
 
 <para>

-In general, type inference for arbitrary-rank types is undecideable.
+In general, type inference for arbitrary-rank types is undecidable.

 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:
 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:

@@ -2665,22 +2803,19 @@ for rank-2 types.
 </title>
 
 <para>
 </title>
 
 <para>

-A <emphasis>pattern type signature</emphasis> can introduce a <emphasis>scoped type
-variable</emphasis>.  For example
-</para>
-
-<para>
-
+A <emphasis>lexically scoped type variable</emphasis> can be bound by:
+<itemizedlist>
+<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>A result type signature (<xref linkend="result-type-sigs"/>)</para></listitem>
+</itemizedlist>
+For example:

 <programlisting>
 f (xs::[a]) = ys ++ ys
            where
               ys :: [a]
               ys = reverse xs
 </programlisting>
 <programlisting>
 f (xs::[a]) = ys ++ ys
            where
               ys :: [a]
               ys = reverse xs
 </programlisting>

-
-</para>
-
-<para>

 The pattern <literal>(xs::[a])</literal> includes a type signature for <varname>xs</varname>.
 This brings the type variable <literal>a</literal> into scope; it scopes over
 all the patterns and right hand sides for this equation for <function>f</function>.
 The pattern <literal>(xs::[a])</literal> includes a type signature for <varname>xs</varname>.
 This brings the type variable <literal>a</literal> into scope; it scopes over
 all the patterns and right hand sides for this equation for <function>f</function>.

@@ -2688,8 +2823,6 @@ In particular, it is in scope at the type signature for <varname>y</varname>.
 </para>
 
 <para>
 </para>
 
 <para>

- Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures.  The two can be used independently or together.

 At ordinary type signatures, such as that for <varname>ys</varname>, any type variables
 mentioned in the type signature <emphasis>that are not in scope</emphasis> are
 implicitly universally quantified.  (If there are no type variables in
 At ordinary type signatures, such as that for <varname>ys</varname>, any type variables
 mentioned in the type signature <emphasis>that are not in scope</emphasis> are
 implicitly universally quantified.  (If there are no type variables in

@@ -2712,10 +2845,10 @@ So much for the basic idea.  Here are the details.
 </para>
 
 <sect3>
 </para>
 
 <sect3>

-<title>What a pattern type signature means</title>
+<title>What a scoped type variable means</title>

 <para>
 <para>

-A type variable brought into scope by a pattern type signature is simply
-the name for a type.   The restriction they express is that all occurrences
+A lexically-scoped type variable is simply
+the name for a type.   The restriction it expresses is that all occurrences

 of the same name mean the same type.  For example:
 <programlisting>
   f :: [Int] -> Int -> Int
 of the same name mean the same type.  For example:
 <programlisting>
   f :: [Int] -> Int -> Int

@@ -2885,7 +3018,33 @@ scope over the methods defined in the <literal>where</literal> part.  For exampl
 
 </sect3>
 
 
 </sect3>
 

-<sect3>
+<sect3 id="decl-type-sigs">
+<title>Declaration type signatures</title>
+<para>A declaration type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the definition of the named function(s).  For example:
+<programlisting>
+  f :: forall a. [a] -> [a]
+  f (x:xs) = xs ++ [ x :: a ]
+</programlisting>
+The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in
+the definition of "<literal>f</literal>".
+</para>
+<para>This only happens if the quantification in <literal>f</literal>'s type
+signature is explicit.  For example:
+<programlisting>
+  g :: [a] -> [a]
+  g (x:xs) = xs ++ [ x :: a ]
+</programlisting>
+This program will be rejected, because "<literal>a</literal>" does not scope
+over the definition of "<literal>f</literal>", so "<literal>x::a</literal>"
+means "<literal>x::forall a. a</literal>" by Haskell's usual implicit
+quantification rules.
+</para>
+</sect3>
+
+<sect3 id="pattern-type-sigs">

 <title>Where a pattern type signature can occur</title>
 
 <para>
 <title>Where a pattern type signature can occur</title>
 
 <para>

@@ -2895,7 +3054,7 @@ A pattern type signature can occur in any pattern.  For example:
 <listitem>
 <para>
 A pattern type signature can be on an arbitrary sub-pattern, not
 <listitem>
 <para>
 A pattern type signature can be on an arbitrary sub-pattern, not

-ust on a variable:
+just on a variable:

 
 
 <programlisting>
 
 
 <programlisting>

@@ -3002,10 +3161,12 @@ in <literal>f4</literal>'s scope.
 </listitem>
 </itemizedlist>
 </para>
 </listitem>
 </itemizedlist>
 </para>

+<para>Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures.  The two can be used independently or together.</para>

 
 </sect3>
 
 
 </sect3>
 

-<sect3>
+<sect3 id="result-type-sigs">

 <title>Result type signatures</title>
 
 <para>
 <title>Result type signatures</title>
 
 <para>

@@ -3075,9 +3236,23 @@ classes <literal>Eq</literal>, <literal>Ord</literal>,
 GHC extends this list with two more classes that may be automatically derived 
 (provided the <option>-fglasgow-exts</option> flag is specified):
 <literal>Typeable</literal>, and <literal>Data</literal>.  These classes are defined in the library
 GHC extends this list with two more classes that may be automatically derived 
 (provided the <option>-fglasgow-exts</option> flag is specified):
 <literal>Typeable</literal>, and <literal>Data</literal>.  These classes are defined in the library

-modules <literal>Data.Dynamic</literal> and <literal>Data.Generics</literal> respectively, and the
+modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively, and the

 appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
 </para>
 appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
 </para>

+<para>An instance of <literal>Typeable</literal> can only be derived if the
+data type has seven or fewer type parameters, all of kind <literal>*</literal>.
+The reason for this is that the <literal>Typeable</literal> class is derived using the scheme
+described in
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/hmap/gmap2.ps">
+Scrap More Boilerplate: Reflection, Zips, and Generalised Casts
+</ulink>.
+(Section 7.4 of the paper describes the multiple <literal>Typeable</literal> classes that
+are used, and only <literal>Typeable1</literal> up to
+<literal>Typeable7</literal> are provided in the library.)
+In other cases, there is nothing to stop the programmer writing a <literal>TypableX</literal>
+class, whose kind suits that of the data type constructor, and
+then writing the data type instance by hand.
+</para>

 </sect2>
 
 <sect2 id="newtype-deriving">
 </sect2>
 
 <sect2 id="newtype-deriving">

@@ -3190,7 +3365,7 @@ class to the new type:
 <para>
 
 As a result of this extension, all derived instances in newtype
 <para>
 
 As a result of this extension, all derived instances in newtype

-declarations are treated uniformly (and implemented just by reusing
+ 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.
 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.

@@ -3271,14 +3446,205 @@ then we would not have been able to derive an instance for the
 classes usually have one "main" parameter for which deriving new
 instances is most interesting.
 </para>
 classes usually have one "main" parameter for which deriving new
 instances is most interesting.
 </para>

+<para>Lastly, all of this applies only for classes other than
+<literal>Read</literal>, <literal>Show</literal>, <literal>Typeable</literal>, 
+and <literal>Data</literal>, for which the built-in derivation applies (section
+4.3.3. of the Haskell Report).
+(For the standard classes <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Ix</literal>, and <literal>Bounded</literal> it is immaterial whether
+the standard method is used or the one described here.)
+</para>

 </sect3>
 
 </sect2>
 
 </sect3>
 
 </sect2>
 

+<sect2 id="typing-binds">
+<title>Generalised typing of mutually recursive bindings</title>
+
+<para>
+The Haskell Report specifies that a group of bindings (at top level, or in a
+<literal>let</literal> or <literal>where</literal>) should be sorted into
+strongly-connected components, and then type-checked in dependency order
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.1">Haskell
+Report, Section 4.5.1</ulink>).  
+As each group is type-checked, any binders of the group that
+have
+an explicit type signature are put in the type environment with the specified
+polymorphic type,
+and all others are monomorphic until the group is generalised 
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.2">Haskell Report, Section 4.5.2</ulink>).
+</para>
+
+<para>Following a suggestion of Mark Jones, in his paper
+<ulink url="http://www.cse.ogi.edu/~mpj/thih/">Typing Haskell in
+Haskell</ulink>,
+GHC implements a more general scheme.  If <option>-fglasgow-exts</option> is
+specified:
+<emphasis>the dependency analysis ignores references to variables that have an explicit
+type signature</emphasis>.
+As a result of this refined dependency analysis, the dependency groups are smaller, and more bindings will
+typecheck.  For example, consider:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True || g "Yes"
+  
+  g y = (y &lt;= y) || f True
+</programlisting>
+This is rejected by Haskell 98, but under Jones's scheme the definition for
+<literal>g</literal> is typechecked first, separately from that for
+<literal>f</literal>,
+because the reference to <literal>f</literal> in <literal>g</literal>'s right
+hand side is ingored by the dependency analysis.  Then <literal>g</literal>'s
+type is generalised, to get
+<programlisting>
+  g :: Ord a =&gt; a -> Bool
+</programlisting>
+Now, the defintion for <literal>f</literal> is typechecked, with this type for
+<literal>g</literal> in the type environment.
+</para>
+
+<para>
+The same refined dependency analysis also allows the type signatures of 
+mutually-recursive functions to have different contexts, something that is illegal in
+Haskell 98 (Section 4.5.2, last sentence).  With
+<option>-fglasgow-exts</option>
+GHC only insists that the type signatures of a <emphasis>refined</emphasis> group have identical
+type signatures; in practice this means that only variables bound by the same
+pattern binding must have the same context.  For example, this is fine:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True
+  
+  g :: Ord a =&gt; a -> Bool
+  g y = (y &lt;= y) || f True
+</programlisting>
+</para>
+</sect2>

 
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
   
 
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
   

+<!-- ====================== Generalised algebraic data types =======================  -->
+
+<sect1 id="gadt">
+<title>Generalised Algebraic Data Types</title>
+
+<para>Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you
+to give the type signatures of constructors explicitly.  For example:
+<programlisting>
+  data Term a where
+      Lit    :: Int -> Term Int
+      Succ   :: Term Int -> Term Int
+      IsZero :: Term Int -> Term Bool  
+      If     :: Term Bool -> Term a -> Term a -> Term a
+      Pair   :: Term a -> Term b -> Term (a,b)
+</programlisting>
+Notice that the return type of the constructors is not always <literal>Term a</literal>, as is the
+case with ordinary vanilla data types.  Now we can write a well-typed <literal>eval</literal> function
+for these <literal>Terms</literal>:
+<programlisting>
+  eval :: Term a -> a
+  eval (Lit i)             = i
+  eval (Succ t)     = 1 + eval t
+  eval (IsZero i)   = eval i == 0
+  eval (If b e1 e2) = if eval b then eval e1 else eval e2
+  eval (Pair e1 e2) = (eval e2, eval e2)
+</programlisting>
+These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
+</para>
+<para> The extensions to GHC are these:
+<itemizedlist>
+<listitem><para>
+  Data type declarations have a 'where' form, as exemplified above.  The type signature of
+each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal
+Haskell data type declaration, the type variable(s) in the "<literal>data Term a where</literal>" header 
+have no scope.  Indeed, one can write a kind signature instead:
+<programlisting>
+  data Term :: * -> * where ...
+</programlisting>
+or even a mixture of the two:
+<programlisting>
+  data Foo a :: (* -> *) -> * where ...
+</programlisting>
+The type variables (if given) may be explicitly kinded, so we could also write the header for <literal>Foo</literal>
+like this:
+<programlisting>
+  data Foo a (b :: * -> *) where ...
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+There are no restrictions on the type of the data constructor, except that the result
+type must begin with the type constructor being defined.  For example, in the <literal>Term</literal> data
+type above, the type of each constructor must end with <literal> ... -> Term ...</literal>.
+</para></listitem>
+
+<listitem><para>
+You cannot use record syntax on a GADT-style data type declaration.  (
+It's not clear what these it would mean.  For example,
+the record selectors might ill-typed.)
+However, you can use strictness annotations, in the obvious places
+in the constructor type:
+<programlisting>
+  data Term a where
+      Lit    :: !Int -> Term Int
+      If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
+      Pair   :: Term a -> Term b -> Term (a,b)
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can use a <literal>deriving</literal> clause on a GADT-style data type
+declaration, but only if the data type could also have been declared in
+Haskell-98 syntax.   For example, these two declarations are equivalent
+<programlisting>
+  data Maybe1 a where {
+      Nothing1 :: Maybe a ;
+      Just1    :: a -> Maybe a
+    } deriving( Eq, Ord )
+
+  data Maybe2 a = Nothing2 | Just2 a 
+       deriving( Eq, Ord )
+</programlisting>
+This simply allows you to declare a vanilla Haskell-98 data type using the
+<literal>where</literal> form without losing the <literal>deriving</literal> clause.
+</para></listitem>
+
+<listitem><para>
+Pattern matching causes type refinement.  For example, in the right hand side of the equation
+<programlisting>
+  eval :: Term a -> a
+  eval (Lit i) =  ...
+</programlisting>
+the type <literal>a</literal> is refined to <literal>Int</literal>.  (That's the whole point!)
+A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper
+about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page.</para>
+
+<para> The general principle is this: <emphasis>type refinement is only carried out based on user-supplied type annotations</emphasis>.
+So if no type signature is supplied for <literal>eval</literal>, no type refinement happens, and lots of obscure error messages will
+occur.  However, the refinement is quite general.  For example, if we had:
+<programlisting>
+  eval :: Term a -> a -> a
+  eval (Lit i) j =  i+j
+</programlisting>
+the pattern match causes the type <literal>a</literal> to be refined to <literal>Int</literal> (because of the type
+of the constructor <literal>Lit</literal>, and that refinement also applies to the type of <literal>j</literal>, and
+the result type of the <literal>case</literal> expression.  Hence the addition <literal>i+j</literal> is legal.
+</para>
+</listitem>
+</itemizedlist>
+</para>
+
+<para>Notice that GADTs generalise existential types.  For example, these two declarations are equivalent:
+<programlisting>
+  data T a = forall b. MkT b (b->a)
+  data T' a where { MKT :: b -> (b->a) -> T' a }
+</programlisting>
+</para>
+</sect1>
+
+<!-- ====================== End of Generalised algebraic data types =======================  -->
+

 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">
 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">

@@ -3328,9 +3694,11 @@ Tim Sheard is going to expand it.)
                  </para>
              <para> A splice can occur in place of 
                  <itemizedlist>
                  </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> an expression; the spliced expression must
+                   have type <literal>Q Exp</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 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>
+                   <listitem><para> [Planned, but not implemented yet.] a
+                   type; the spliced expression must have type <literal>Q Typ</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>
                    </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>

@@ -3345,7 +3713,7 @@ Tim Sheard is going to expand it.)
                              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>
                              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; 
+                   <listitem><para>  [Planned, but not implemented yet.]  <literal>[t| ... |]</literal>, where the "..." is a type; 

                              the quotation has type <literal>Type</literal>.</para></listitem>
                  </itemizedlist></para></listitem>
 
                              the quotation has type <literal>Type</literal>.</para></listitem>
                  </itemizedlist></para></listitem>
 

@@ -3423,7 +3791,7 @@ module Printf where
 -- you intend to use it.
 
 -- Import some Template Haskell syntax
 -- you intend to use it.
 
 -- Import some Template Haskell syntax

-import Language.Haskell.TH.Syntax
+import Language.Haskell.TH

 
 -- Describe a format string
 data Format = D | S | L String
 
 -- Describe a format string
 data Format = D | S | L String

@@ -3591,7 +3959,7 @@ proc x -> f x -&lt;&lt; x+1
 </screen>
 which is equivalent to
 <screen>
 </screen>
 which is equivalent to
 <screen>

-arr (\ x -> (f, x+1)) >>> app
+arr (\ x -> (f x, x+1)) >>> app

 </screen>
 so in this case the arrow must belong to the <literal>ArrowApply</literal>
 class.
 </screen>
 so in this case the arrow must belong to the <literal>ArrowApply</literal>
 class.

@@ -4028,12 +4396,13 @@ can still define and use your own versions of
 </para>
 
 <para>
 </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
+GHC ignores assertions when optimisation is turned on with the
+      <option>-O</option><indexterm><primary><option>-O</option></primary></indexterm> flag.  That is, expressions of the form

 <literal>assert pred e</literal> will be rewritten to
 <literal>assert pred e</literal> will be rewritten to

-<literal>e</literal>.
-</para>
+<literal>e</literal>.  You can also disable assertions using the
+      <option>-fignore-asserts</option>
+      option<indexterm><primary><option>-fignore-asserts</option></primary>
+      </indexterm>.</para>

 
 <para>
 Assertion failures can be caught, see the documentation for the
 
 <para>
 Assertion failures can be caught, see the documentation for the

@@ -4090,14 +4459,21 @@ Assertion failures can be caught, see the documentation for the
        </listitem>
 
        <listitem>
        </listitem>
 
        <listitem>

-         <para>You can deprecate a function, class, or type, with the
+         <para>You can deprecate a function, class, type, or data constructor, with the

          following top-level declaration:</para>
 <programlisting>
    {-# DEPRECATED f, C, T "Don't use these" #-}
 </programlisting>
          <para>When you compile any module that imports and uses any
          following top-level declaration:</para>
 <programlisting>
    {-# DEPRECATED f, C, T "Don't use these" #-}
 </programlisting>
          <para>When you compile any module that imports and uses any

-          of the specifed entities, GHC will print the specified
+          of the specified entities, GHC will print the specified

           message.</para>
           message.</para>

+         <para> You can only depecate entities declared at top level in the module
+         being compiled, and you can only use unqualified names in the list of
+         entities being deprecated.  A capitalised name, such as <literal>T</literal>
+         refers to <emphasis>either</emphasis> the type constructor <literal>T</literal>
+         <emphasis>or</emphasis> the data constructor <literal>T</literal>, or both if
+         both are in scope.  If both are in scope, there is currently no way to deprecate 
+         one without the other (c.f. fixities <xref linkend="infix-tycons"/>).</para>

        </listitem>
       </itemizedlist>
       Any use of the deprecated item, or of anything from a deprecated
        </listitem>
       </itemizedlist>
       Any use of the deprecated item, or of anything from a deprecated

@@ -4113,6 +4489,31 @@ Assertion failures can be caught, see the documentation for the
       <option>-fno-warn-deprecations</option>.</para>
     </sect2>
 
       <option>-fno-warn-deprecations</option>.</para>
     </sect2>
 

+    <sect2 id="include-pragma">
+      <title>INCLUDE pragma</title>
+
+      <para>The <literal>INCLUDE</literal> pragma is for specifying the names
+       of C header files that should be <literal>#include</literal>'d into
+       the C source code generated by the compiler for the current module (if
+       compiling via C).  For example:</para>
+
+<programlisting>
+{-# INCLUDE "foo.h" #-}
+{-# INCLUDE &lt;stdio.h&gt; #-}</programlisting>
+
+      <para>The <literal>INCLUDE</literal> pragma(s) must appear at the top of
+       your source file with any <literal>OPTIONS_GHC</literal>
+       pragma(s).</para>
+
+      <para>An <literal>INCLUDE</literal> pragma is  the preferred alternative
+       to the <option>-#include</option> option (<xref
+         linkend="options-C-compiler" />), because the
+       <literal>INCLUDE</literal> pragma is understood by other
+       compilers.  Yet another alternative is to add the include file to each
+       <literal>foreign import</literal> declaration in your code, but we
+       don't recommend using this approach with GHC.</para>
+    </sect2>
+

     <sect2 id="inline-noinline-pragma">
       <title>INLINE and NOINLINE pragmas</title>
 
     <sect2 id="inline-noinline-pragma">
       <title>INLINE and NOINLINE pragmas</title>
 

@@ -4152,7 +4553,7 @@ key_function :: Int -> String -> (Bool, Double)
         The normal unfolding machinery will then be very keen to
         inline it.</para>
 
         The normal unfolding machinery will then be very keen to
         inline it.</para>
 

-       <para>Syntactially, an <literal>INLINE</literal> pragma for a
+       <para>Syntactically, an <literal>INLINE</literal> pragma for a

         function can be put anywhere its type signature could be
         put.</para>
 
         function can be put anywhere its type signature could be
         put.</para>
 

@@ -4186,7 +4587,7 @@ key_function :: Int -> String -> (Bool, Double)
         you're very cautious about code size.</para>
 
        <para><literal>NOTINLINE</literal> is a synonym for
         you're very cautious about code size.</para>
 
        <para><literal>NOTINLINE</literal> is a synonym for

-        <literal>NOINLINE</literal> (<literal>NOTINLINE</literal> is
+        <literal>NOINLINE</literal> (<literal>NOINLINE</literal> is

         specified by Haskell 98 as the standard way to disable
         inlining, so it should be used if you want your code to be
         portable).</para>
         specified by Haskell 98 as the standard way to disable
         inlining, so it should be used if you want your code to be
         portable).</para>

@@ -4202,7 +4603,7 @@ key_function :: Int -> String -> (Bool, Double)
         number</emphasis>; the phase number decreases towards zero.
         If you use <option>-dverbose-core2core</option> you'll see the
         sequence of phase numbers for successive runs of the
         number</emphasis>; the phase number decreases towards zero.
         If you use <option>-dverbose-core2core</option> you'll see the
         sequence of phase numbers for successive runs of the

-        simpifier.  In an INLINE pragma you can optionally specify a
+        simplifier.  In an INLINE pragma you can optionally specify a

         phase number, thus:</para>
 
        <itemizedlist>
         phase number, thus:</para>
 
        <itemizedlist>

@@ -4264,6 +4665,29 @@ key_function :: Int -> String -> (Bool, Double)
       </sect3>
     </sect2>
 
       </sect3>
     </sect2>
 

+    <sect2 id="language-pragma">
+      <title>LANGUAGE pragma</title>
+
+      <indexterm><primary>LANGUAGE</primary><secondary>pragma</secondary></indexterm>
+      <indexterm><primary>pragma</primary><secondary>LANGUAGE</secondary></indexterm>
+
+      <para>This allows language extensions to be enabled in a portable way.
+       It is the intention that all Haskell compilers support the
+       <literal>LANGUAGE</literal> pragma with the same syntax, although not
+       all extensions are supported by all compilers, of
+       course.  The <literal>LANGUAGE</literal> pragma should be used instead
+       of <literal>OPTIONS_GHC</literal>, if possible.</para>
+
+      <para>For example, to enable the FFI and preprocessing with CPP:</para>
+
+<programlisting>{-# LANGUAGE ForeignFunctionInterface, CPP #-}</programlisting>
+
+      <para>Any extension from the <literal>Extension</literal> type defined in
+       <ulink
+         url="../libraries/Cabal/Language-Haskell-Extension.html"><literal>Language.Haskell.Extension</literal></ulink> may be used.  GHC will report an error if any of the requested extensions are not supported.</para>
+    </sect2>
+
+

     <sect2 id="line-pragma">
       <title>LINE pragma</title>
 
     <sect2 id="line-pragma">
       <title>LINE pragma</title>
 

@@ -4274,9 +4698,7 @@ key_function :: Int -> String -> (Bool, Double)
       code.  It lets you specify the line number and filename of the
       original code; for example</para>
 
       code.  It lets you specify the line number and filename of the
       original code; for example</para>
 

-<programlisting>
-{-# LINE 42 "Foo.vhs" #-}
-</programlisting>
+<programlisting>{-# LINE 42 "Foo.vhs" #-}</programlisting>

 
       <para>if you'd generated the current file from something called
       <filename>Foo.vhs</filename> and this line corresponds to line
 
       <para>if you'd generated the current file from something called
       <filename>Foo.vhs</filename> and this line corresponds to line

@@ -4286,16 +4708,19 @@ key_function :: Int -> String -> (Bool, Double)
     </sect2>
 
     <sect2 id="options-pragma">
     </sect2>
 
     <sect2 id="options-pragma">

-      <title>OPTIONS pragma</title>
-      <indexterm><primary>OPTIONS</primary>
+      <title>OPTIONS_GHC pragma</title>
+      <indexterm><primary>OPTIONS_GHC</primary>

       </indexterm>
       </indexterm>

-      <indexterm><primary>pragma</primary><secondary>OPTIONS</secondary>
+      <indexterm><primary>pragma</primary><secondary>OPTIONS_GHC</secondary>

       </indexterm>
 
       </indexterm>
 

-      <para>The <literal>OPTIONS</literal> pragma is used to specify
+      <para>The <literal>OPTIONS_GHC</literal> pragma is used to specify

       additional options that are given to the compiler when compiling
       this source file.  See <xref linkend="source-file-options"/> for
       details.</para>
       additional options that are given to the compiler when compiling
       this source file.  See <xref linkend="source-file-options"/> for
       details.</para>

+
+      <para>Previous versions of GHC accepted <literal>OPTIONS</literal> rather
+       than <literal>OPTIONS_GHC</literal>, but that is now deprecated.</para>

     </sect2>
 
     <sect2 id="rules">
     </sect2>
 
     <sect2 id="rules">

@@ -4318,7 +4743,7 @@ key_function :: Int -> String -> (Bool, Double)
       overloaded function:</para>
 
 <programlisting>
       overloaded function:</para>
 
 <programlisting>

-hammeredLookup :: Ord key => [(key, value)] -> key -> value
+  hammeredLookup :: Ord key => [(key, value)] -> key -> value

 </programlisting>
 
       <para>If it is heavily used on lists with
 </programlisting>
 
       <para>If it is heavily used on lists with

@@ -4326,7 +4751,7 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       follows:</para>
 
 <programlisting>
       follows:</para>
 
 <programlisting>

-{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+  {-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}

 </programlisting>
 
       <para>A <literal>SPECIALIZE</literal> pragma for a function can
 </programlisting>
 
       <para>A <literal>SPECIALIZE</literal> pragma for a function can

@@ -4337,7 +4762,35 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       (see <xref linkend="rewrite-rules"/>) that rewrites a call to the
       un-specialised function into a call to the specialised one.</para>
 
       (see <xref linkend="rewrite-rules"/>) that rewrites a call to the
       un-specialised function into a call to the specialised one.</para>
 

-      <para>In earlier versions of GHC, it was possible to provide your own
+      <para>The type in a SPECIALIZE pragma can be any type that is less
+       polymorphic than the type of the original function.  In concrete terms,
+       if the original function is <literal>f</literal> then the pragma
+<programlisting>
+  {-# SPECIALIZE f :: &lt;type&gt; #-}
+</programlisting>
+      is valid if and only if the defintion
+<programlisting>
+  f_spec :: &lt;type&gt;
+  f_spec = f
+</programlisting>
+      is valid.  Here are some examples (where we only give the type signature
+      for the original function, not its code):
+<programlisting>
+  f :: Eq a => a -> b -> b
+  {-# SPECIALISE g :: Int -> b -> b #-}
+
+  g :: (Eq a, Ix b) => a -> b -> b
+  {-# SPECIALISE g :: (Eq a) => a -> Int -> Int #-}
+
+  h :: Eq a => a -> a -> a
+  {-# SPECIALISE h :: (Eq a) => [a] -> [a] -> [a] #-}
+</programlisting>  
+The last of these examples will generate a 
+RULE with a somewhat-complex left-hand side (try it yourself), so it might not fire very
+well.  If you use this kind of specialisation, let us know how well it works.
+</para>
+
+      <para>Note: In earlier versions of GHC, it was possible to provide your own

       specialised function for a given type:
 
 <programlisting>
       specialised function for a given type:
 
 <programlisting>

@@ -4447,7 +4900,7 @@ data S = S {-# UNPACK #-} !Int {-# UNPACK #-} !Int
 <sect1 id="rewrite-rules">
 <title>Rewrite rules
 
 <sect1 id="rewrite-rules">
 <title>Rewrite rules
 

-<indexterm><primary>RULES pagma</primary></indexterm>
+<indexterm><primary>RULES pragma</primary></indexterm>

 <indexterm><primary>pragma, RULES</primary></indexterm>
 <indexterm><primary>rewrite rules</primary></indexterm></title>
 
 <indexterm><primary>pragma, RULES</primary></indexterm>
 <indexterm><primary>rewrite rules</primary></indexterm></title>
 

@@ -4613,7 +5066,7 @@ same type.
 
 <para>
  GHC makes absolutely no attempt to verify that the LHS and RHS
 
 <para>
  GHC makes absolutely no attempt to verify that the LHS and RHS

-of a rule have the same meaning.  That is undecideable in general, and
+of a rule have the same meaning.  That is undecidable in general, and

 infeasible in most interesting cases.  The responsibility is entirely the programmer's!
 
 </para>
 infeasible in most interesting cases.  The responsibility is entirely the programmer's!
 
 </para>

@@ -4645,7 +5098,7 @@ This rule will cause the compiler to go into an infinite loop.
 for matching a rule LHS with an expression.  It seeks a substitution
 which makes the LHS and expression syntactically equal modulo alpha
 conversion.  The pattern (rule), but not the expression, is eta-expanded if
 for matching a rule LHS with an expression.  It seeks a substitution
 which makes the LHS and expression syntactically equal modulo alpha
 conversion.  The pattern (rule), but not the expression, is eta-expanded if

-necessary.  (Eta-expanding the epression can lead to laziness bugs.)
+necessary.  (Eta-expanding the expression can lead to laziness bugs.)

 But not beta conversion (that's called higher-order matching).
 </para>
 
 But not beta conversion (that's called higher-order matching).
 </para>
 

@@ -5011,7 +5464,7 @@ If you add <option>-dppr-debug</option> you get a more detailed listing.
 <listitem>
 
 <para>
 <listitem>
 
 <para>

- The defintion of (say) <function>build</function> in <filename>GHC/Base.lhs</filename> looks llike this:
+ The definition of (say) <function>build</function> in <filename>GHC/Base.lhs</filename> looks llike this:

 
 <programlisting>
         build   :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
 
 <programlisting>
         build   :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]

@@ -5060,7 +5513,7 @@ program even if fusion doesn't happen.  More rules in <filename>GHC/List.lhs</fi
 f x = ({-# CORE "foo" #-} show) ({-# CORE "bar" #-} x)
 </programlisting>
 
 f x = ({-# CORE "foo" #-} show) ({-# CORE "bar" #-} x)
 </programlisting>
 

-  Sematically, this is equivalent to:
+  Semantically, this is equivalent to:

 
 <programlisting>
 g x = show x
 
 <programlisting>
 g x = show x