remove unused primitives.xml
[ghc-hetmet.git] / docs / users_guide / glasgow_exts.xml
index f803f6d..4ed8c2a 100644 (file)
@@ -106,9 +106,7 @@ documentation</ulink> describes all the libraries that come with GHC.
         </term>
        <listitem>
          <para>This option enables the language extension defined in the
-         Haskell 98 Foreign Function Interface Addendum plus deprecated
-         syntax of previous versions of the FFI for backwards
-         compatibility.</para> 
+         Haskell 98 Foreign Function Interface Addendum.</para>
 
          <para>New reserved words: <literal>foreign</literal>.</para>
        </listitem>
@@ -116,11 +114,22 @@ documentation</ulink> describes all the libraries that come with GHC.
 
       <varlistentry>
        <term>
-          <option>-fno-monomorphism-restriction</option>:
-          <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
+          <option>-fno-monomorphism-restriction</option>,<option>-fno-mono-pat-binds</option>:
+        </term>
+       <listitem>
+         <para> These two flags control how generalisation is done.
+           See <xref linkend="monomorphism"/>.
+          </para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+          <option>-fextended-default-rules</option>:
+          <indexterm><primary><option>-fextended-default-rules</option></primary></indexterm>
         </term>
        <listitem>
-         <para> Switch off the Haskell 98 monomorphism restriction.
+         <para> Use GHCi's extended default rules in a regular module (<xref linkend="extended-default-rules"/>).
           Independent of the <option>-fglasgow-exts</option>
           flag. </para>
        </listitem>
@@ -232,6 +241,14 @@ documentation</ulink> describes all the libraries that come with GHC.
       </varlistentry>
 
       <varlistentry>
+       <term><option>-foverloaded-strings</option></term>
+       <listitem>
+         <para>Enables overloaded string literals (see <xref
+         linkend="overloaded-strings"/>).</para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
        <term><option>-fscoped-type-variables</option></term>
        <listitem>
          <para>Enables lexically-scoped type variables (see <xref
@@ -260,8 +277,6 @@ documentation</ulink> describes all the libraries that come with GHC.
   </sect1>
 
 <!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
-<!--    included from primitives.sgml  -->
-<!-- &primitives; -->
 <sect1 id="primitives">
   <title>Unboxed types and primitive operations</title>
 
@@ -535,14 +550,11 @@ import qualified Control.Monad.ST.Strict as ST
       linkend="search-path"/>.</para>
 
       <para>GHC comes with a large collection of libraries arranged
-      hierarchically; see the accompanying library documentation.
-      There is an ongoing project to create and maintain a stable set
-      of <quote>core</quote> libraries used by several Haskell
-      compilers, and the libraries that GHC comes with represent the
-      current status of that project.  For more details, see <ulink
-      url="http://www.haskell.org/~simonmar/libraries/libraries.html">Haskell
-      Libraries</ulink>.</para>
-
+      hierarchically; see the accompanying <ulink
+      url="../libraries/index.html">library
+      documentation</ulink>.  More libraries to install are available
+      from <ulink
+      url="http://hackage.haskell.org/packages/hackage.html">HackageDB</ulink>.</para>
     </sect2>
 
     <!-- ====================== PATTERN GUARDS =======================  -->
@@ -611,7 +623,7 @@ to write clunky would be to use case expressions:
 </para>
 
 <programlisting>
-clunky env var1 var1 = case lookup env var1 of
+clunky env var1 var2 = case lookup env var1 of
   Nothing -&gt; fail
   Just val1 -&gt; case lookup env var2 of
     Nothing -&gt; fail
@@ -636,7 +648,7 @@ Here is how I would write clunky:
 </para>
 
 <programlisting>
-clunky env var1 var1
+clunky env var1 var2
   | Just val1 &lt;- lookup env var1
   , Just val2 &lt;- lookup env var2
   = val1 + val2
@@ -894,18 +906,46 @@ fromInteger :: Integer -> Bool -> Bool
             you should be all right.</para>
 
 </sect2>
-</sect1>
 
+<sect2 id="postfix-operators">
+<title>Postfix operators</title>
 
-<!-- TYPE SYSTEM EXTENSIONS -->
-<sect1 id="type-extensions">
-<title>Type system extensions</title>
+<para>
+GHC allows a small extension to the syntax of left operator sections, which
+allows you to define postfix operators.  The extension is this:  the left section
+<programlisting>
+  (e !)
+</programlisting> 
+is equivalent (from the point of view of both type checking and execution) to the expression
+<programlisting>
+  ((!) e)
+</programlisting> 
+(for any expression <literal>e</literal> and operator <literal>(!)</literal>.
+The strict Haskell 98 interpretation is that the section is equivalent to
+<programlisting>
+  (\y -> (!) e y)
+</programlisting> 
+That is, the operator must be a function of two arguments.  GHC allows it to
+take only one argument, and that in turn allows you to write the function
+postfix.
+</para>
+<para>Since this extension goes beyond Haskell 98, it should really be enabled
+by a flag; but in fact it is enabled all the time.  (No Haskell 98 programs
+change their behaviour, of course.)
+</para>
+<para>The extension does not extend to the left-hand side of function
+definitions; you must define such a function in prefix form.</para>
 
+</sect2>
 
-<sect2>
-<title>Data types and type synonyms</title>
+</sect1>
 
-<sect3 id="nullary-types">
+
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="data-type-extensions">
+<title>Extensions to data types and type synonyms</title>
+
+<sect2 id="nullary-types">
 <title>Data types with no constructors</title>
 
 <para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
@@ -919,13 +959,13 @@ a data type with no constructors.  For example:</para>
 <para>Syntactically, the declaration lacks the "= constrs" part.  The 
 type can be parameterised over types of any kind, but if the kind is
 not <literal>*</literal> then an explicit kind annotation must be used
-(see <xref linkend="sec-kinding"/>).</para>
+(see <xref linkend="kinding"/>).</para>
 
 <para>Such data types have only one value, namely bottom.
 Nevertheless, they can be useful when defining "phantom types".</para>
-</sect3>
+</sect2>
 
-<sect3 id="infix-tycons">
+<sect2 id="infix-tycons">
 <title>Infix type constructors, classes, and type variables</title>
 
 <para>
@@ -992,9 +1032,9 @@ to be written infix, very much like expressions.  More specifically:
 
 </itemizedlist>
 </para>
-</sect3>
+</sect2>
 
-<sect3 id="type-synonyms">
+<sect2 id="type-synonyms">
 <title>Liberalised type synonyms</title>
 
 <para>
@@ -1084,10 +1124,10 @@ this will be rejected:
 </programlisting>
 because GHC does not allow  unboxed tuples on the left of a function arrow.
 </para>
-</sect3>
+</sect2>
 
 
-<sect3 id="existential-quantification">
+<sect2 id="existential-quantification">
 <title>Existentially quantified data constructors
 </title>
 
@@ -1181,7 +1221,7 @@ that collection of packages in a uniform manner.  You can express
 quite a bit of object-oriented-like programming this way.
 </para>
 
-<sect4 id="existential">
+<sect3 id="existential">
 <title>Why existential?
 </title>
 
@@ -1204,9 +1244,9 @@ But Haskell programmers can safely think of the ordinary
 adding a new existential quantification construct.
 </para>
 
-</sect4>
+</sect3>
 
-<sect4>
+<sect3>
 <title>Type classes</title>
 
 <para>
@@ -1266,9 +1306,9 @@ Notice the way that the syntax fits smoothly with that used for
 universal quantification earlier.
 </para>
 
-</sect4>
+</sect3>
 
-<sect4>
+<sect3 id="existential-records">
 <title>Record Constructors</title>
 
 <para>
@@ -1285,7 +1325,7 @@ data Counter a = forall self. NewCounter
 Here <literal>tag</literal> is a public field, with a well-typed selector
 function <literal>tag :: Counter a -> a</literal>.  The <literal>self</literal>
 type is hidden from the outside; any attempt to apply <literal>_this</literal>,
-<literal>_inc</literal> or <literal>_output</literal> as functions will raise a
+<literal>_inc</literal> or <literal>_display</literal> as functions will raise a
 compile-time error.  In other words, <emphasis>GHC defines a record selector function
 only for fields whose type does not mention the existentially-quantified variables</emphasis>.
 (This example used an underscore in the fields for which record selectors
@@ -1320,20 +1360,6 @@ main = do
     display (inc (inc counterB))   -- prints "##"
 </programlisting>
 
-In GADT declarations (see <xref linkend="gadt"/>), the explicit
-<literal>forall</literal> may be omitted.  For example, we can express
-the same <literal>Counter a</literal> using GADT:
-
-<programlisting>
-data Counter a where
-    NewCounter { _this    :: self
-               , _inc     :: self -> self
-               , _display :: self -> IO ()
-               , tag      :: a
-               }
-        :: Counter a
-</programlisting>
-
 At the moment, record update syntax is only supported for Haskell 98 data types,
 so the following function does <emphasis>not</emphasis> work:
 
@@ -1345,10 +1371,10 @@ setTag obj t = obj{ tag = t }
 
 </para>
 
-</sect4>
+</sect3>
 
 
-<sect4>
+<sect3>
 <title>Restrictions</title>
 
 <para>
@@ -1474,7 +1500,7 @@ are convincing reasons to change it.
  You can't use <literal>deriving</literal> to define instances of a
 data type with existentially quantified data constructors.
 
-Reason: in most cases it would not make sense. For example:&num;
+Reason: in most cases it would not make sense. For example:;
 
 <programlisting>
 data T = forall a. MkT [a] deriving( Eq )
@@ -1499,198 +1525,767 @@ declarations.  Define your own instances!
 
 </para>
 
-</sect4>
 </sect3>
-
 </sect2>
 
+<!-- ====================== Generalised algebraic data types =======================  -->
 
+<sect2 id="gadt-style">
+<title>Declaring data types with explicit constructor signatures</title>
 
-<sect2 id="multi-param-type-classes">
-<title>Class declarations</title>
-
-<para>
-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>
-All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
-</para>
-
-<sect3>
-<title>Multi-parameter type classes</title>
-<para>
-Multi-parameter type classes are permitted. For example:
-
-
+<para>GHC allows you to declare an algebraic data type by 
+giving the type signatures of constructors explicitly.  For example:
 <programlisting>
-  class Collection c a where
-    union :: c a -> c a -> c a
-    ...etc.
+  data Maybe a where
+      Nothing :: Maybe a
+      Just    :: a -> Maybe a
 </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:
-
-
+The form is called a "GADT-style declaration"
+because Generalised Algebraic Data Types, described in <xref linkend="gadt"/>, 
+can only be declared using this form.</para>
+<para>Notice that GADT-style syntax generalises existential types (<xref linkend="existential-quantification"/>).  
+For example, these two declarations are equivalent:
 <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
+  data Foo = forall a. MkFoo a (a -> Bool)
+  data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
 </programlisting>
-
-
 </para>
-<para>
-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:
-
-
+<para>Any data type that can be declared in standard Haskell-98 syntax 
+can also be declared using GADT-style syntax.
+The choice is largely stylistic, but GADT-style declarations differ in one important respect:
+they treat class constraints on the data constructors differently.
+Specifically, if the constructor is given a type-class context, that
+context is made available by pattern matching.  For example:
 <programlisting>
-  class C a where {
-    op :: D b => a -> b -> b
-  }
+  data Set a where
+    MkSet :: Eq a => [a] -> Set a
 
-  class C a => D a where { ... }
-</programlisting>
+  makeSet :: Eq a => [a] -> Set a
+  makeSet xs = MkSet (nub xs)
 
-
-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>.)
+  insert :: a -> Set a -> Set a
+  insert a (MkSet as) | a `elem` as = MkSet as
+                      | otherwise   = MkSet (a:as)
+</programlisting>
+A use of <literal>MkSet</literal> as a constructor (e.g. in the definition of <literal>makeSet</literal>) 
+gives rise to a <literal>(Eq a)</literal>
+constraint, as you would expect.  The new feature is that pattern-matching on <literal>MkSet</literal>
+(as in the definition of <literal>insert</literal>) makes <emphasis>available</emphasis> an <literal>(Eq a)</literal>
+context.  In implementation terms, the <literal>MkSet</literal> constructor has a hidden field that stores
+the <literal>(Eq a)</literal> dictionary that is passed to <literal>MkSet</literal>; so
+when pattern-matching that dictionary becomes available for the right-hand side of the match.
+In the example, the equality dictionary is used to satisfy the equality constraint 
+generated by the call to <literal>elem</literal>, so that the type of
+<literal>insert</literal> itself has no <literal>Eq</literal> constraint.
 </para>
-</sect3>
-
-
-
-
-<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:
+<para>This behaviour contrasts with Haskell 98's peculiar treament of 
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
+In Haskell 98 the defintion
 <programlisting>
-  class Seq s a where
-    fromList :: [a] -> s a
-    elem     :: Eq a => a -> s a -> Bool
+  data Eq a => Set' a = MkSet' [a]
 </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>
-
-
-</sect3>
-</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>
+gives <literal>MkSet'</literal> the same type as <literal>MkSet</literal> above.  But instead of 
+<emphasis>making available</emphasis> an <literal>(Eq a)</literal> constraint, pattern-matching
+on <literal>MkSet'</literal> <emphasis>requires</emphasis> an <literal>(Eq a)</literal> constraint!
+GHC faithfully implements this behaviour, odd though it is.  But for GADT-style declarations,
+GHC's behaviour is much more useful, as well as much more intuitive.</para>
 <para>
-Functional dependencies are introduced by a vertical bar in the syntax of a 
-class declaration;  e.g. 
+For example, a possible application of GHC's behaviour is to reify dictionaries:
 <programlisting>
-  class (Monad m) => MonadState s m | m -> s where ...
+   data NumInst a where
+     MkNumInst :: Num a => NumInst a
 
-  class Foo a b c | a b -> c where ...
+   intInst :: NumInst Int
+   intInst = MkNumInst
+
+   plus :: NumInst a -> a -> a -> a
+   plus MkNumInst p q = p + q
 </programlisting>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
+Here, a value of type <literal>NumInst a</literal> is equivalent 
+to an explicit <literal>(Num a)</literal> dictionary.
 </para>
 
-<sect3><title>Rules for functional dependencies </title>
 <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:
+The rest of this section gives further details about GADT-style data
+type declarations.
+
+<itemizedlist>
+<listitem><para>
+The result type of each data constructor must begin with the type constructor being defined.
+If the result type of all constructors 
+has the form <literal>T a1 ... an</literal>, where <literal>a1 ... an</literal>
+are distinct type variables, then the data type is <emphasis>ordinary</emphasis>;
+otherwise is a <emphasis>generalised</emphasis> data type (<xref linkend="gadt"/>).
+</para></listitem>
 
+<listitem><para>
+The type signature of
+each constructor is independent, and is implicitly universally quantified as usual. 
+Different constructors may have different universally-quantified type variables
+and different type-class constraints.  
+For example, this is fine:
 <programlisting>
-  class Coll s a where
-    empty  :: s
-    insert :: s -> a -> s
+  data T a where
+    T1 :: Eq b => b -> T b
+    T2 :: (Show c, Ix c) => c -> [c] -> T c
 </programlisting>
+</para></listitem>
 
-is not OK, because the type of <literal>empty</literal> doesn't mention
-<literal>a</literal>.  Functional dependencies can make the type variable
-reachable:
+<listitem><para>
+Unlike a Haskell-98-style 
+data type declaration, the type variable(s) in the "<literal>data Set a where</literal>" header 
+have no scope.  Indeed, one can write a kind signature instead:
 <programlisting>
-  class Coll s a | s -> a where
-    empty  :: s
-    insert :: s -> a -> s
+  data Set :: * -> * 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>
 
-Alternatively <literal>Coll</literal> might be rewritten
 
+<listitem><para>
+You can use strictness annotations, in the obvious places
+in the constructor type:
 <programlisting>
-  class Coll s a where
-    empty  :: s a
-    insert :: s a -> a -> s a
+  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.   For example, these two declarations are equivalent
+<programlisting>
+  data Maybe1 a where {
+      Nothing1 :: Maybe1 a ;
+      Just1    :: a -> Maybe1 a
+    } deriving( Eq, Ord )
 
-which makes the connection between the type of a collection of
-<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
-Occasionally this really doesn't work, in which case you can split the
-class like this:
+  data Maybe2 a = Nothing2 | Just2 a 
+       deriving( Eq, Ord )
+</programlisting>
+</para></listitem>
 
+<listitem><para>
+You can use record syntax on a GADT-style data type declaration:
 
 <programlisting>
-  class CollE s where
-    empty  :: s
-
-  class CollE s => Coll s a where
-    insert :: s -> a -> s
+  data Person where
+      Adult { name :: String, children :: [Person] } :: Person
+      Child { name :: String } :: Person
 </programlisting>
+As usual, for every constructor that has a field <literal>f</literal>, the type of
+field <literal>f</literal> must be the same (modulo alpha conversion).
 </para>
-</sect3>
-
+<para>
+At the moment, record updates are not yet possible with GADT-style declarations, 
+so support is limited to record construction, selection and pattern matching.
+For exmaple
+<programlisting>
+  aPerson = Adult { name = "Fred", children = [] }
 
-<sect3>
-<title>Background on functional dependencies</title>
+  shortName :: Person -> Bool
+  hasChildren (Adult { children = kids }) = not (null kids)
+  hasChildren (Child {})                  = False
+</programlisting>
+</para></listitem>
 
-<para>The following description of the motivation and use of functional dependencies is taken
-from the Hugs user manual, reproduced here (with minor changes) by kind
-permission of Mark Jones.
-</para>
-<para> 
-Consider the following class, intended as part of a
-library for collection types:
+<listitem><para> 
+As in the case of existentials declared using the Haskell-98-like record syntax 
+(<xref linkend="existential-records"/>),
+record-selector functions are generated only for those fields that have well-typed
+selectors.  
+Here is the example of that section, in GADT-style syntax:
 <programlisting>
-   class Collects e ce where
-       empty  :: ce
-       insert :: e -> ce -> ce
-       member :: e -> ce -> Bool
+data Counter a where
+    NewCounter { _this    :: self
+               , _inc     :: self -> self
+               , _display :: self -> IO ()
+               , tag      :: a
+               }
+        :: Counter a
 </programlisting>
-The type variable e used here represents the element type, while ce is the type
-of the container itself. Within this framework, we might want to define
-instances of this class for lists or characteristic functions (both of which
-can be used to represent collections of any equality type), bit sets (which can
-be used to represent collections of characters), or hash tables (which can be
-used to represent any collection whose elements have a hash function). Omitting
-standard implementation details, this would lead to the following declarations: 
+As before, only one selector function is generated here, that for <literal>tag</literal>.
+Nevertheless, you can still use all the field names in pattern matching and record construction.
+</para></listitem>
+</itemizedlist></para>
+</sect2>
+
+<sect2 id="gadt">
+<title>Generalised Algebraic Data Types (GADTs)</title>
+
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types 
+by allowing constructors to have richer return types.  Here is an 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 data types.  This generality allows us to 
+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 t)   = eval t == 0
+  eval (If b e1 e2) = if eval b then eval e1 else eval e2
+  eval (Pair e1 e2) = (eval e1, eval e2)
+</programlisting>
+The key point about GADTs is that <emphasis>pattern matching causes type refinement</emphasis>.  
+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 the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+(ICFP 2006).
+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>
+<para>
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.
+</para>
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs. 
+<itemizedlist>
+<listitem><para>
+A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>); 
+the old Haskell-98 syntax for data declarations always declares an ordinary data type.
+The result type of each constructor must begin with the type constructor being defined,
+but for a GADT the arguments to the type constructor can be arbitrary monotypes.  
+For example, in the <literal>Term</literal> data
+type above, the type of each constructor must end with <literal>Term ty</literal>, but
+the <literal>ty</literal> may not be a type variable (e.g. the <literal>Lit</literal>
+constructor).
+</para></listitem>
+
+<listitem><para>
+You cannot use a <literal>deriving</literal> clause for a GADT; only for
+an ordianary data type.
+</para></listitem>
+
+<listitem><para>
+As mentioned in <xref linkend="gadt-style"/>, record syntax is supported.
+For example:
+<programlisting>
+  data Term a where
+      Lit    { val  :: Int }      :: Term Int
+      Succ   { num  :: Term Int } :: Term Int
+      Pred   { num  :: Term Int } :: Term Int
+      IsZero { arg  :: Term Int } :: Term Bool 
+      Pair   { arg1 :: Term a
+             , arg2 :: Term b
+             }                    :: Term (a,b)
+      If     { cnd  :: Term Bool
+             , tru  :: Term a
+             , fls  :: Term a
+             }                    :: Term a
+</programlisting>
+However, for GADTs there is the following additional constraint: 
+every constructor that has a field <literal>f</literal> must have
+the same result type (modulo alpha conversion)
+Hence, in the above example, we cannot merge the <literal>num</literal> 
+and <literal>arg</literal> fields above into a 
+single name.  Although their field types are both <literal>Term Int</literal>,
+their selector functions actually have different types:
+
+<programlisting>
+  num :: Term Int -> Term Int
+  arg :: Term Bool -> Term Int
+</programlisting>
+</para></listitem>
+
+</itemizedlist>
+</para>
+
+</sect2>
+
+<!-- ====================== End of Generalised algebraic data types =======================  -->
+
+
+<sect2 id="deriving-typeable">
+<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
+
+<para>
+Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type 
+declaration, to generate a standard instance declaration for classes specified in the <literal>deriving</literal> clause.  
+In Haskell 98, the only classes that may appear in the <literal>deriving</literal> clause are the standard
+classes <literal>Eq</literal>, <literal>Ord</literal>, 
+<literal>Enum</literal>, <literal>Ix</literal>, <literal>Bounded</literal>, <literal>Read</literal>, and <literal>Show</literal>.
+</para>
+<para>
+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.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>
+<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">
+<title>Generalised derived instances for newtypes</title>
+
+<para>
+When you define an abstract type using <literal>newtype</literal>, you may want
+the new type to inherit some instances from its representation. In
+Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
+other classes you have to write an explicit instance declaration. For
+example, if you define
+
+<programlisting> 
+  newtype Dollars = Dollars Int 
+</programlisting> 
+
+and you want to use arithmetic on <literal>Dollars</literal>, you have to
+explicitly define an instance of <literal>Num</literal>:
+
+<programlisting> 
+  instance Num Dollars where
+    Dollars a + Dollars b = Dollars (a+b)
+    ...
+</programlisting>
+All the instance does is apply and remove the <literal>newtype</literal>
+constructor. It is particularly galling that, since the constructor
+doesn't appear at run-time, this instance declaration defines a
+dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
+dictionary, only slower!
+</para>
+
+
+<sect3> <title> Generalising the deriving clause </title>
+<para>
+GHC now permits such instances to be derived instead, so one can write 
+<programlisting> 
+  newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+</programlisting> 
+
+and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
+for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
+derives an instance declaration of the form
+
+<programlisting> 
+  instance Num Int => Num Dollars
+</programlisting> 
+
+which just adds or removes the <literal>newtype</literal> constructor according to the type.
+</para>
+<para>
+
+We can also derive instances of constructor classes in a similar
+way. For example, suppose we have implemented state and failure monad
+transformers, such that
+
+<programlisting> 
+  instance Monad m => Monad (State s m) 
+  instance Monad m => Monad (Failure m)
+</programlisting> 
+In Haskell 98, we can define a parsing monad by 
+<programlisting> 
+  type Parser tok m a = State [tok] (Failure m) a
+</programlisting> 
+
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract,
+without needing to write an instance of class <literal>Monad</literal>, via
+
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving Monad
+</programlisting>
+In this case the derived instance declaration is of the form 
+<programlisting> 
+  instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) 
+</programlisting> 
+
+Notice that, since <literal>Monad</literal> is a constructor class, the
+instance is a <emphasis>partial application</emphasis> of the new type, not the
+entire left hand side. We can imagine that the type declaration is
+``eta-converted'' to generate the context of the instance
+declaration.
+</para>
+<para>
+
+We can even derive instances of multi-parameter classes, provided the
+newtype is the last class parameter. In this case, a ``partial
+application'' of the class appears in the <literal>deriving</literal>
+clause. For example, given the class
+
+<programlisting> 
+  class StateMonad s m | m -> s where ... 
+  instance Monad m => StateMonad s (State s m) where ... 
+</programlisting> 
+then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by 
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving (Monad, StateMonad [tok])
+</programlisting>
+
+The derived instance is obtained by completing the application of the
+class to the new type:
+
+<programlisting> 
+  instance StateMonad [tok] (State [tok] (Failure m)) =>
+           StateMonad [tok] (Parser tok m)
+</programlisting>
+</para>
+<para>
+
+As a result of this extension, all derived instances in newtype
+ declarations are treated uniformly (and implemented just by reusing
+the dictionary for the representation type), <emphasis>except</emphasis>
+<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
+the newtype and its representation.
+</para>
+</sect3>
+
+<sect3> <title> A more precise specification </title>
+<para>
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
+
+<programlisting> 
+  newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm) 
+</programlisting> 
+
+where 
+ <itemizedlist>
+<listitem><para>
+  The <literal>ci</literal> are partial applications of
+  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.
+</para></listitem>
+<listitem><para>
+  The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
+</para></listitem>
+<listitem><para>
+  The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+  The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>, 
+  nor in the <literal>ci</literal>, and
+</para></listitem>
+<listitem><para>
+  None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>, 
+               <literal>Typeable</literal>, or <literal>Data</literal>.  These classes
+               should not "look through" the type or its constructor.  You can still
+               derive these classes for a newtype, but it happens in the usual way, not 
+               via this new mechanism.  
+</para></listitem>
+</itemizedlist>
+Then, for each <literal>ci</literal>, the derived instance
+declaration is:
+<programlisting> 
+  instance ci t => ci (T v1...vk)
+</programlisting>
+As an example which does <emphasis>not</emphasis> work, consider 
+<programlisting> 
+  newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
+</programlisting> 
+Here we cannot derive the instance 
+<programlisting> 
+  instance Monad (State s m) => Monad (NonMonad m) 
+</programlisting> 
+
+because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
+and so cannot be "eta-converted" away. It is a good thing that this
+<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
+not, in fact, a monad --- for the same reason. Try defining
+<literal>>>=</literal> with the correct type: you won't be able to.
+</para>
+<para>
+
+Notice also that the <emphasis>order</emphasis> of class parameters becomes
+important, since we can only derive instances for the last one. If the
+<literal>StateMonad</literal> class above were instead defined as
+
+<programlisting> 
+  class StateMonad m s | m -> s where ... 
+</programlisting>
+
+then we would not have been able to derive an instance for the
+<literal>Parser</literal> type above. We hypothesise that multi-parameter
+classes usually have one "main" parameter for which deriving new
+instances is most interesting.
+</para>
+<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>
+
+<sect2 id="stand-alone-deriving">
+<title>Stand-alone deriving declarations</title>
+
+<para>
+GHC now allows stand-alone <literal>deriving</literal> declarations, enabled by <literal>-fglasgow-exts</literal>:
+<programlisting>
+  data Foo a = Bar a | Baz String
+
+  derive instance Eq (Foo a)
+</programlisting>
+The token "<literal>derive</literal>" is a keyword only when followed by "<literal>instance</literal>";
+you can use it as a variable name elsewhere.</para>
+<para>The stand-alone syntax is generalised for newtypes in exactly the same
+way that ordinary <literal>deriving</literal> clauses are generalised (<xref linkend="newtype-deriving"/>).
+For example:
+<programlisting>
+  newtype Foo a = MkFoo (State Int a)
+
+  derive instance MonadState Int Foo
+</programlisting>
+GHC always treats the <emphasis>last</emphasis> parameter of the instance
+(<literal>Foo</literal> in this exmample) as the type whose instance is being derived.
+</para>
+
+</sect2>
+
+</sect1>
+
+
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="other-type-extensions">
+<title>Other type system extensions</title>
+
+<sect2 id="multi-param-type-classes">
+<title>Class declarations</title>
+
+<para>
+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>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>
+
+<sect3>
+<title>Multi-parameter type classes</title>
+<para>
+Multi-parameter type classes are permitted. For example:
+
+
+<programlisting>
+  class Collection c a where
+    union :: c a -> c a -> c a
+    ...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:
+
+
+<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>
+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:
+
+
+<programlisting>
+  class C a where {
+    op :: D b => a -> b -> b
+  }
+
+  class C a => D a where { ... }
+</programlisting>
+
+
+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>
+</sect3>
+
+
+
+
+<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>).
+GHC lifts this restriction.
+</para>
+
+
+</sect3>
+</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>
+
+<sect3><title>Rules for functional dependencies </title>
+<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
+    empty  :: s
+    insert :: s -> a -> s
+</programlisting>
+
+is not OK, because the type of <literal>empty</literal> doesn't mention
+<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
+    empty  :: s a
+    insert :: s a -> a -> s a
+</programlisting>
+
+
+which makes the connection between the type of a collection of
+<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
+
+
+<programlisting>
+  class CollE s where
+    empty  :: s
+
+  class CollE s => Coll s a where
+    insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>
+
+
+<sect3>
+<title>Background on functional dependencies</title>
+
+<para>The following description of the motivation and use of functional dependencies is taken
+from the Hugs user manual, reproduced here (with minor changes) by kind
+permission of Mark Jones.
+</para>
+<para> 
+Consider the following class, intended as part of a
+library for collection types:
+<programlisting>
+   class Collects e ce where
+       empty  :: ce
+       insert :: e -> ce -> ce
+       member :: e -> ce -> Bool
+</programlisting>
+The type variable e used here represents the element type, while ce is the type
+of the container itself. Within this framework, we might want to define
+instances of this class for lists or characteristic functions (both of which
+can be used to represent collections of any equality type), bit sets (which can
+be used to represent collections of characters), or hash tables (which can be
+used to represent any collection whose elements have a hash function). Omitting
+standard implementation details, this would lead to the following declarations: 
 <programlisting>
    instance Eq e => Collects e [e] where ...
    instance Eq e => Collects e (e -> Bool) where ...
@@ -1946,7 +2541,7 @@ the context and head of the instance declaration can each consist of arbitrary
 following rules:
 <orderedlist>
 <listitem><para>
-For each assertion in the context:
+The Paterson Conditions: for each assertion in the context
 <orderedlist>
 <listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
 <listitem><para>The assertion has fewer constructors and variables (taken together
@@ -1954,7 +2549,7 @@ For each assertion in the context:
 </orderedlist>
 </para></listitem>
 
-<listitem><para>The coverage condition.  For each functional dependency,
+<listitem><para>The Coverage Condition.  For each functional dependency,
 <replaceable>tvs</replaceable><subscript>left</subscript> <literal>-&gt;</literal>
 <replaceable>tvs</replaceable><subscript>right</subscript>,  of the class,
 every type variable in
@@ -1966,11 +2561,15 @@ corresponding type in the instance declaration.
 </orderedlist>
 These restrictions ensure that context reduction terminates: each reduction
 step makes the problem smaller by at least one
-constructor.  For example, the following would make the type checker
-loop if it wasn't excluded:
-<programlisting>
-  instance C a => C a where ...
-</programlisting>
+constructor.  Both the Paterson Conditions and the Coverage Condition are lifted 
+if you give the <option>-fallow-undecidable-instances</option> 
+flag (<xref linkend="undecidable-instances"/>).
+You can find lots of background material about the reason for these
+restrictions in the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
+Understanding functional dependencies via Constraint Handling Rules</ulink>.
+</para>
+<para>
 For example, these are OK:
 <programlisting>
   instance C Int [a]          -- Multiple parameters
@@ -2086,8 +2685,8 @@ makes instance inference go into a loop, because it requires the constraint
 Nevertheless, GHC allows you to experiment with more liberal rules.  If you use
 the experimental flag <option>-fallow-undecidable-instances</option>
 <indexterm><primary>-fallow-undecidable-instances
-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head.  Termination is ensured by having a
+option</primary></indexterm>, both the Paterson Conditions and the Coverage Condition
+(described in <xref linkend="instance-rules"/>) are lifted.  Termination is ensured by having a
 fixed-depth recursion stack.  If you exceed the stack depth you get a
 sort of backtrace, and the opportunity to increase the stack depth
 with <option>-fcontext-stack=</option><emphasis>N</emphasis>.
@@ -2178,8 +2777,20 @@ some other constraint.  But if the instance declaration was compiled with
 check for that declaration.
 </para></listitem>
 </itemizedlist>
-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.
+These rules make it possible for a library author to design a library that relies on 
+overlapping instances without the library client having to know.  
+</para>
+<para>
+If an instance declaration is compiled without
+<option>-fallow-overlapping-instances</option>,
+then that instance can never be overlapped.  This could perhaps be
+inconvenient.  Perhaps the rule should instead say that the
+<emphasis>overlapping</emphasis> instance declaration should be compiled in
+this way, rather than the <emphasis>overlapped</emphasis> one.  Perhaps overlap
+at a usage site should be permitted regardless of how the instance declarations
+are compiled, if the <option>-fallow-overlapping-instances</option> flag is
+used at the usage site.  (Mind you, the exact usage site can occasionally be
+hard to pin down.)  We are interested to receive feedback on these points.
 </para>
 <para>The <option>-fallow-incoherent-instances</option> flag implies the
 <option>-fallow-overlapping-instances</option> flag, but not vice versa.
@@ -2347,54 +2958,6 @@ territory free in case we need it later.
 </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>
@@ -2466,7 +3029,7 @@ function that called it. For example, our <literal>sort</literal> function might
 to pick out the least value in a list:
 <programlisting>
   least   :: (?cmp :: a -> a -> Bool) => [a] -> a
-  least xs = fst (sort xs)
+  least xs = head (sort xs)
 </programlisting>
 Without lifting a finger, the <literal>?cmp</literal> parameter is
 propagated to become a parameter of <literal>least</literal> as well. With explicit
@@ -2626,6 +3189,11 @@ inner binding of <literal>?x</literal>, so <literal>(f 9)</literal> will return
 </sect3>
 </sect2>
 
+    <!--   ======================= COMMENTED OUT ========================
+
+    We intend to remove linear implicit parameters, so I'm at least removing
+    them from the 6.6 user manual
+
 <sect2 id="linear-implicit-parameters">
 <title>Linear implicit parameters</title>
 <para>
@@ -2641,7 +3209,7 @@ problem that monads seem over-kill for certain sorts of problem, notably:
 
 <para>
 Linear implicit parameters are just like ordinary implicit parameters,
-except that they are "linear" -- that is, they cannot be copied, and
+except that they are "linear"; that is, they cannot be copied, and
 must be explicitly "split" instead.  Linear implicit parameters are
 written '<literal>%x</literal>' instead of '<literal>?x</literal>'.  
 (The '/' in the '%' suggests the split!)
@@ -2796,7 +3364,9 @@ and you'd be right.  That is why they are an experimental feature.
 
 </sect2>
 
-<sect2 id="sec-kinding">
+================ END OF Linear Implicit Parameters commented out -->
+
+<sect2 id="kinding">
 <title>Explicitly-kinded quantification</title>
 
 <para>
@@ -2890,6 +3460,8 @@ For example, all the following types are legal:
     g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
 
     f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+
+    f4 :: Int -> (forall a. a -> a)
 </programlisting>
 Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
 can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
@@ -2912,22 +3484,14 @@ that restriction has now been lifted.)
 In particular, a forall-type (also called a "type scheme"),
 including an operational type class context, is legal:
 <itemizedlist>
-<listitem> <para> On the left of a function arrow </para> </listitem>
-<listitem> <para> On the right of a function arrow (see <xref linkend="hoist"/>) </para> </listitem>
+<listitem> <para> On the left or right (see <literal>f4</literal>, for example)
+of a function arrow </para> </listitem>
 <listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
 example, any of the <literal>f1,f2,f3,g1,g2</literal> above would be valid
 field type signatures.</para> </listitem>
 <listitem> <para> As the type of an implicit parameter </para> </listitem>
 <listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables"/>) </para> </listitem>
 </itemizedlist>
-There is one place you cannot put a <literal>forall</literal>:
-you cannot instantiate a type variable with a forall-type.  So you cannot 
-make a forall-type the argument of a type constructor.  So these types are illegal:
-<programlisting>
-    x1 :: [forall a. a->a]
-    x2 :: (forall a. a->a, Int)
-    x3 :: Maybe (forall a. a->a)
-</programlisting>
 Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
 a type variable any more!
 </para>
@@ -3159,669 +3723,277 @@ but at least the rule is simple.  If you want the latter type, you
 can write your for-alls explicitly.  Indeed, doing so is strongly advised
 for rank-2 types.
 </para>
-</sect3>
-</sect2>
-
-
-
-
-<sect2 id="scoped-type-variables">
-<title>Scoped type variables
-</title>
-
-<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>
-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>.
-In particular, it is in scope at the type signature for <varname>y</varname>.
-</para>
-
-<para>
-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
-scope, all type variables mentioned in the signature are universally
-quantified, which is just as in Haskell 98.)  In this case, since <varname>a</varname>
-is in scope, it is not universally quantified, so the type of <varname>ys</varname> is
-the same as that of <varname>xs</varname>.  In Haskell 98 it is not possible to declare
-a type for <varname>ys</varname>; a major benefit of scoped type variables is that
-it becomes possible to do so.
-</para>
-
-<para>
-Scoped type variables are implemented in both GHC and Hugs.  Where the
-implementations differ from the specification below, those differences
-are noted.
-</para>
-
-<para>
-So much for the basic idea.  Here are the details.
-</para>
-
-<sect3>
-<title>What a scoped type variable means</title>
-<para>
-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
-  f (xs::[a]) (y::a) = (head xs + y) :: a
-</programlisting>
-The pattern type signatures on the left hand side of
-<literal>f</literal> express the fact that <literal>xs</literal>
-must be a list of things of some type <literal>a</literal>; and that <literal>y</literal>
-must have this same type.  The type signature on the expression <literal>(head xs)</literal>
-specifies that this expression must have the same type <literal>a</literal>.
-<emphasis>There is no requirement that the type named by "<literal>a</literal>" is
-in fact a type variable</emphasis>.  Indeed, in this case, the type named by "<literal>a</literal>" is
-<literal>Int</literal>.  (This is a slight liberalisation from the original rather complex
-rules, which specified that a pattern-bound type variable should be universally quantified.)
-For example, all of these are legal:</para>
-
-<programlisting>
-  t (x::a) (y::a) = x+y*2
-
-  f (x::a) (y::b) = [x,y]       -- a unifies with b
-
-  g (x::a) = x + 1::Int         -- a unifies with Int
-
-  h x = let k (y::a) = [x,y]    -- a is free in the
-        in k x                  -- environment
-
-  k (x::a) True    = ...        -- a unifies with Int
-  k (x::Int) False = ...
-
-  w :: [b] -> [b]
-  w (x::a) = x                  -- a unifies with [b]
-</programlisting>
-
-</sect3>
-
-<sect3>
-<title>Scope and implicit quantification</title>
-
-<para>
-
-<itemizedlist>
-<listitem>
-
-<para>
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern.  We describe this set as
-the <emphasis>type variables bound by the pattern</emphasis>.
-For example:
-<programlisting>
-  f (x::a) = let g (y::(a,b)) = fst y
-             in
-             g (x,True)
-</programlisting>
-The pattern <literal>(x::a)</literal> brings the type variable
-<literal>a</literal> into scope, as well as the term 
-variable <literal>x</literal>.  The pattern <literal>(y::(a,b))</literal>
-contains an occurrence of the already-in-scope type variable <literal>a</literal>,
-and brings into scope the type variable <literal>b</literal>.
-</para>
-</listitem>
-
-<listitem>
-<para>
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern.  For example:
-<programlisting>
-  let
-    f (x::a) = &lt;...rhs of f...>
-    (p::b, q::b) = (1,2)
-  in &lt;...body of let...>
-</programlisting>
-Here, the type variable <literal>a</literal> scopes over the right hand side of <literal>f</literal>,
-just like <literal>x</literal> does; while the type variable <literal>b</literal> scopes over the
-body of the <literal>let</literal>, and all the other definitions in the <literal>let</literal>,
-just like <literal>p</literal> and <literal>q</literal> do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the <literal>let</literal> group.
-</para>
-</listitem>
-
-
-<listitem>
-<para>
-The type variables bound by the pattern may be 
-mentioned in ordinary type signatures or pattern 
-type signatures anywhere within their scope.
-
-</para>
-</listitem>
-
-<listitem>
-<para>
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is <emphasis>not</emphasis> universally quantified.
-
-</para>
-</listitem>
-
-<listitem>
-
-<para>
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-<programlisting>
-  f :: a -> a
-  f x = x::a
-</programlisting>
-
-It's illegal because <varname>a</varname> is not in scope in the body of <function>f</function>,
-so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
-and that is an incorrect typing.
-
-</para>
-</listitem>
-
-<listitem>
-<para>
-The pattern type signature is a monotype:
-</para>
-
-<itemizedlist>
-<listitem> <para> 
-A pattern type signature cannot contain any explicit <literal>forall</literal> quantification.
-</para> </listitem>
-
-<listitem>  <para> 
-The type variables bound by a pattern type signature can only be instantiated to monotypes,
-not to type schemes.
-</para> </listitem>
-
-<listitem>  <para> 
-There is no implicit universal quantification on pattern type signatures (in contrast to
-ordinary type signatures).
-</para> </listitem>
-
-</itemizedlist>
-
-</listitem>
-
-<listitem>
-<para>
-
-The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
-scope over the methods defined in the <literal>where</literal> part.  For example:
-
-
-<programlisting>
-  class C a where
-    op :: [a] -> a
-
-    op xs = let ys::[a]
-                ys = reverse xs
-            in
-            head ys
-</programlisting>
-
-
-(Not implemented in Hugs yet, Dec 98).
-</para>
-</listitem>
-
-</itemizedlist>
-
-</para>
-
-</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>
-A pattern type signature can occur in any pattern.  For example:
-<itemizedlist>
-
-<listitem>
-<para>
-A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
-
-
-<programlisting>
-  f ((x,y)::(a,b)) = (y,x) :: (b,a)
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
-
-<programlisting>
-  (\ (x::a, y) :: a -> x)
-</programlisting>
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in <literal>case</literal> expressions:
-
-<programlisting>
-  case e of { ((x::a, y) :: (a,b)) -> x }
-</programlisting>
-
-Note that the <literal>-&gt;</literal> symbol in a case alternative
-leads to difficulties when parsing a type signature in the pattern: in
-the absence of the extra parentheses in the example above, the parser
-would try to interpret the <literal>-&gt;</literal> as a function
-arrow and give a parse error later.
-
-</para>
-
-</listitem>
-
-<listitem>
-<para>
-To avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort).  To see why,
-consider how one would parse this:
-
-
-<programlisting>
-  \ x :: a -> b -> x
-</programlisting>
-
-
-</para>
-</listitem>
-
-<listitem>
-
-<para>
- Pattern type signatures can bind existential type variables.
-For example:
-
-
-<programlisting>
-  data T = forall a. MkT [a]
-
-  f :: T -> T
-  f (MkT [t::a]) = MkT t3
-                 where
-                   t3::[a] = [t,t,t]
-</programlisting>
-
-
-</para>
-</listitem>
-
-
-<listitem>
-
-<para>
-Pattern type signatures 
-can be used in pattern bindings:
+</sect3>
+</sect2>
 
-<programlisting>
-  f x = let (y, z::a) = x in ...
-  f1 x                = let (y, z::Int) = x in ...
-  f2 (x::(Int,a))     = let (y, z::a)   = x in ...
-  f3 :: (b->b)        = \x -> x
-</programlisting>
 
-In all such cases, the binding is not generalised over the pattern-bound
-type variables.  Thus <literal>f3</literal> is monomorphic; <literal>f3</literal>
-has type <literal>b -&gt; b</literal> for some type <literal>b</literal>, 
-and <emphasis>not</emphasis> <literal>forall b. b -&gt; b</literal>.
-In contrast, the binding
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>.  This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types.  For example:
 <programlisting>
-  f4 :: b->b
-  f4 = \x -> x
+  f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+  f (Just g) = Just (g [3], g "hello")
+  f Nothing  = Nothing
 </programlisting>
-makes a polymorphic function, but <literal>b</literal> is not in scope anywhere
-in <literal>f4</literal>'s scope.
-
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
 </para>
-</listitem>
-</itemizedlist>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.  
 </para>
-<para>Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures.  The two can be used independently or together.</para>
-
-</sect3>
+</sect2>
 
-<sect3 id="result-type-sigs">
-<title>Result type signatures</title>
+<sect2 id="scoped-type-variables">
+<title>Lexically scoped type variables
+</title>
 
 <para>
-The result type of a function can be given a signature, thus:
-
-
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
 <programlisting>
-  f (x::a) :: [a] = [x,x,x]
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+     where
+       ys :: [a]
+       ys = reverse xs
 </programlisting>
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
+the entire definition of <literal>f</literal>.
+In particular, it is in scope at the type signature for <varname>ys</varname>. 
+In Haskell 98 it is not possible to declare
+a type for <varname>ys</varname>; a major benefit of scoped type variables is that
+it becomes possible to do so.
+</para>
+<para>Lexically-scoped type variables are enabled by
+<option>-fglasgow-exts</option>.
+</para>
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases.  Read this section
+carefully!</para>
 
+<sect3>
+<title>Overview</title>
 
-The final <literal>:: [a]</literal> after all the patterns gives a signature to the
-result type.  Sometimes this is the only way of naming the type variable
-you want:
-
-
-<programlisting>
-  f :: Int -> [a] -> [a]
-  f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
-                        in \xs -> map g (reverse xs `zip` xs)
-</programlisting>
-
+<para>The design follows the following principles
+<itemizedlist>
+<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
+a <emphasis>type</emphasis>. (This is a change from GHC's earlier
+design.)</para></listitem>
+<listitem><para>Furthermore, distinct lexical type variables stand for distinct
+type variables.  This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
+checker, and no inference is involved.</para></listitem>
+<listitem><para>Lexical type variables may be alpha-renamed freely, without
+changing the program.</para></listitem>
+</itemizedlist>
 </para>
 <para>
-The type variables bound in a result type signature scope over the right hand side
-of the definition. However, consider this corner-case:
-<programlisting>
-  rev1 :: [a] -> [a] = \xs -> reverse xs
-
-  foo ys = rev (ys::[a])
-</programlisting>
-The signature on <literal>rev1</literal> is considered a pattern type signature, not a result
-type signature, and the type variables it binds have the same scope as <literal>rev1</literal>
-itself (i.e. the right-hand side of <literal>rev1</literal> and the rest of the module too).
-In particular, the expression <literal>(ys::[a])</literal> is OK, because the type variable <literal>a</literal>
-is in scope (otherwise it would mean <literal>(ys::forall a.[a])</literal>, which would be rejected).  
+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>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
+</itemizedlist>
 </para>
 <para>
-As mentioned above, <literal>rev1</literal> is made monomorphic by this scoping rule.
-For example, the following program would be rejected, because it claims that <literal>rev1</literal>
-is polymorphic:
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (<ulink
+url="http://haskell.org/onlinereport/decls.html#sect4.1.2">Section
+4.1.2</ulink> 
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
+quantified. For example, if type variable <literal>a</literal> is in scope,
+then
 <programlisting>
-  rev1 :: [b] -> [b]
-  rev1 :: [a] -> [a] = \xs -> reverse xs
+  (e :: a -> a)     means     (e :: a -> a)
+  (e :: b -> b)     means     (e :: forall b. b->b)
+  (e :: a -> b)     means     (e :: forall b. a->b)
 </programlisting>
 </para>
 
-<para>
-Result type signatures are not yet implemented in Hugs.
-</para>
 
 </sect3>
 
-</sect2>
-
-<sect2 id="deriving-typeable">
-<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
 
-<para>
-Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type 
-declaration, to generate a standard instance declaration for classes specified in the <literal>deriving</literal> clause.  
-In Haskell 98, the only classes that may appear in the <literal>deriving</literal> clause are the standard
-classes <literal>Eq</literal>, <literal>Ord</literal>, 
-<literal>Enum</literal>, <literal>Ix</literal>, <literal>Bounded</literal>, <literal>Read</literal>, and <literal>Show</literal>.
-</para>
-<para>
-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.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.
+<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>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>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>
-</sect2>
-
-<sect2 id="newtype-deriving">
-<title>Generalised derived instances for newtypes</title>
-
-<para>
-When you define an abstract type using <literal>newtype</literal>, you may want
-the new type to inherit some instances from its representation. In
-Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
-<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
-other classes you have to write an explicit instance declaration. For
-example, if you define
-
-<programlisting> 
-  newtype Dollars = Dollars Int 
-</programlisting> 
+</sect3>
 
-and you want to use arithmetic on <literal>Dollars</literal>, you have to
-explicitly define an instance of <literal>Num</literal>:
+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
 
-<programlisting> 
-  instance Num Dollars where
-    Dollars a + Dollars b = Dollars (a+b)
-    ...
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression.  For example:
+<programlisting>
+  f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
 </programlisting>
-All the instance does is apply and remove the <literal>newtype</literal>
-constructor. It is particularly galling that, since the constructor
-doesn't appear at run-time, this instance declaration defines a
-dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
-dictionary, only slower!
+Here, the type signature <literal>forall a. ST s Bool</literal> brings the 
+type variable <literal>s</literal> into scope, in the annotated expression 
+<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
 </para>
 
+</sect3>
 
-<sect3> <title> Generalising the deriving clause </title>
+<sect3 id="pattern-type-sigs">
+<title>Pattern type signatures</title>
 <para>
-GHC now permits such instances to be derived instead, so one can write 
-<programlisting> 
-  newtype Dollars = Dollars Int deriving (Eq,Show,Num)
-</programlisting> 
-
-and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
-for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
-derives an instance declaration of the form
-
-<programlisting> 
-  instance Num Int => Num Dollars
-</programlisting> 
-
-which just adds or removes the <literal>newtype</literal> constructor according to the type.
+A type signature may occur in any pattern; this is a <emphasis>pattern type
+signature</emphasis>.  
+For example:
+<programlisting>
+  -- f and g assume that 'a' is already in scope
+  f = \(x::Int, y::a) -> x
+  g (x::a) = x
+  h ((x,y) :: (Int,Bool)) = (y,x)
+</programlisting>
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
 </para>
 <para>
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor.  For example:
+<programlisting>
+  data T = forall a. MkT [a]
 
-We can also derive instances of constructor classes in a similar
-way. For example, suppose we have implemented state and failure monad
-transformers, such that
-
-<programlisting> 
-  instance Monad m => Monad (State s m) 
-  instance Monad m => Monad (Failure m)
-</programlisting> 
-In Haskell 98, we can define a parsing monad by 
-<programlisting> 
-  type Parser tok m a = State [tok] (Failure m) a
-</programlisting> 
-
-which is automatically a monad thanks to the instance declarations
-above. With the extension, we can make the parser type abstract,
-without needing to write an instance of class <literal>Monad</literal>, via
-
-<programlisting> 
-  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
-                         deriving Monad
+  k :: T -> T
+  k (MkT [t::a]) = MkT t3
+                 where
+                   t3::[a] = [t,t,t]
 </programlisting>
-In this case the derived instance declaration is of the form 
-<programlisting> 
-  instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) 
-</programlisting> 
-
-Notice that, since <literal>Monad</literal> is a constructor class, the
-instance is a <emphasis>partial application</emphasis> of the new type, not the
-entire left hand side. We can imagine that the type declaration is
-``eta-converted'' to generate the context of the instance
-declaration.
+Here, the pattern type signature <literal>(t::a)</literal> mentions a lexical type
+variable that is not already in scope.  Indeed, it cannot already be in scope,
+because it is bound by the pattern match.  GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
 </para>
 <para>
-
-We can even derive instances of multi-parameter classes, provided the
-newtype is the last class parameter. In this case, a ``partial
-application'' of the class appears in the <literal>deriving</literal>
-clause. For example, given the class
-
-<programlisting> 
-  class StateMonad s m | m -> s where ... 
-  instance Monad m => StateMonad s (State s m) where ... 
-</programlisting> 
-then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by 
-<programlisting> 
-  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
-                         deriving (Monad, StateMonad [tok])
-</programlisting>
-
-The derived instance is obtained by completing the application of the
-class to the new type:
-
-<programlisting> 
-  instance StateMonad [tok] (State [tok] (Failure m)) =>
-           StateMonad [tok] (Parser tok m)
-</programlisting>
+If this seems a little odd, we think so too.  But we must have
+<emphasis>some</emphasis> way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
 </para>
 <para>
-
-As a result of this extension, all derived instances in newtype
- declarations are treated uniformly (and implemented just by reusing
-the dictionary for the representation type), <emphasis>except</emphasis>
-<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
-the newtype and its representation.
+This is (now) the <emphasis>only</emphasis> situation in which a pattern type 
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both <literal>f</literal> and <literal>g</literal> would be
+illegal if <literal>a</literal> was not already in scope.
 </para>
+
+
 </sect3>
 
-<sect3> <title> A more precise specification </title>
-<para>
-Derived instance declarations are constructed as follows. Consider the
-declaration (after expansion of any type synonyms)
+<!-- ==================== Commented out part about result type signatures 
 
-<programlisting> 
-  newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm) 
-</programlisting> 
+<sect3 id="result-type-sigs">
+<title>Result type signatures</title>
 
-where 
- <itemizedlist>
-<listitem><para>
-  The type <literal>t</literal> is an arbitrary type
-</para></listitem>
-<listitem><para>
-  The <literal>vk+1...vn</literal> are type variables which do not occur in 
-  <literal>t</literal>, and
-</para></listitem>
-<listitem><para>
-  The <literal>ci</literal> are partial applications of
-  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
-  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.
-</para></listitem>
-<listitem><para>
-  None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>, 
-               <literal>Typeable</literal>, or <literal>Data</literal>.  These classes
-               should not "look through" the type or its constructor.  You can still
-               derive these classes for a newtype, but it happens in the usual way, not 
-               via this new mechanism.  
-</para></listitem>
-</itemizedlist>
-Then, for each <literal>ci</literal>, the derived instance
-declaration is:
-<programlisting> 
-  instance ci (t vk+1...v) => ci (T v1...vp)
-</programlisting>
-where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the 
-right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
-</para>
 <para>
+The result type of a function, lambda, or case expression alternative can be given a signature, thus:
 
-As an example which does <emphasis>not</emphasis> work, consider 
-<programlisting> 
-  newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
-</programlisting> 
-Here we cannot derive the instance 
-<programlisting> 
-  instance Monad (State s m) => Monad (NonMonad m) 
-</programlisting> 
+<programlisting>
+  {- f assumes that 'a' is already in scope -}
+  f x y :: [a] = [x,y,x]
+
+  g = \ x :: [Int] -> [3,4]
 
-because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
-and so cannot be "eta-converted" away. It is a good thing that this
-<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
-not, in fact, a monad --- for the same reason. Try defining
-<literal>>>=</literal> with the correct type: you won't be able to.
+  h :: forall a. [a] -> a
+  h xs = case xs of
+           (y:ys) :: a -> y
+</programlisting>
+The final <literal>:: [a]</literal> after the patterns of <literal>f</literal> gives the type of 
+the result of the function.  Similarly, the body of the lambda in the RHS of
+<literal>g</literal> is <literal>[Int]</literal>, and the RHS of the case
+alternative in <literal>h</literal> is <literal>a</literal>.
 </para>
+<para> A result type signature never brings new type variables into scope.</para>
 <para>
+There are a couple of syntactic wrinkles.  First, notice that all three
+examples would parse quite differently with parentheses:
+<programlisting>
+  {- f assumes that 'a' is already in scope -}
+  f x (y :: [a]) = [x,y,x]
 
-Notice also that the <emphasis>order</emphasis> of class parameters becomes
-important, since we can only derive instances for the last one. If the
-<literal>StateMonad</literal> class above were instead defined as
+  g = \ (x :: [Int]) -> [3,4]
 
-<programlisting> 
-  class StateMonad m s | m -> s where ... 
+  h :: forall a. [a] -> a
+  h xs = case xs of
+           ((y:ys) :: a) -> y
 </programlisting>
+Now the signature is on the <emphasis>pattern</emphasis>; and
+<literal>h</literal> would certainly be ill-typed (since the pattern
+<literal>(y:ys)</literal> cannot have the type <literal>a</literal>.
 
-then we would not have been able to derive an instance for the
-<literal>Parser</literal> type above. We hypothesise that multi-parameter
-classes usually have one "main" parameter for which deriving new
-instances is most interesting.
+Second, to avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort).  To see why,
+consider how one would parse this:
+<programlisting>
+  \ x :: a -> b -> x
+</programlisting>
 </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.)
+</sect3>
+
+ -->
+
+<sect3 id="cls-inst-scoped-tyvars">
+<title>Class and instance declarations</title>
+<para>
+
+The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
+scope over the methods defined in the <literal>where</literal> part.  For example:
+
+
+<programlisting>
+  class C a where
+    op :: [a] -> a
+
+    op xs = let ys::[a]
+                ys = reverse xs
+            in
+            head ys
+</programlisting>
 </para>
 </sect3>
 
 </sect2>
 
+
 <sect2 id="typing-binds">
 <title>Generalised typing of mutually recursive bindings</title>
 
@@ -3885,193 +4057,109 @@ pattern binding must have the same context.  For example, this is fine:
 </para>
 </sect2>
 
-</sect1>
-<!-- ==================== End of type system extensions =================  -->
-  
-<!-- ====================== Generalised algebraic data types =======================  -->
-
-<sect1 id="gadt">
-<title>Generalised Algebraic Data Types</title>
+<sect2 id="overloaded-strings">
+<title>Overloaded string literals
+</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:
+<para>
+GHC supports <emphasis>overloaded string literals</emphasis>.  Normally a
+string literal has type <literal>String</literal>, but with overloaded string
+literals enabled (with <literal>-foverloaded-strings</literal>)
+ a string literal has type <literal>(IsString a) => a</literal>.
+</para>
+<para>
+This means that the usual string syntax can be used, e.g., for packed strings
+and other variations of string like types.  String literals behave very much
+like integer literals, i.e., they can be used in both expressions and patterns.
+If used in a pattern the literal with be replaced by an equality test, in the same
+way as an integer literal is.
+</para>
+<para>
+The class <literal>IsString</literal> is defined as:
 <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)
+class IsString a where
+    fromString :: String -> a
 </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>:
+The only predefined instance is the obvious one to make strings work as usual:
 <programlisting>
-  eval :: Term a -> a
-  eval (Lit i)             = i
-  eval (Succ t)     = 1 + eval t
-  eval (IsZero t)   = eval t == 0
-  eval (If b e1 e2) = if eval b then eval e1 else eval e2
-  eval (Pair e1 e2) = (eval e1, eval e2)
+instance IsString [Char] where
+    fromString cs = cs
 </programlisting>
-These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
+The class <literal>IsString</literal> is not in scope by default.  If you want to mention
+it explicitly (for exmaple, to give an instance declaration for it), you can import it
+from module <literal>GHC.Exts</literal>.
 </para>
-<para> The extensions to GHC are these:
+<para>
+Haskell's defaulting mechanism is extended to cover string literals, when <option>-foverloaded-strings</option> is specified.
+Specifically:
 <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>.
+Each type in a default declaration must be an 
+instance of <literal>Num</literal> <emphasis>or</emphasis> of <literal>IsString</literal>.
 </para></listitem>
 
 <listitem><para>
-You can use record syntax on a GADT-style data type declaration:
-
-<programlisting>
-  data Term a where
-      Lit    { val  :: Int }      :: Term Int
-      Succ   { num  :: Term Int } :: Term Int
-      Pred   { num  :: Term Int } :: Term Int
-      IsZero { arg  :: Term Int } :: Term Bool 
-      Pair   { arg1 :: Term a
-             , arg2 :: Term b
-             }                    :: Term (a,b)
-      If     { cnd  :: Term Bool
-             , tru  :: Term a
-             , fls  :: Term a
-             }                    :: Term a
-</programlisting>
-For every constructor that has a field <literal>f</literal>, (a) the type of
-field <literal>f</literal> must be the same; and (b) the
-result type of the constructor must be the same; both modulo alpha conversion.
-Hence, in our example, we cannot merge the <literal>num</literal> and <literal>arg</literal>
-fields above into a 
-single name.  Although their field types are both <literal>Term Int</literal>,
-their selector functions actually have different types:
-
-<programlisting>
-  num :: Term Int -> Term Int
-  arg :: Term Bool -> Term Int
-</programlisting>
-
-At the moment, record updates are not yet possible with GADT, so support is 
-limited to record construction, selection and pattern matching:
-
-<programlisting>
-  someTerm :: Term Bool
-  someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
-
-  eval :: Term a -> a
-  eval Lit    { val = i } = i
-  eval Succ   { num = t } = eval t + 1
-  eval Pred   { num = t } = eval t - 1
-  eval IsZero { arg = t } = eval t == 0
-  eval Pair   { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
-  eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
-</programlisting>
-
+The standard defaulting rule (<ulink url="http://haskell.org/onlinereport/decls.html#sect4.3.4">Haskell Report, Section 4.3.4</ulink>)
+is extended thus: defaulting applies when all the unresolved constraints involve standard classes
+<emphasis>or</emphasis> <literal>IsString</literal>; and at least one is a numeric class
+<emphasis>or</emphasis> <literal>IsString</literal>.
 </para></listitem>
-
-<listitem><para>
-You can use strictness annotations, in the obvious places
-in the constructor type:
+</itemizedlist>
+</para>
+<para>
+A small example:
 <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>
+module Main where
 
-<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 )
+import GHC.Exts( IsString(..) )
 
-  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>
+newtype MyString = MyString String deriving (Eq, Show)
+instance IsString MyString where
+    fromString = MyString
 
-<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>
+greet :: MyString -> MyString
+greet "hello" = "world"
+greet other = other
 
-<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
+main = do
+    print $ greet "hello"
+    print $ greet "fool"
 </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>
+Note that deriving <literal>Eq</literal> is necessary for the pattern matching
+to work since it gets translated into an equality comparison.
 </para>
+</sect2>
 
-<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 =======================  -->
-
+<!-- ==================== End of type system extensions =================  -->
+  
 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">
 <title>Template Haskell</title>
 
-<para>Template Haskell allows you to do compile-time meta-programming in Haskell.  There is a "home page" for
-Template Haskell at <ulink url="http://www.haskell.org/th/">
-http://www.haskell.org/th/</ulink>, while
-the background to
+<para>Template Haskell allows you to do compile-time meta-programming in
+Haskell.  
+The background to
 the main technical innovations is discussed in "<ulink
 url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
 Template Meta-programming for Haskell</ulink>" (Proc Haskell Workshop 2002).
-The details of the Template Haskell design are still in flux.  Make sure you
-consult the <ulink url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online library reference material</ulink> 
+</para>
+<para>
+There is a Wiki page about
+Template Haskell at <ulink url="http://haskell.org/haskellwiki/Template_Haskell">
+http://www.haskell.org/th/</ulink>, and that is the best place to look for
+further details.
+You may also 
+consult the <ulink
+url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online
+Haskell library reference material</ulink> 
 (search for the type ExpQ).
 [Temporary: many changes to the original design are described in 
       <ulink url="http://research.microsoft.com/~simonpj/tmp/notes2.ps">"http://research.microsoft.com/~simonpj/tmp/notes2.ps"</ulink>.
-Not all of these changes are in GHC 6.2.]
+Not all of these changes are in GHC 6.6.]
 </para>
 
 <para> The first example from that paper is set out below as a worked example to help get you started. 
@@ -4155,6 +4243,14 @@ Tim Sheard is going to expand it.)
            (It would make sense to do so, but it's hard to implement.)
    </para></listitem>
 
+   <listitem><para>
+   Furthermore, you can only run a function at compile time if it is imported
+   from another module <emphasis>that is not part of a mutually-recursive group of modules
+   that includes the module currently being compiled</emphasis>.  For example, when compiling module A,
+   you can only run Template Haskell functions imported from B if B does not import A (directly or indirectly).
+   The reason should be clear: to run B we must compile and run A, but we are currently type-checking A.
+   </para></listitem>
+
     <listitem><para>
            The flag <literal>-ddump-splices</literal> shows the expansion of all top-level splices as they happen.
    </para></listitem>
@@ -4772,9 +4868,153 @@ Because the preprocessor targets Haskell (rather than Core),
 
 </sect1>
 
+<!-- ==================== BANG PATTERNS =================  -->
+
+<sect1 id="bang-patterns">
+<title>Bang patterns
+<indexterm><primary>Bang patterns</primary></indexterm>
+</title>
+<para>GHC supports an extension of pattern matching called <emphasis>bang
+patterns</emphasis>.   Bang patterns are under consideration for Haskell Prime.
+The <ulink
+url="http://hackage.haskell.org/trac/haskell-prime/wiki/BangPatterns">Haskell
+prime feature description</ulink> contains more discussion and examples
+than the material below.
+</para>
+<para>
+Bang patterns are enabled by the flag <option>-fbang-patterns</option>.
+</para>
+
+<sect2 id="bang-patterns-informal">
+<title>Informal description of bang patterns
+</title>
+<para>
+The main idea is to add a single new production to the syntax of patterns:
+<programlisting>
+  pat ::= !pat
+</programlisting>
+Matching an expression <literal>e</literal> against a pattern <literal>!p</literal> is done by first
+evaluating <literal>e</literal> (to WHNF) and then matching the result against <literal>p</literal>.
+Example:
+<programlisting>
+f1 !x = True
+</programlisting>
+This definition makes <literal>f1</literal> is strict in <literal>x</literal>,
+whereas without the bang it would be lazy.
+Bang patterns can be nested of course:
+<programlisting>
+f2 (!x, y) = [x,y]
+</programlisting>
+Here, <literal>f2</literal> is strict in <literal>x</literal> but not in
+<literal>y</literal>.  
+A bang only really has an effect if it precedes a variable or wild-card pattern:
+<programlisting>
+f3 !(x,y) = [x,y]
+f4 (x,y)  = [x,y]
+</programlisting>
+Here, <literal>f3</literal> and <literal>f4</literal> are identical; putting a bang before a pattern that
+forces evaluation anyway does nothing.
+</para><para>
+Bang patterns work in <literal>case</literal> expressions too, of course:
+<programlisting>
+g5 x = let y = f x in body
+g6 x = case f x of { y -&gt; body }
+g7 x = case f x of { !y -&gt; body }
+</programlisting>
+The functions <literal>g5</literal> and <literal>g6</literal> mean exactly the same thing.  
+But <literal>g7</literal> evalutes <literal>(f x)</literal>, binds <literal>y</literal> to the
+result, and then evaluates <literal>body</literal>.
+</para><para>
+Bang patterns work in <literal>let</literal> and <literal>where</literal>
+definitions too. For example:
+<programlisting>
+let ![x,y] = e in b
+</programlisting>
+is a strict pattern: operationally, it evaluates <literal>e</literal>, matches
+it against the pattern <literal>[x,y]</literal>, and then evaluates <literal>b</literal>
+The "<literal>!</literal>" should not be regarded as part of the pattern; after all,
+in a function argument <literal>![x,y]</literal> means the 
+same as <literal>[x,y]</literal>.  Rather, the "<literal>!</literal>" 
+is part of the syntax of <literal>let</literal> bindings.
+</para>
+</sect2>
+
+
+<sect2 id="bang-patterns-sem">
+<title>Syntax and semantics
+</title>
+<para>
+
+We add a single new production to the syntax of patterns:
+<programlisting>
+  pat ::= !pat
+</programlisting>
+There is one problem with syntactic ambiguity.  Consider:
+<programlisting>
+f !x = 3
+</programlisting>
+Is this a definition of the infix function "<literal>(!)</literal>",
+or of the "<literal>f</literal>" with a bang pattern? GHC resolves this
+ambiguity in favour of the latter.  If you want to define
+<literal>(!)</literal> with bang-patterns enabled, you have to do so using
+prefix notation:
+<programlisting>
+(!) f x = 3
+</programlisting>
+The semantics of Haskell pattern matching is described in <ulink
+url="http://haskell.org/onlinereport/exps.html#sect3.17.2">
+Section 3.17.2</ulink> of the Haskell Report.  To this description add 
+one extra item 10, saying:
+<itemizedlist><listitem><para>Matching
+the pattern <literal>!pat</literal> against a value <literal>v</literal> behaves as follows:
+<itemizedlist><listitem><para>if <literal>v</literal> is bottom, the match diverges</para></listitem>
+               <listitem><para>otherwise, <literal>pat</literal> is matched against
+               <literal>v</literal></para></listitem>
+</itemizedlist>
+</para></listitem></itemizedlist>
+Similarly, in Figure 4 of  <ulink url="http://haskell.org/onlinereport/exps.html#sect3.17.3">
+Section 3.17.3</ulink>, add a new case (t):
+<programlisting>
+case v of { !pat -> e; _ -> e' }
+   = v `seq` case v of { pat -> e; _ -> e' }
+</programlisting>
+</para><para>
+That leaves let expressions, whose translation is given in 
+<ulink url="http://haskell.org/onlinereport/exps.html#sect3.12">Section
+3.12</ulink>
+of the Haskell Report.
+In the translation box, first apply 
+the following transformation:  for each pattern <literal>pi</literal> that is of 
+form <literal>!qi = ei</literal>, transform it to <literal>(xi,!qi) = ((),ei)</literal>, and and replace <literal>e0</literal> 
+by <literal>(xi `seq` e0)</literal>.  Then, when none of the left-hand-side patterns
+have a bang at the top, apply the rules in the existing box.
+</para>
+<para>The effect of the let rule is to force complete matching of the pattern
+<literal>qi</literal> before evaluation of the body is begun.  The bang is
+retained in the translated form in case <literal>qi</literal> is a variable,
+thus:
+<programlisting>
+  let !y = f x in b
+</programlisting>
+
+</para>
+<para>
+The let-binding can be recursive.  However, it is much more common for
+the let-binding to be non-recursive, in which case the following law holds:
+<literal>(let !p = rhs in body)</literal>
+     is equivalent to
+<literal>(case rhs of !p -> body)</literal>
+</para>
+<para>
+A pattern with a bang at the outermost level is not allowed at the top level of
+a module.
+</para>
+</sect2>
+</sect1>
+
 <!-- ==================== ASSERTIONS =================  -->
 
-<sect1 id="sec-assertions">
+<sect1 id="assertions">
 <title>Assertions
 <indexterm><primary>Assertions</primary></indexterm>
 </title>
@@ -5743,12 +5983,6 @@ The following are good consumers:
 <listitem>
 
 <para>
- <function>length</function>
-</para>
-</listitem>
-<listitem>
-
-<para>
  <function>++</function> (on its first argument)
 </para>
 </listitem>
@@ -6016,7 +6250,7 @@ r)
                    GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
 r) ->
               tpl2})
-        (%note "foo"
+        (%note "bar"
          eta);
 </programlisting>
 
@@ -6038,6 +6272,22 @@ r) ->
 described in this section.  All are exported by
 <literal>GHC.Exts</literal>.</para>
 
+<sect2> <title>The <literal>seq</literal> function </title>
+<para>
+The function <literal>seq</literal> is as described in the Haskell98 Report.
+<programlisting>
+  seq :: a -> b -> b
+</programlisting>
+It evaluates its first argument to head normal form, and then returns its
+second argument as the result.  The reason that it is documented here is 
+that, despite <literal>seq</literal>'s polymorphism, its 
+second argument can have an unboxed type, or
+can be an unboxed tuple; for example <literal>(seq x 4#)</literal>
+or <literal>(seq x (# p,q #))</literal>.  This requires <literal>b</literal>
+to be instantiated to an unboxed type, which is not usually allowed.
+</para>
+</sect2>
+
 <sect2> <title>The <literal>inline</literal> function </title>
 <para>
 The <literal>inline</literal> function is somewhat experimental.
@@ -6096,6 +6346,11 @@ If <literal>lazy</literal> were not lazy, <literal>par</literal> would
 look strict in <literal>y</literal> which would defeat the whole 
 purpose of <literal>par</literal>.
 </para>
+<para>
+Like <literal>seq</literal>, the argument of <literal>lazy</literal> can have
+an unboxed type.
+</para>
+
 </sect2>
 
 <sect2> <title>The <literal>unsafeCoerce#</literal> function </title>
@@ -6111,16 +6366,20 @@ It is generally used when you want to write a program that you know is
 well-typed, but where Haskell's type system is not expressive enough to prove
 that it is well typed.
 </para>
+<para>
+The argument to <literal>unsafeCoerce#</literal> can have unboxed types,
+although extremely bad things will happen if you coerce a boxed type 
+to an unboxed type.
+</para>
+
 </sect2>
+
 </sect1>
 
 
 <sect1 id="generic-classes">
 <title>Generic classes</title>
 
-    <para>(Note: support for generic classes is currently broken in
-    GHC 5.02).</para>
-
 <para>
 The ideas behind this extension are described in detail in "Derivable type classes",
 Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
@@ -6371,6 +6630,51 @@ Just to finish with, here's another example I rather like:
 </sect2>
 </sect1>
 
+<sect1 id="monomorphism">
+<title>Control over monomorphism</title>
+
+<para>GHC supports two flags that control the way in which generalisation is
+carried out at let and where bindings.
+</para>
+
+<sect2>
+<title>Switching off the dreaded Monomorphism Restriction</title>
+          <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
+
+<para>Haskell's monomorphism restriction (see 
+<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.5">Section
+4.5.5</ulink>
+of the Haskell Report)
+can be completely switched off by
+<option>-fno-monomorphism-restriction</option>.
+</para>
+</sect2>
+
+<sect2>
+<title>Monomorphic pattern bindings</title>
+          <indexterm><primary><option>-fno-mono-pat-binds</option></primary></indexterm>
+          <indexterm><primary><option>-fmono-pat-binds</option></primary></indexterm>
+
+         <para> As an experimental change, we are exploring the possibility of
+         making pattern bindings monomorphic; that is, not generalised at all.  
+           A pattern binding is a binding whose LHS has no function arguments,
+           and is not a simple variable.  For example:
+<programlisting>
+  f x = x                    -- Not a pattern binding
+  f = \x -> x                -- Not a pattern binding
+  f :: Int -> Int = \x -> x  -- Not a pattern binding
+
+  (g,h) = e                  -- A pattern binding
+  (f) = e                    -- A pattern binding
+  [x] = e                    -- A pattern binding
+</programlisting>
+Experimentally, GHC now makes pattern bindings monomorphic <emphasis>by
+default</emphasis>.  Use <option>-fno-mono-pat-binds</option> to recover the
+standard behaviour.
+</para>
+</sect2>
+</sect1>
+
 
 
 <!-- Emacs stuff: