New syntax for GADT-style record declarations, and associated refactoring
[ghc-hetmet.git] / docs / users_guide / glasgow_exts.xml
index 6b8a20b..5d1b5cf 100644 (file)
@@ -38,277 +38,68 @@ documentation</ulink> describes all the libraries that come with GHC.
     <indexterm><primary>extensions</primary><secondary>options controlling</secondary>
     </indexterm>
 
-    <para>The language option flag control what variation of the language are
+    <para>The language option flags control what variation of the language are
     permitted.  Leaving out all of them gives you standard Haskell
     98.</para>
 
-    <para>Generally speaking, all the language options are introduced by "<option>-X</option>", 
-    e.g. <option>-XTemplateHaskell</option>.
-    </para>
-
-   <para> All the language options can be turned off by using the prefix "<option>No</option>"; 
-      e.g. "<option>-XNoTemplateHaskell</option>".</para>
-
-   <para> Language options recognised by Cabal can also be enabled using the <literal>LANGUAGE</literal> pragma,
-   thus <literal>{-# LANGUAGE TemplateHaskell #-}</literal> (see <xref linkend="language-pragma"/>>). </para>
-
-    <para>Turning on an option that enables special syntax
-    <emphasis>might</emphasis> cause working Haskell 98 code to fail
-    to compile, perhaps because it uses a variable name which has
-    become a reserved word.  So, together with each option below, we
-    list the special syntax which is enabled by this option.  We use
-    notation and nonterminal names from the Haskell 98 lexical syntax
-    (see the Haskell 98 Report).  There are two classes of special
-    syntax:</para>
-
+    <para>Language options can be controlled in two ways:
     <itemizedlist>
-      <listitem>
-       <para>New reserved words and symbols: character sequences
-        which are no longer available for use as identifiers in the
-        program.</para>
-      </listitem>
-      <listitem>
-       <para>Other special syntax: sequences of characters that have
-       a different meaning when this particular option is turned
-       on.</para>
-      </listitem>
-    </itemizedlist>
-
-    <para>We are only listing syntax changes here that might affect
-    existing working programs (i.e. "stolen" syntax).  Many of these
-    extensions will also enable new context-free syntax, but in all
-    cases programs written to use the new syntax would not be
-    compilable without the option enabled.</para>
-
-    <variablelist>
-
-      <varlistentry>
-       <term>
-          <option>-fglasgow-exts</option>:
+      <listitem><para>Every language option can switched on by a command-line flag "<option>-X...</option>" 
+        (e.g. <option>-XTemplateHaskell</option>), and switched off by the flag "<option>-XNo...</option>"; 
+        (e.g. <option>-XNoTemplateHaskell</option>).</para></listitem>
+      <listitem><para>
+          Language options recognised by Cabal can also be enabled using the <literal>LANGUAGE</literal> pragma,
+          thus <literal>{-# LANGUAGE TemplateHaskell #-}</literal> (see <xref linkend="language-pragma"/>). </para>
+          </listitem>
+      </itemizedlist></para>
+
+    <para>The flag <option>-fglasgow-exts</option>
           <indexterm><primary><option>-fglasgow-exts</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para>This simultaneously enables all of the extensions to
-          Haskell 98 described in <xref
-          linkend="ghc-language-features"/>, except where otherwise
-          noted. We are trying to move away from this portmanteau flag, 
+         is equivalent to enabling the following extensions: 
+          <option>-XPrintExplicitForalls</option>,
+          <option>-XForeignFunctionInterface</option>,
+          <option>-XUnliftedFFITypes</option>,
+          <option>-XGADTs</option>,
+          <option>-XImplicitParams</option>,
+          <option>-XScopedTypeVariables</option>,
+          <option>-XUnboxedTuples</option>,
+          <option>-XTypeSynonymInstances</option>,
+          <option>-XStandaloneDeriving</option>,
+          <option>-XDeriveDataTypeable</option>,
+          <option>-XFlexibleContexts</option>,
+          <option>-XFlexibleInstances</option>,
+          <option>-XConstrainedClassMethods</option>,
+          <option>-XMultiParamTypeClasses</option>,
+          <option>-XFunctionalDependencies</option>,
+          <option>-XMagicHash</option>,
+          <option>-XPolymorphicComponents</option>,
+          <option>-XExistentialQuantification</option>,
+          <option>-XUnicodeSyntax</option>,
+          <option>-XPostfixOperators</option>,
+          <option>-XPatternGuards</option>,
+          <option>-XLiberalTypeSynonyms</option>,
+          <option>-XRankNTypes</option>,
+          <option>-XImpredicativeTypes</option>,
+          <option>-XTypeOperators</option>,
+          <option>-XRecursiveDo</option>,
+          <option>-XParallelListComp</option>,
+          <option>-XEmptyDataDecls</option>,
+          <option>-XKindSignatures</option>,
+          <option>-XGeneralizedNewtypeDeriving</option>,
+          <option>-XTypeFamilies</option>.
+           Enabling these options is the <emphasis>only</emphasis> 
+           effect of <option>-fglasgow-exts</option>.
+          We are trying to move away from this portmanteau flag, 
          and towards enabling features individually.</para>
 
-         <para>New reserved words: <literal>forall</literal> (only in
-         types), <literal>mdo</literal>.</para>
-
-         <para>Other syntax stolen:
-             <replaceable>varid</replaceable>{<literal>&num;</literal>},
-             <replaceable>char</replaceable><literal>&num;</literal>,      
-             <replaceable>string</replaceable><literal>&num;</literal>,    
-             <replaceable>integer</replaceable><literal>&num;</literal>,    
-             <replaceable>float</replaceable><literal>&num;</literal>,    
-             <replaceable>float</replaceable><literal>&num;&num;</literal>,    
-             <literal>(&num;</literal>, <literal>&num;)</literal>,         
-             <literal>|)</literal>, <literal>{|</literal>.</para>
-
-         <para>Implies these specific language options: 
-           <option>-XForeignFunctionInterface</option>,
-           <option>-XImplicitParams</option>,
-           <option>-XScopedTypeVariables</option>,
-           <option>-XGADTs</option>, 
-           <option>-XTypeFamilies</option>. </para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XForeignFunctionInterface</option>:
-          <indexterm><primary><option>-XForeignFunctionInterface</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para>This option enables the language extension defined in the
-         Haskell 98 Foreign Function Interface Addendum.</para>
-
-         <para>New reserved words: <literal>foreign</literal>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XMonomorphismRestriction</option>,<option>-XMonoPatBinds</option>:
-        </term>
-       <listitem>
-         <para> These two flags control how generalisation is done.
-           See <xref linkend="monomorphism"/>.
-          </para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XExtendedDefaultRules</option>:
-          <indexterm><primary><option>-XExtendedDefaultRules</option></primary></indexterm>
-        </term>
-       <listitem>
-         <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>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XOverlappingInstances</option>
-          <indexterm><primary><option>-XOverlappingInstances</option></primary></indexterm>
-        </term>
-       <term>
-          <option>-XUndecidableInstances</option>
-          <indexterm><primary><option>-XUndecidableInstances</option></primary></indexterm>
-        </term>
-       <term>
-          <option>-XIncoherentInstances</option>
-          <indexterm><primary><option>-XIncoherentInstances</option></primary></indexterm>
-        </term>
-       <term>
-          <option>-fcontext-stack=N</option>
-          <indexterm><primary><option>-fcontext-stack</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para> See <xref linkend="instance-decls"/>.  Only relevant
-          if you also use <option>-fglasgow-exts</option>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-finline-phase</option>
-          <indexterm><primary><option>-finline-phase</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para>See <xref linkend="rewrite-rules"/>.  Only relevant if
-          you also use <option>-fglasgow-exts</option>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XArrows</option>
-          <indexterm><primary><option>-XArrows</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para>See <xref linkend="arrow-notation"/>.  Independent of
-          <option>-fglasgow-exts</option>.</para>
-
-         <para>New reserved words/symbols: <literal>rec</literal>,
-         <literal>proc</literal>, <literal>-&lt;</literal>,
-         <literal>&gt;-</literal>, <literal>-&lt;&lt;</literal>,
-         <literal>&gt;&gt;-</literal>.</para>
-
-         <para>Other syntax stolen: <literal>(|</literal>,
-         <literal>|)</literal>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term>
-          <option>-XGenerics</option>
-          <indexterm><primary><option>-XGenerics</option></primary></indexterm>
-        </term>
-       <listitem>
-         <para>See <xref linkend="generic-classes"/>.  Independent of
-          <option>-fglasgow-exts</option>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XNoImplicitPrelude</option></term>
-       <listitem>
-         <para><indexterm><primary>-XNoImplicitPrelude
-          option</primary></indexterm> GHC normally imports
-          <filename>Prelude.hi</filename> files for you.  If you'd
-          rather it didn't, then give it a
-          <option>-XNoImplicitPrelude</option> option.  The idea is
-          that you can then import a Prelude of your own.  (But don't
-          call it <literal>Prelude</literal>; the Haskell module
-          namespace is flat, and you must not conflict with any
-          Prelude module.)</para>
-
-         <para>Even though you have not imported the Prelude, most of
-          the built-in syntax still refers to the built-in Haskell
-          Prelude types and values, as specified by the Haskell
-          Report.  For example, the type <literal>[Int]</literal>
-          still means <literal>Prelude.[] Int</literal>; tuples
-          continue to refer to the standard Prelude tuples; the
-          translation for list comprehensions continues to use
-          <literal>Prelude.map</literal> etc.</para>
-
-         <para>However, <option>-XNoImplicitPrelude</option> does
-         change the handling of certain built-in syntax: see <xref
-         linkend="rebindable-syntax"/>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XImplicitParams</option></term>
-       <listitem>
-         <para>Enables implicit parameters (see <xref
-         linkend="implicit-parameters"/>).  Currently also implied by 
-         <option>-fglasgow-exts</option>.</para>
-
-         <para>Syntax stolen:
-         <literal>?<replaceable>varid</replaceable></literal>,
-         <literal>%<replaceable>varid</replaceable></literal>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XOverloadedStrings</option></term>
-       <listitem>
-         <para>Enables overloaded string literals (see <xref
-         linkend="overloaded-strings"/>).</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XScopedTypeVariables</option></term>
-       <listitem>
-         <para>Enables lexically-scoped type variables (see <xref
-         linkend="scoped-type-variables"/>).  Implied by
-         <option>-fglasgow-exts</option>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XTemplateHaskell</option></term>
-       <listitem>
-         <para>Enables Template Haskell (see <xref
-         linkend="template-haskell"/>).  This flag must
-         be given explicitly; it is no longer implied by
-         <option>-fglasgow-exts</option>.</para>
-
-         <para>Syntax stolen: <literal>[|</literal>,
-         <literal>[e|</literal>, <literal>[p|</literal>,
-         <literal>[d|</literal>, <literal>[t|</literal>,
-         <literal>$(</literal>,
-         <literal>$<replaceable>varid</replaceable></literal>.</para>
-       </listitem>
-      </varlistentry>
-
-      <varlistentry>
-       <term><option>-XQuasiQuotes</option></term>
-       <listitem>
-         <para>Enables quasiquotation (see <xref
-         linkend="th-quasiquotation"/>).</para>
-
-         <para>Syntax stolen:
-         <literal>[:<replaceable>varid</replaceable>|</literal>.</para>
-       </listitem>
-      </varlistentry>
-
-    </variablelist>
   </sect1>
 
 <!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
 <sect1 id="primitives">
   <title>Unboxed types and primitive operations</title>
 
-<para>GHC is built on a raft of primitive data types and operations.
+<para>GHC is built on a raft of primitive data types and operations;
+"primitive" in the sense that they cannot be defined in Haskell itself.
 While you really can use this stuff to write fast code,
   we generally find it a lot less painful, and more satisfying in the
   long run, to use higher-level language features and libraries.  With
@@ -316,28 +107,21 @@ While you really can use this stuff to write fast code,
   unboxed version in any case.  And if it isn't, we'd like to know
   about it.</para>
 
-<para>We do not currently have good, up-to-date documentation about the
-primitives, perhaps because they are mainly intended for internal use.
-There used to be a long section about them here in the User Guide, but it
-became out of date, and wrong information is worse than none.</para>
-
-<para>The Real Truth about what primitive types there are, and what operations
-work over those types, is held in the file
-<filename>compiler/prelude/primops.txt.pp</filename>.
-This file is used directly to generate GHC's primitive-operation definitions, so
-it is always correct!  It is also intended for processing into text.</para>
-
-<para>Indeed,
-the result of such processing is part of the description of the 
- <ulink
-      url="http://www.haskell.org/ghc/docs/papers/core.ps.gz">External
-        Core language</ulink>.
-So that document is a good place to look for a type-set version.
-We would be very happy if someone wanted to volunteer to produce an XML
-back end to the program that processes <filename>primops.txt</filename> so that
-we could include the results here in the User Guide.</para>
-
-<para>What follows here is a brief summary of some main points.</para>
+<para>All these primitive data types and operations are exported by the 
+library <literal>GHC.Prim</literal>, for which there is 
+<ulink url="../libraries/base/GHC.Prim.html">detailed online documentation</ulink>.
+(This documentation is generated from the file <filename>compiler/prelude/primops.txt.pp</filename>.)
+</para>
+<para>
+If you want to mention any of the primitive data types or operations in your
+program, you must first import <literal>GHC.Prim</literal> to bring them
+into scope.  Many of them have names ending in "&num;", and to mention such
+names you need the <option>-XMagicHash</option> extension (<xref linkend="magic-hash"/>).
+</para>
+
+<para>The primops make extensive use of <link linkend="glasgow-unboxed">unboxed types</link> 
+and <link linkend="unboxed-tuples">unboxed tuples</link>, which
+we briefly summarise here. </para>
   
 <sect2 id="glasgow-unboxed">
 <title>Unboxed types
@@ -366,26 +150,15 @@ would use in C: <literal>Int&num;</literal> (long int),
 know and love&mdash;usually one instruction.
 </para>
 
-<para> For some primitive types we have special syntax for literals.
-Anything that would be an integer lexeme followed by a
-<literal>&num;</literal> is an <literal>Int&num;</literal> literal, e.g.
-<literal>32&num;</literal> and <literal>-0x3A&num;</literal>. Likewise,
-any non-negative integer literal followed by
-<literal>&num;&num;</literal> is a <literal>Word&num;</literal> literal.
-Likewise, any floating point literal followed by a
-<literal>&num;</literal> is a <literal>Float&num;</literal> literal, and
-followed by <literal>&num;&num;</literal> is a
-<literal>Double&num;</literal>. Finally, a string literal followed by a
-<literal>&num;</literal>, e.g. <literal>&quot;foo&quot;&num;</literal>,
-is a <literal>Addr&num;</literal> literal.
-</para>
-
 <para>
 Primitive (unboxed) types cannot be defined in Haskell, and are
 therefore built into the language and compiler.  Primitive types are
 always unlifted; that is, a value of a primitive type cannot be
-bottom.  We use the convention that primitive types, values, and
-operations have a <literal>&num;</literal> suffix.
+bottom.  We use the convention (but it is only a convention) 
+that primitive types, values, and
+operations have a <literal>&num;</literal> suffix (see <xref linkend="magic-hash"/>).
+For some primitive types we have special syntax for literals, also
+described in the <link linkend="magic-hash">same section</link>.
 </para>
 
 <para>
@@ -437,22 +210,20 @@ in a <emphasis>top-level</emphasis> binding.
 in a <emphasis>recursive</emphasis> binding.
 </para></listitem>
 <listitem><para> You may bind unboxed variables in a (non-recursive,
-non-top-level) pattern binding, but any such variable causes the entire
-pattern-match
-to become strict.  For example:
+non-top-level) pattern binding, but you must make any such pattern-match
+strict.  For example, rather than:
 <programlisting>
   data Foo = Foo Int Int#
 
   f x = let (Foo a b, w) = ..rhs.. in ..body..
 </programlisting>
-Since <literal>b</literal> has type <literal>Int#</literal>, the entire pattern
-match
-is strict, and the program behaves as if you had written
+you must write:
 <programlisting>
   data Foo = Foo Int Int#
 
-  f x = case ..rhs.. of { (Foo a b, w) -> ..body.. }
+  f x = let !(Foo a b, w) = ..rhs.. in ..body..
 </programlisting>
+since <literal>b</literal> has type <literal>Int#</literal>.
 </para>
 </listitem>
 </itemizedlist>
@@ -562,8 +333,146 @@ Indeed, the bindings can even be recursive.
 <sect1 id="syntax-extns">
 <title>Syntactic extensions</title>
  
+    <sect2 id="unicode-syntax">
+      <title>Unicode syntax</title>
+      <para>The language
+      extension <option>-XUnicodeSyntax</option><indexterm><primary><option>-XUnicodeSyntax</option></primary></indexterm>
+      enables Unicode characters to be used to stand for certain ASCII
+      character sequences.  The following alternatives are provided:</para>
+
+      <informaltable>
+       <tgroup cols="2" align="left" colsep="1" rowsep="1">
+         <thead>
+           <row>
+             <entry>ASCII</entry>
+              <entry>Unicode alternative</entry>
+             <entry>Code point</entry>
+             <entry>Name</entry>
+           </row>
+         </thead>
+         <tbody>
+           <row>
+             <entry><literal>::</literal></entry>
+             <entry>::</entry> <!-- no special char, apparently -->
+              <entry>0x2237</entry>
+             <entry>PROPORTION</entry>
+           </row>
+          </tbody>
+         <tbody>
+           <row>
+             <entry><literal>=&gt;</literal></entry>
+             <entry>&rArr;</entry>
+             <entry>0x21D2</entry>
+              <entry>RIGHTWARDS DOUBLE ARROW</entry>
+           </row>
+          </tbody>
+         <tbody>
+           <row>
+             <entry><literal>forall</literal></entry>
+             <entry>&forall;</entry>
+             <entry>0x2200</entry>
+              <entry>FOR ALL</entry>
+           </row>
+          </tbody>
+         <tbody>
+           <row>
+             <entry><literal>-&gt;</literal></entry>
+             <entry>&rarr;</entry>
+             <entry>0x2192</entry>
+              <entry>RIGHTWARDS ARROW</entry>
+           </row>
+          </tbody>
+         <tbody>
+           <row>
+             <entry><literal>&lt;-</literal></entry>
+             <entry>&larr;</entry>
+             <entry>0x2190</entry>
+              <entry>LEFTWARDS ARROW</entry>
+           </row>
+          </tbody>
+         <tbody>
+           <row>
+             <entry>..</entry>
+             <entry>&hellip;</entry>
+             <entry>0x22EF</entry>
+             <entry>MIDLINE HORIZONTAL ELLIPSIS</entry>
+           </row>
+          </tbody>
+        </tgroup>
+      </informaltable>
+    </sect2>
+
+    <sect2 id="magic-hash">
+      <title>The magic hash</title>
+      <para>The language extension <option>-XMagicHash</option> allows "&num;" as a
+       postfix modifier to identifiers.  Thus, "x&num;" is a valid variable, and "T&num;" is
+       a valid type constructor or data constructor.</para>
+
+      <para>The hash sign does not change sematics at all.  We tend to use variable
+       names ending in "&num;" for unboxed values or types (e.g. <literal>Int&num;</literal>), 
+       but there is no requirement to do so; they are just plain ordinary variables.
+       Nor does the <option>-XMagicHash</option> extension bring anything into scope.
+       For example, to bring <literal>Int&num;</literal> into scope you must 
+       import <literal>GHC.Prim</literal> (see <xref linkend="primitives"/>); 
+       the <option>-XMagicHash</option> extension
+       then allows you to <emphasis>refer</emphasis> to the <literal>Int&num;</literal>
+       that is now in scope.</para>
+      <para> The <option>-XMagicHash</option> also enables some new forms of literals (see <xref linkend="glasgow-unboxed"/>):
+       <itemizedlist> 
+         <listitem><para> <literal>'x'&num;</literal> has type <literal>Char&num;</literal></para> </listitem>
+         <listitem><para> <literal>&quot;foo&quot;&num;</literal> has type <literal>Addr&num;</literal></para> </listitem>
+         <listitem><para> <literal>3&num;</literal> has type <literal>Int&num;</literal>. In general,
+         any Haskell 98 integer lexeme followed by a <literal>&num;</literal> is an <literal>Int&num;</literal> literal, e.g.
+            <literal>-0x3A&num;</literal> as well as <literal>32&num;</literal></para>.</listitem>
+         <listitem><para> <literal>3&num;&num;</literal> has type <literal>Word&num;</literal>. In general,
+         any non-negative Haskell 98 integer lexeme followed by <literal>&num;&num;</literal> 
+             is a <literal>Word&num;</literal>. </para> </listitem>
+         <listitem><para> <literal>3.2&num;</literal> has type <literal>Float&num;</literal>.</para> </listitem>
+         <listitem><para> <literal>3.2&num;&num;</literal> has type <literal>Double&num;</literal></para> </listitem>
+         </itemizedlist>
+      </para>
+   </sect2>
+
+    <sect2 id="new-qualified-operators">
+      <title>New qualified operator syntax</title>
+
+      <para>A new syntax for referencing qualified operators is
+        planned to be introduced by Haskell', and is enabled in GHC
+        with
+        the <option>-XNewQualifiedOperators</option><indexterm><primary><option>-XNewQualifiedOperators</option></primary></indexterm>
+        option.  In the new syntax, the prefix form of a qualified
+        operator is
+        written <literal><replaceable>module</replaceable>.(<replaceable>symbol</replaceable>)</literal>
+        (in Haskell 98 this would
+        be <literal>(<replaceable>module</replaceable>.<replaceable>symbol</replaceable>)</literal>),
+        and the infix form is
+        written <literal>`<replaceable>module</replaceable>.(<replaceable>symbol</replaceable>)`</literal>
+        (in Haskell 98 this would
+        be <literal>`<replaceable>module</replaceable>.<replaceable>symbol</replaceable>`</literal>.
+        For example:
+<programlisting>
+  add x y = Prelude.(+) x y
+  subtract y = (`Prelude.(-)` y)
+</programlisting>
+        The new form of qualified operators is intended to regularise
+        the syntax by eliminating odd cases
+        like <literal>Prelude..</literal>.  For example,
+        when <literal>NewQualifiedOperators</literal> is on, it is possible to
+        write the enumerated sequence <literal>[Monday..]</literal>
+        without spaces, whereas in Haskell 98 this would be a
+        reference to the operator &lsquo;<literal>.</literal>&lsquo;
+        from module <literal>Monday</literal>.</para>
+
+      <para>When <option>-XNewQualifiedOperators</option> is on, the old Haskell
+        98 syntax for qualified operators is not accepted, so this
+        option may cause existing Haskell 98 code to break.</para>
+
+    </sect2>
+        
+
     <!-- ====================== HIERARCHICAL MODULES =======================  -->
 
+
     <sect2 id="hierarchical-modules">
       <title>Hierarchical Modules</title>
 
@@ -1018,11 +927,6 @@ and improve termination (Section 3.2 of the paper).
 </para>
 
 <para>
-The web page: <ulink url="http://www.cse.ogi.edu/PacSoft/projects/rmb/">http://www.cse.ogi.edu/PacSoft/projects/rmb/</ulink>
-contains up to date information on recursive monadic bindings.
-</para>
-
-<para>
 Historical note: The old implementation of the mdo-notation (and most
 of the existing documents) used the name
 <literal>MonadRec</literal> for the class and the corresponding library.
@@ -1102,6 +1006,7 @@ This name is not supported by GHC.
        paper <ulink url="http://research.microsoft.com/~simonpj/papers/list-comp">
          Comprehensive comprehensions: comprehensions with "order by" and "group by"</ulink>,
     except that the syntax we use differs slightly from the paper.</para>
+<para>The extension is enabled with the flag <option>-XTransformListComp</option>.</para>
 <para>Here is an example: 
 <programlisting>
 employees = [ ("Simon", "MS", 80)
@@ -1247,21 +1152,28 @@ output = [ x
    <!-- ===================== REBINDABLE SYNTAX ===================  -->
 
 <sect2 id="rebindable-syntax">
-<title>Rebindable syntax</title>
-
-      <para>GHC allows most kinds of built-in syntax to be rebound by
-      the user, to facilitate replacing the <literal>Prelude</literal>
-      with a home-grown version, for example.</para>
-
-            <para>You may want to define your own numeric class
+<title>Rebindable syntax and the implicit Prelude import</title>
+
+ <para><indexterm><primary>-XNoImplicitPrelude
+ option</primary></indexterm> GHC normally imports
+ <filename>Prelude.hi</filename> files for you.  If you'd
+ rather it didn't, then give it a
+ <option>-XNoImplicitPrelude</option> option.  The idea is
+ that you can then import a Prelude of your own.  (But don't
+ call it <literal>Prelude</literal>; the Haskell module
+ namespace is flat, and you must not conflict with any
+ Prelude module.)</para>
+
+            <para>Suppose you are importing a Prelude of your own
+             in order to define your own numeric class
             hierarchy.  It completely defeats that purpose if the
             literal "1" means "<literal>Prelude.fromInteger
             1</literal>", which is what the Haskell Report specifies.
-            So the <option>-XNoImplicitPrelude</option> flag causes
+            So the <option>-XNoImplicitPrelude</option> 
+             flag <emphasis>also</emphasis> causes
             the following pieces of built-in syntax to refer to
             <emphasis>whatever is in scope</emphasis>, not the Prelude
             versions:
-
            <itemizedlist>
              <listitem>
                <para>An integer literal <literal>368</literal> means
@@ -1333,8 +1245,9 @@ fromInteger :: Integer -> Bool -> Bool
 <title>Postfix operators</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
+  The <option>-XPostfixOperators</option> flag enables 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>
@@ -1351,10 +1264,6 @@ 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>
 
@@ -1392,7 +1301,7 @@ it is not clear which of the two types is intended.
 </para>
 <para>
 Haskell 98 regards all four as ambiguous, but with the
-<option>-fdisambiguate-record-fields</option> flag, GHC will accept
+<option>-XDisambiguateRecordFields</option> flag, GHC will accept
 the former two.  The rules are precisely the same as those for instance
 declarations in Haskell 98, where the method names on the left-hand side 
 of the method bindings in an instance declaration refer unambiguously
@@ -1410,7 +1319,7 @@ records from different modules that use the same field name.
 </title>
 
 <para>
-Record puns are enabled by the flag <literal>-XRecordPuns</literal>.
+Record puns are enabled by the flag <literal>-XNamedFieldPuns</literal>.
 </para>
 
 <para>
@@ -1568,6 +1477,167 @@ necessary to enable them.
 </para>
 </sect2>
 
+<sect2 id="package-imports">
+  <title>Package-qualified imports</title>
+
+  <para>With the <option>-XPackageImports</option> flag, GHC allows
+  import declarations to be qualified by the package name that the
+    module is intended to be imported from.  For example:</para>
+
+<programlisting>
+import "network" Network.Socket
+</programlisting>
+  
+  <para>would import the module <literal>Network.Socket</literal> from
+    the package <literal>network</literal> (any version).  This may
+    be used to disambiguate an import when the same module is
+    available from multiple packages, or is present in both the
+    current package being built and an external package.</para>
+
+  <para>Note: you probably don't need to use this feature, it was
+    added mainly so that we can build backwards-compatible versions of
+    packages when APIs change.  It can lead to fragile dependencies in
+    the common case: modules occasionally move from one package to
+    another, rendering any package-qualified imports broken.</para>
+</sect2>
+
+<sect2 id="syntax-stolen">
+<title>Summary of stolen syntax</title>
+
+    <para>Turning on an option that enables special syntax
+    <emphasis>might</emphasis> cause working Haskell 98 code to fail
+    to compile, perhaps because it uses a variable name which has
+    become a reserved word.  This section lists the syntax that is
+    "stolen" by language extensions.
+     We use
+    notation and nonterminal names from the Haskell 98 lexical syntax
+    (see the Haskell 98 Report).  
+    We only list syntax changes here that might affect
+    existing working programs (i.e. "stolen" syntax).  Many of these
+    extensions will also enable new context-free syntax, but in all
+    cases programs written to use the new syntax would not be
+    compilable without the option enabled.</para>
+
+<para>There are two classes of special
+    syntax:
+
+    <itemizedlist>
+      <listitem>
+       <para>New reserved words and symbols: character sequences
+        which are no longer available for use as identifiers in the
+        program.</para>
+      </listitem>
+      <listitem>
+       <para>Other special syntax: sequences of characters that have
+       a different meaning when this particular option is turned
+       on.</para>
+      </listitem>
+    </itemizedlist>
+    
+The following syntax is stolen:
+
+    <variablelist>
+      <varlistentry>
+       <term>
+          <literal>forall</literal>
+          <indexterm><primary><literal>forall</literal></primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen (in types) by: <option>-XScopedTypeVariables</option>,
+           <option>-XLiberalTypeSynonyms</option>,
+           <option>-XRank2Types</option>,
+           <option>-XRankNTypes</option>,
+           <option>-XPolymorphicComponents</option>,
+           <option>-XExistentialQuantification</option>
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+          <literal>mdo</literal>
+          <indexterm><primary><literal>mdo</literal></primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XRecursiveDo</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+          <literal>foreign</literal>
+          <indexterm><primary><literal>foreign</literal></primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XForeignFunctionInterface</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+          <literal>rec</literal>,
+         <literal>proc</literal>, <literal>-&lt;</literal>,
+         <literal>&gt;-</literal>, <literal>-&lt;&lt;</literal>,
+         <literal>&gt;&gt;-</literal>, and <literal>(|</literal>,
+         <literal>|)</literal> brackets
+          <indexterm><primary><literal>proc</literal></primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XArrows</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+         <literal>?<replaceable>varid</replaceable></literal>,
+         <literal>%<replaceable>varid</replaceable></literal>
+          <indexterm><primary>implicit parameters</primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XImplicitParams</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+         <literal>[|</literal>,
+         <literal>[e|</literal>, <literal>[p|</literal>,
+         <literal>[d|</literal>, <literal>[t|</literal>,
+         <literal>$(</literal>,
+         <literal>$<replaceable>varid</replaceable></literal>
+          <indexterm><primary>Template Haskell</primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XTemplateHaskell</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+         <literal>[:<replaceable>varid</replaceable>|</literal>
+          <indexterm><primary>quasi-quotation</primary></indexterm>
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XQuasiQuotes</option>,
+         </para></listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+             <replaceable>varid</replaceable>{<literal>&num;</literal>},
+             <replaceable>char</replaceable><literal>&num;</literal>,      
+             <replaceable>string</replaceable><literal>&num;</literal>,    
+             <replaceable>integer</replaceable><literal>&num;</literal>,    
+             <replaceable>float</replaceable><literal>&num;</literal>,    
+             <replaceable>float</replaceable><literal>&num;&num;</literal>,    
+             <literal>(&num;</literal>, <literal>&num;)</literal>,         
+       </term>
+       <listitem><para>
+       Stolen by: <option>-XMagicHash</option>,
+         </para></listitem>
+      </varlistentry>
+    </variablelist>
+</para>
+</sect2>
 </sect1>
 
 
@@ -1668,9 +1738,12 @@ to be written infix, very much like expressions.  More specifically:
 <title>Liberalised type synonyms</title>
 
 <para>
-Type synonyms are like macros at the type level, and
+Type synonyms are like macros at the type level, but Haskell 98 imposes many rules
+on individual synonym declarations.
+With the <option>-XLiberalTypeSynonyms</option> extension,
 GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
-That means that GHC can be very much more liberal about type synonyms than Haskell 98:
+That means that GHC can be very much more liberal about type synonyms than Haskell 98. 
+
 <itemizedlist>
 <listitem> <para>You can write a <literal>forall</literal> (including overloading)
 in a type synonym, thus:
@@ -1687,7 +1760,8 @@ in a type synonym, thus:
 </listitem>
 
 <listitem><para>
-You can write an unboxed tuple in a type synonym:
+If you also use <option>-XUnboxedTuples</option>, 
+you can write an unboxed tuple in a type synonym:
 <programlisting>
   type Pr = (# Int, Int #)
 
@@ -1985,15 +2059,28 @@ main = do
     display (inc (inc counterB))   -- prints "##"
 </programlisting>
 
-At the moment, record update syntax is only supported for Haskell 98 data types,
-so the following function does <emphasis>not</emphasis> work:
-
+Record update syntax is supported for existentials (and GADTs):
 <programlisting>
--- This is invalid; use explicit NewCounter instead for now
 setTag :: Counter a -> a -> Counter a
 setTag obj t = obj{ tag = t }
 </programlisting>
+The rule for record update is this: <emphasis>
+the types of the updated fields may
+mention only the universally-quantified type variables
+of the data constructor.  For GADTs, the field may mention only types
+that appear as a simple type-variable argument in the constructor's result
+type</emphasis>.  For example:
+<programlisting>
+data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b } -- c is existential
+upd1 t x = t { f1=x }   -- OK:   upd1 :: T a b -> a' -> T a' b
+upd2 t x = t { f3=x }   -- BAD   (f3's type mentions c, which is
+                        --        existentially quantified)
 
+data G a b where { G1 { g1::a, g2::c } :: G a [c] }
+upd3 g x = g { g1=x }   -- OK:   upd3 :: G a b -> c -> G c b
+upd4 g x = g { g2=x }   -- BAD (f2's type mentions c, which is not a simple
+                        --      type-variable argument in G1's result type)
+</programlisting>
 </para>
 
 </sect3>
@@ -2265,16 +2352,46 @@ otherwise is a <emphasis>generalised</emphasis> data type (<xref linkend="gadt"/
 </para></listitem>
 
 <listitem><para>
+As with other type signatures, you can give a single signature for several data constructors.
+In this example we give a single signature for <literal>T1</literal> and <literal>T2</literal>:
+<programlisting>
+  data T a where
+    T1,T2 :: a -> T a
+    T3 :: T a
+</programlisting>
+</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:
+In particular, the type variable(s) in the "<literal>data T a where</literal>" header 
+have no scope, and different constructors may have different universally-quantified type variables:
+<programlisting>
+  data T a where        -- The 'a' has no scope
+    T1,T2 :: b -> T b   -- Means forall b. b -> T b
+    T3 :: T a           -- Means forall a. T a
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+A constructor signature may mention type class constraints, which can differ for
+different constructors.  For example, this is fine:
 <programlisting>
   data T a where
-    T1 :: Eq b => b -> T b
+    T1 :: Eq b => b -> b -> T b
     T2 :: (Show c, Ix c) => c -> [c] -> T c
 </programlisting>
+When patten matching, these constraints are made available to discharge constraints
+in the body of the match. For example:
+<programlisting>
+  f :: T a -> String
+  f (T1 x y) | x==y      = "yes"
+             | otherwise = "no"
+  f (T2 a b)             = show a
+</programlisting>
+Note that <literal>f</literal> is not overloaded; the <literal>Eq</literal> constraint arising
+from the use of <literal>==</literal> is discharged by the pattern match on <literal>T1</literal>
+and similarly the <literal>Show</literal> constraint arising from the use of <literal>show</literal>.
 </para></listitem>
 
 <listitem><para>
@@ -2286,12 +2403,12 @@ have no scope.  Indeed, one can write a kind signature instead:
 </programlisting>
 or even a mixture of the two:
 <programlisting>
-  data Foo a :: (* -> *) -> * where ...
+  data Bar 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 ...
+  data Bar a (b :: * -> *) where ...
 </programlisting>
 </para></listitem>
 
@@ -2322,27 +2439,48 @@ declaration.   For example, these two declarations are equivalent
 </para></listitem>
 
 <listitem><para>
+The type signature may have quantified type variables that do not appear
+in the result type:
+<programlisting>
+  data Foo where
+     MkFoo :: a -> (a->Bool) -> Foo
+     Nil   :: Foo
+</programlisting>
+Here the type variable <literal>a</literal> does not appear in the result type
+of either constructor.  
+Although it is universally quantified in the type of the constructor, such
+a type variable is often called "existential".  
+Indeed, the above declaration declares precisely the same type as 
+the <literal>data Foo</literal> in <xref linkend="existential-quantification"/>.
+</para><para>
+The type may contain a class context too, of course:
+<programlisting>
+  data Showable where
+    MkShowable :: Show a => a -> Showable
+</programlisting>
+</para></listitem>
+
+<listitem><para>
 You can use record syntax on a GADT-style data type declaration:
 
 <programlisting>
   data Person where
-      Adult { name :: String, children :: [Person] } :: Person
-      Child { name :: String } :: Person
+      Adult :: { name :: String, children :: [Person] } -> Person
+      Child :: Show a => { name :: !String, funny :: a } -> 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>
-<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 example
-<programlisting>
-  aPerson = Adult { name = "Fred", children = [] }
+The <literal>Child</literal> constructor above shows that the signature
+may have a context, existentially-quantified variables, and strictness annotations, 
+just as in the non-record case.  (NB: the "type" that follows the double-colon
+is not really a type, because of the record syntax and strictness annotations.
+A "type" of this form can appear only in a constructor signature.)
+</para></listitem>
 
-  shortName :: Person -> Bool
-  hasChildren (Adult { children = kids }) = not (null kids)
-  hasChildren (Child {})                  = False
-</programlisting>
+<listitem><para> 
+Record updates are allowed with GADT-style declarations, 
+only fields that have the following property: the type of the field
+mentions no existential type variables.
 </para></listitem>
 
 <listitem><para> 
@@ -2436,11 +2574,17 @@ The result type of each constructor must begin with the type constructor being d
 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>
+the <literal>ty</literal> need not be a type variable (e.g. the <literal>Lit</literal>
 constructor).
 </para></listitem>
 
 <listitem><para>
+It's is permitted to declare an ordinary algebraic data type using GADT-style syntax.
+What makes a GADT into a GADT is not the syntax, but rather the presence of data constructors
+whose result type is not just <literal>T a b</literal>.
+</para></listitem>
+
+<listitem><para>
 You cannot use a <literal>deriving</literal> clause for a GADT; only for
 an ordinary data type.
 </para></listitem>
@@ -2476,6 +2620,23 @@ their selector functions actually have different types:
 </programlisting>
 </para></listitem>
 
+<listitem><para>
+When pattern-matching against data constructors drawn from a GADT, 
+for example in a <literal>case</literal> expression, the following rules apply:
+<itemizedlist>
+<listitem><para>The type of the scrutinee must be rigid.</para></listitem>
+<listitem><para>The type of the entire <literal>case</literal> expression must be rigid.</para></listitem>
+<listitem><para>The type of any free variable mentioned in any of
+the <literal>case</literal> alternatives must be rigid.</para></listitem>
+</itemizedlist>
+A type is "rigid" if it is completely known to the compiler at its binding site.  The easiest
+way to ensure that a variable a rigid type is to give it a type signature.
+For more precise details see <ulink url="http://research.microsoft.com/%7Esimonpj/papers/gadt">
+Simple unification-based type inference for GADTs
+</ulink>. The criteria implemented by GHC are given in the Appendix.
+
+</para></listitem>
+
 </itemizedlist>
 </para>
 
@@ -2571,7 +2732,7 @@ GHC always treats the <emphasis>last</emphasis> parameter of the instance
 
 
 <sect2 id="deriving-typeable">
-<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
+<title>Deriving clause for extra classes (<literal>Typeable</literal>, <literal>Data</literal>, etc)</title>
 
 <para>
 Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type 
@@ -2581,11 +2742,11 @@ 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>-XDeriveDataTypeable</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.
+GHC extends this list with several more classes that may be automatically derived:
+<itemizedlist>
+<listitem><para> With <option>-XDeriveDataTypeable</option>, you can derive instances of the classes
+<literal>Typeable</literal>, and <literal>Data</literal>, defined in the library
+modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively.
 </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>.
@@ -2601,6 +2762,26 @@ In other cases, there is nothing to stop the programmer writing a <literal>Typab
 class, whose kind suits that of the data type constructor, and
 then writing the data type instance by hand.
 </para>
+</listitem>
+
+<listitem><para> With <option>-XDeriveFunctor</option>, you can derive instances of 
+the class <literal>Functor</literal>,
+defined in <literal>GHC.Base</literal>.
+</para></listitem>
+
+<listitem><para> With <option>-XDeriveFoldable</option>, you can derive instances of 
+the class <literal>Foldable</literal>,
+defined in <literal>Data.Foldable</literal>.
+</para></listitem>
+
+<listitem><para> With <option>-XDeriveTraversable</option>, you can derive instances of 
+the class <literal>Traversable</literal>,
+defined in <literal>Data.Traversable</literal>.
+</para></listitem>
+</itemizedlist>
+In each case the appropriate class must be in scope before it 
+can be mentioned in the <literal>deriving</literal> clause.
+</para>
 </sect2>
 
 <sect2 id="newtype-deriving">
@@ -3219,9 +3400,6 @@ sets of instance declarations.
 <sect2 id="instance-decls">
 <title>Instance declarations</title>
 
-<sect3 id="instance-rules">
-<title>Relaxed rules for instance declarations</title>
-
 <para>An instance declaration has the form
 <screen>
   instance ( <replaceable>assertion</replaceable><subscript>1</subscript>, ..., <replaceable>assertion</replaceable><subscript>n</subscript>) =&gt; <replaceable>class</replaceable> <replaceable>type</replaceable><subscript>1</subscript> ... <replaceable>type</replaceable><subscript>m</subscript> where ...
@@ -3231,19 +3409,73 @@ The part before the "<literal>=&gt;</literal>" is the
 "<literal>=&gt;</literal>" is the <emphasis>head</emphasis> of the instance declaration.
 </para>
 
+<sect3 id="flexible-instance-head">
+<title>Relaxed rules for the instance head</title>
+
 <para>
 In Haskell 98 the head of an instance declaration
 must be of the form <literal>C (T a1 ... an)</literal>, where
-<literal>C</literal> is the class, <literal>T</literal> is a type constructor,
+<literal>C</literal> is the class, <literal>T</literal> is a data type constructor,
 and the <literal>a1 ... an</literal> are distinct type variables.
-Furthermore, the assertions in the context of the instance declaration
+GHC relaxes these rules in two ways.
+<itemizedlist>
+<listitem>
+<para>
+The <option>-XFlexibleInstances</option> flag allows the head of the instance
+declaration to mention arbitrary nested types.
+For example, this becomes a legal instance declaration
+<programlisting>
+  instance C (Maybe Int) where ...
+</programlisting>
+See also the <link linkend="instance-overlap">rules on overlap</link>.
+</para></listitem>
+<listitem><para>
+With the <option>-XTypeSynonymInstances</option> flag, instance heads may use type
+synonyms. As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition.  For example:
+
+
+<programlisting>
+  type Point = (Int,Int)
+  instance C Point   where ...
+  instance C [Point] where ...
+</programlisting>
+
+
+is legal.  However, if you added
+
+
+<programlisting>
+  instance C (Int,Int) where ...
+</programlisting>
+
+
+as well, then the compiler will complain about the overlapping
+(actually, identical) instance declarations.  As always, type synonyms
+must be fully applied.  You cannot, for example, write:
+
+<programlisting>
+  type P a = [[a]]
+  instance Monad P where ...
+</programlisting>
+
+</para></listitem>
+</itemizedlist>
+</para>
+</sect3>
+
+<sect3 id="instance-rules">
+<title>Relaxed rules for instance contexts</title>
+
+<para>In Haskell 98, the assertions in the context of the instance declaration
 must be of the form <literal>C a</literal> where <literal>a</literal>
 is a type variable that occurs in the head.
 </para>
+
 <para>
-The <option>-XFlexibleInstances</option> flag loosens these restrictions
-considerably.  Firstly, multi-parameter type classes are permitted.  Secondly,
-the context and head of the instance declaration can each consist of arbitrary
+The <option>-XFlexibleContexts</option> flag relaxes this rule, as well
+as the corresponding rule for type signatures (see <xref linkend="flexible-contexts"/>).
+With this flag the context of the instance declaration can each consist of arbitrary
 (well-kinded) assertions <literal>(C t1 ... tn)</literal> subject only to the
 following rules:
 <orderedlist>
@@ -3269,7 +3501,7 @@ corresponding type in the instance declaration.
 These restrictions ensure that context reduction terminates: each reduction
 step makes the problem smaller by at least one
 constructor.  Both the Paterson Conditions and the Coverage Condition are lifted 
-if you give the <option>-fallow-undecidable-instances</option> 
+if you give the <option>-XUndecidableInstances</option> 
 flag (<xref linkend="undecidable-instances"/>).
 You can find lots of background material about the reason for these
 restrictions in the paper <ulink
@@ -3467,14 +3699,36 @@ Notice that we gave a type signature to <literal>f</literal>, so GHC had to
 <emphasis>check</emphasis> that <literal>f</literal> has the specified type.  
 Suppose instead we do not give a type signature, asking GHC to <emphasis>infer</emphasis>
 it instead.  In this case, GHC will refrain from
-simplifying the constraint <literal>C Int [Int]</literal> (for the same reason
+simplifying the constraint <literal>C Int [b]</literal> (for the same reason
 as before) but, rather than rejecting the program, it will infer the type
 <programlisting>
-  f :: C Int b => [b] -> [b]
+  f :: C Int [b] => [b] -> [b]
 </programlisting>
 That postpones the question of which instance to pick to the 
 call site for <literal>f</literal>
 by which time more is known about the type <literal>b</literal>.
+You can write this type signature yourself if you use the 
+<link linkend="flexible-contexts"><option>-XFlexibleContexts</option></link>
+flag.
+</para>
+<para>
+Exactly the same situation can arise in instance declarations themselves.  Suppose we have
+<programlisting>
+  class Foo a where
+     f :: a -> a
+  instance Foo [b] where
+     f x = ...
+</programlisting>
+and, as before, the constraint <literal>C Int [b]</literal> arises from <literal>f</literal>'s
+right hand side.  GHC will reject the instance, complaining as before that it does not know how to resolve
+the constraint <literal>C Int [b]</literal>, because it matches more than one instance
+declaration.  The solution is to postpone the choice by adding the constraint to the context
+of the instance declaration, thus:
+<programlisting>
+  instance C Int [b] => Foo [b] where
+     f x = ...
+</programlisting>
+(You need <link linkend="instance-rules"><option>-XFlexibleInstances</option></link> to do this.)
 </para>
 <para>
 The willingness to be overlapped or incoherent is a property of 
@@ -3519,47 +3773,6 @@ hard to pin down.)  We are interested to receive feedback on these points.
 </para>
 </sect3>
 
-<sect3>
-<title>Type synonyms in the instance head</title>
-
-<para>
-<emphasis>Unlike Haskell 98, instance heads may use type
-synonyms</emphasis>.  (The instance "head" is the bit after the "=>" in an instance decl.)
-As always, using a type synonym is just shorthand for
-writing the RHS of the type synonym definition.  For example:
-
-
-<programlisting>
-  type Point = (Int,Int)
-  instance C Point   where ...
-  instance C [Point] where ...
-</programlisting>
-
-
-is legal.  However, if you added
-
-
-<programlisting>
-  instance C (Int,Int) where ...
-</programlisting>
-
-
-as well, then the compiler will complain about the overlapping
-(actually, identical) instance declarations.  As always, type synonyms
-must be fully applied.  You cannot, for example, write:
-
-
-<programlisting>
-  type P a = [[a]]
-  instance Monad P where ...
-</programlisting>
-
-
-This design decision is independent of all the others, and easily
-reversed, but it makes sense to me.
-
-</para>
-</sect3>
 
 
 </sect2>
@@ -3641,6 +3854,706 @@ to work since it gets translated into an equality comparison.
 
 </sect1>
 
+<sect1 id="type-families">
+<title>Type families</title>
+
+<para>
+  <firstterm>Indexed type families</firstterm> are a new GHC extension to
+  facilitate type-level 
+  programming. Type families are a generalisation of <firstterm>associated
+  data types</firstterm> 
+  (&ldquo;<ulink url="http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html">Associated 
+  Types with Class</ulink>&rdquo;, M. Chakravarty, G. Keller, S. Peyton Jones,
+  and S. Marlow. In Proceedings of &ldquo;The 32nd Annual ACM SIGPLAN-SIGACT
+     Symposium on Principles of Programming Languages (POPL'05)&rdquo;, pages
+  1-13, ACM Press, 2005) and <firstterm>associated type synonyms</firstterm>
+  (&ldquo;<ulink url="http://www.cse.unsw.edu.au/~chak/papers/CKP05.html">Type  
+  Associated Type Synonyms</ulink>&rdquo;. M. Chakravarty, G. Keller, and
+  S. Peyton Jones. 
+  In Proceedings of &ldquo;The Tenth ACM SIGPLAN International Conference on
+  Functional Programming&rdquo;, ACM Press, pages 241-253, 2005).  Type families
+  themselves are described in the paper &ldquo;<ulink 
+  url="http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html">Type
+  Checking with Open Type Functions</ulink>&rdquo;, T. Schrijvers,
+  S. Peyton-Jones, 
+  M. Chakravarty, and M. Sulzmann, in Proceedings of &ldquo;ICFP 2008: The
+  13th ACM SIGPLAN International Conference on Functional
+  Programming&rdquo;, ACM Press, pages 51-62, 2008. Type families
+  essentially provide type-indexed data types and named functions on types,
+  which are useful for generic programming and highly parameterised library
+  interfaces as well as interfaces with enhanced static information, much like
+  dependent types. They might also be regarded as an alternative to functional
+  dependencies, but provide a more functional style of type-level programming
+  than the relational style of functional dependencies. 
+</para>
+<para>
+  Indexed type families, or type families for short, are type constructors that
+  represent sets of types. Set members are denoted by supplying the type family
+  constructor with type parameters, which are called <firstterm>type
+  indices</firstterm>. The 
+  difference between vanilla parametrised type constructors and family
+  constructors is much like between parametrically polymorphic functions and
+  (ad-hoc polymorphic) methods of type classes. Parametric polymorphic functions
+  behave the same at all type instances, whereas class methods can change their
+  behaviour in dependence on the class type parameters. Similarly, vanilla type
+  constructors imply the same data representation for all type instances, but
+  family constructors can have varying representation types for varying type
+  indices. 
+</para>
+<para>
+  Indexed type families come in two flavours: <firstterm>data
+    families</firstterm> and <firstterm>type synonym 
+    families</firstterm>. They are the indexed family variants of algebraic
+  data types and type synonyms, respectively. The instances of data families
+  can be data types and newtypes. 
+</para>
+<para>
+  Type families are enabled by the flag <option>-XTypeFamilies</option>.
+  Additional information on the use of type families in GHC is available on
+  <ulink url="http://www.haskell.org/haskellwiki/GHC/Indexed_types">the
+  Haskell wiki page on type families</ulink>.
+</para>
+
+<sect2 id="data-families">
+  <title>Data families</title>
+
+  <para>
+    Data families appear in two flavours: (1) they can be defined on the
+    toplevel 
+    or (2) they can appear inside type classes (in which case they are known as
+    associated types). The former is the more general variant, as it lacks the
+    requirement for the type-indexes to coincide with the class
+    parameters. However, the latter can lead to more clearly structured code and
+    compiler warnings if some type instances were - possibly accidentally -
+    omitted. In the following, we always discuss the general toplevel form first
+    and then cover the additional constraints placed on associated types.
+  </para>
+
+  <sect3 id="data-family-declarations"> 
+    <title>Data family declarations</title>
+
+    <para>
+      Indexed data families are introduced by a signature, such as 
+<programlisting>
+data family GMap k :: * -> *
+</programlisting>
+      The special <literal>family</literal> distinguishes family from standard
+      data declarations.  The result kind annotation is optional and, as
+      usual, defaults to <literal>*</literal> if omitted.  An example is
+<programlisting>
+data family Array e
+</programlisting>
+      Named arguments can also be given explicit kind signatures if needed.
+      Just as with
+      [http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html GADT
+      declarations] named arguments are entirely optional, so that we can
+      declare <literal>Array</literal> alternatively with 
+<programlisting>
+data family Array :: * -> *
+</programlisting>
+    </para>
+
+    <sect4 id="assoc-data-family-decl">
+      <title>Associated data family declarations</title>
+      <para>
+       When a data family is declared as part of a type class, we drop
+       the <literal>family</literal> special.  The <literal>GMap</literal>
+       declaration takes the following form 
+<programlisting>
+class GMapKey k where
+  data GMap k :: * -> *
+  ...
+</programlisting>
+       In contrast to toplevel declarations, named arguments must be used for
+       all type parameters that are to be used as type-indexes.  Moreover,
+       the argument names must be class parameters.  Each class parameter may
+       only be used at most once per associated type, but some may be omitted
+       and they may be in an order other than in the class head.  Hence, the
+       following contrived example is admissible: 
+<programlisting>
+  class C a b c where
+  data T c a :: *
+</programlisting>
+      </para>
+    </sect4>
+  </sect3>
+
+  <sect3 id="data-instance-declarations"> 
+    <title>Data instance declarations</title>
+
+    <para>
+      Instance declarations of data and newtype families are very similar to
+      standard data and newtype declarations.  The only two differences are
+      that the keyword <literal>data</literal> or <literal>newtype</literal>
+      is followed by <literal>instance</literal> and that some or all of the
+      type arguments can be non-variable types, but may not contain forall
+      types or type synonym families.  However, data families are generally
+      allowed in type parameters, and type synonyms are allowed as long as
+      they are fully applied and expand to a type that is itself admissible -
+      exactly as this is required for occurrences of type synonyms in class
+      instance parameters.  For example, the <literal>Either</literal>
+      instance for <literal>GMap</literal> is 
+<programlisting>
+data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+</programlisting>
+      In this example, the declaration has only one variant.  In general, it
+      can be any number.
+    </para>
+    <para>
+      Data and newtype instance declarations are only permitted when an
+      appropriate family declaration is in scope - just as a class instance declaratoin
+      requires the class declaration to be visible.  Moreover, each instance
+      declaration has to conform to the kind determined by its family
+      declaration.  This implies that the number of parameters of an instance
+      declaration matches the arity determined by the kind of the family.
+    </para>
+    <para>
+      A data family instance declaration can use the full exprssiveness of
+      ordinary <literal>data</literal> or <literal>newtype</literal> declarations:
+      <itemizedlist>
+      <listitem><para> Although, a data family is <emphasis>introduced</emphasis> with
+      the keyword "<literal>data</literal>", a data family <emphasis>instance</emphasis> can 
+      use either <literal>data</literal> or <literal>newtype</literal>. For example:
+<programlisting>
+data family T a
+data    instance T Int  = T1 Int | T2 Bool
+newtype instance T Char = TC Bool
+</programlisting>
+      </para></listitem>
+      <listitem><para> A <literal>data instance</literal> can use GADT syntax for the data constructors,
+      and indeed can define a GADT.  For example:
+<programlisting>
+data family G a b
+data instance G [a] b where
+   G1 :: c -> G [Int] b
+   G2 :: G [a] Bool
+</programlisting>
+      </para></listitem>
+      <listitem><para> You can use a <literal>deriving</literal> clause on a
+      <literal>data instance</literal> or <literal>newtype instance</literal>
+      declaration.
+      </para></listitem>
+      </itemizedlist>
+    </para>
+
+    <para>
+      Even if type families are defined as toplevel declarations, functions
+      that perform different computations for different family instances may still
+      need to be defined as methods of type classes.  In particular, the
+      following is not possible: 
+<programlisting>
+data family T a
+data instance T Int  = A
+data instance T Char = B
+foo :: T a -> Int
+foo A = 1             -- WRONG: These two equations together...
+foo B = 2             -- ...will produce a type error.
+</programlisting>
+Instead, you would have to write <literal>foo</literal> as a class operation, thus:
+<programlisting>
+class C a where 
+  foo :: T a -> Int
+instance Foo Int where
+  foo A = 1
+instance Foo Char where
+  foo B = 2
+</programlisting>
+      (Given the functionality provided by GADTs (Generalised Algebraic Data
+      Types), it might seem as if a definition, such as the above, should be
+      feasible.  However, type families are - in contrast to GADTs - are
+      <emphasis>open;</emphasis> i.e., new instances can always be added,
+      possibly in other 
+      modules.  Supporting pattern matching across different data instances
+      would require a form of extensible case construct.)
+    </para>
+
+    <sect4 id="assoc-data-inst">
+      <title>Associated data instances</title>
+      <para>
+       When an associated data family instance is declared within a type
+       class instance, we drop the <literal>instance</literal> keyword in the
+       family instance.  So, the <literal>Either</literal> instance
+       for <literal>GMap</literal> becomes: 
+<programlisting>
+instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
+  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+  ...
+</programlisting>
+        The most important point about associated family instances is that the
+        type indexes corresponding to class parameters must be identical to
+        the type given in the instance head; here this is the first argument
+        of <literal>GMap</literal>, namely <literal>Either a b</literal>,
+        which coincides with the only class parameter.  Any parameters to the
+        family constructor that do not correspond to class parameters, need to
+        be variables in every instance; here this is the
+        variable <literal>v</literal>. 
+      </para>
+      <para>
+       Instances for an associated family can only appear as part of
+       instances declarations of the class in which the family was declared -
+       just as with the equations of the methods of a class.  Also in
+       correspondence to how methods are handled, declarations of associated
+       types can be omitted in class instances.  If an associated family
+       instance is omitted, the corresponding instance type is not inhabited;
+       i.e., only diverging expressions, such
+       as <literal>undefined</literal>, can assume the type. 
+      </para>
+    </sect4>
+
+    <sect4 id="scoping-class-params">
+      <title>Scoping of class parameters</title>
+      <para>
+       In the case of multi-parameter type classes, the visibility of class
+       parameters in the right-hand side of associated family instances
+       depends <emphasis>solely</emphasis> on the parameters of the data
+       family.  As an example, consider the simple class declaration 
+<programlisting>
+class C a b where
+  data T a
+</programlisting>
+        Only one of the two class parameters is a parameter to the data
+        family.  Hence, the following instance declaration is invalid: 
+<programlisting>
+instance C [c] d where
+  data T [c] = MkT (c, d)    -- WRONG!!  'd' is not in scope
+</programlisting>
+        Here, the right-hand side of the data instance mentions the type
+        variable <literal>d</literal> that does not occur in its left-hand
+        side.  We cannot admit such data instances as they would compromise
+        type safety. 
+      </para>
+    </sect4>
+
+    <sect4 id="family-class-inst">
+      <title>Type class instances of family instances</title>
+      <para>
+       Type class instances of instances of data families can be defined as
+       usual, and in particular data instance declarations can
+       have <literal>deriving</literal> clauses.  For example, we can write 
+<programlisting>
+data GMap () v = GMapUnit (Maybe v)
+               deriving Show
+</programlisting>
+        which implicitly defines an instance of the form
+<programlisting>
+instance Show v => Show (GMap () v) where ...
+</programlisting>
+      </para>
+      <para>
+       Note that class instances are always for
+       particular <emphasis>instances</emphasis> of a data family and never
+       for an entire family as a whole.  This is for essentially the same
+       reasons that we cannot define a toplevel function that performs
+       pattern matching on the data constructors
+       of <emphasis>different</emphasis> instances of a single type family.
+       It would require a form of extensible case construct. 
+      </para>
+    </sect4>
+
+    <sect4 id="data-family-overlap">
+      <title>Overlap of data instances</title>
+      <para>
+       The instance declarations of a data family used in a single program
+       may not overlap at all, independent of whether they are associated or
+       not.  In contrast to type class instances, this is not only a matter
+       of consistency, but one of type safety. 
+      </para>
+    </sect4>
+
+  </sect3>
+
+  <sect3 id="data-family-import-export">
+    <title>Import and export</title>
+
+    <para>
+      The association of data constructors with type families is more dynamic
+      than that is the case with standard data and newtype declarations.  In
+      the standard case, the notation <literal>T(..)</literal> in an import or
+      export list denotes the type constructor and all the data constructors
+      introduced in its declaration.  However, a family declaration never
+      introduces any data constructors; instead, data constructors are
+      introduced by family instances.  As a result, which data constructors
+      are associated with a type family depends on the currently visible
+      instance declarations for that family.  Consequently, an import or
+      export item of the form <literal>T(..)</literal> denotes the family
+      constructor and all currently visible data constructors - in the case of
+      an export item, these may be either imported or defined in the current
+      module.  The treatment of import and export items that explicitly list
+      data constructors, such as <literal>GMap(GMapEither)</literal>, is
+      analogous. 
+    </para>
+
+    <sect4 id="data-family-impexp-assoc">
+      <title>Associated families</title>
+      <para>
+       As expected, an import or export item of the
+       form <literal>C(..)</literal> denotes all of the class' methods and
+       associated types.  However, when associated types are explicitly
+       listed as subitems of a class, we need some new syntax, as uppercase
+       identifiers as subitems are usually data constructors, not type
+       constructors.  To clarify that we denote types here, each associated
+       type name needs to be prefixed by the keyword <literal>type</literal>.
+       So for example, when explicitly listing the components of
+       the <literal>GMapKey</literal> class, we write <literal>GMapKey(type
+       GMap, empty, lookup, insert)</literal>. 
+      </para>
+    </sect4>
+
+    <sect4 id="data-family-impexp-examples">
+      <title>Examples</title>
+      <para>
+       Assuming our running <literal>GMapKey</literal> class example, let us
+       look at some export lists and their meaning: 
+       <itemizedlist>
+         <listitem>
+           <para><literal>module GMap (GMapKey) where...</literal>: Exports
+             just the class name.</para>
+         </listitem>
+         <listitem>
+           <para><literal>module GMap (GMapKey(..)) where...</literal>:
+             Exports the class, the associated type <literal>GMap</literal>
+             and the member
+             functions <literal>empty</literal>, <literal>lookup</literal>,
+             and <literal>insert</literal>.  None of the data constructors is 
+             exported.</para>
+         </listitem> 
+         <listitem>
+           <para><literal>module GMap (GMapKey(..), GMap(..))
+               where...</literal>: As before, but also exports all the data
+             constructors <literal>GMapInt</literal>, 
+             <literal>GMapChar</literal>,  
+             <literal>GMapUnit</literal>, <literal>GMapPair</literal>,
+             and <literal>GMapUnit</literal>.</para>
+         </listitem>
+         <listitem>
+           <para><literal>module GMap (GMapKey(empty, lookup, insert),
+           GMap(..)) where...</literal>: As before.</para>
+         </listitem>
+         <listitem>
+           <para><literal>module GMap (GMapKey, empty, lookup, insert, GMap(..))
+               where...</literal>: As before.</para>
+         </listitem>
+       </itemizedlist>
+      </para>
+      <para>
+       Finally, you can write <literal>GMapKey(type GMap)</literal> to denote
+       both the class <literal>GMapKey</literal> as well as its associated
+       type <literal>GMap</literal>.  However, you cannot
+       write <literal>GMapKey(type GMap(..))</literal> &mdash; i.e.,
+       sub-component specifications cannot be nested.  To
+       specify <literal>GMap</literal>'s data constructors, you have to list
+       it separately. 
+      </para>
+    </sect4>
+
+    <sect4 id="data-family-impexp-instances">
+      <title>Instances</title>
+      <para>
+       Family instances are implicitly exported, just like class instances.
+       However, this applies only to the heads of instances, not to the data
+       constructors an instance defines. 
+      </para>
+    </sect4>
+
+  </sect3>
+
+</sect2>
+
+<sect2 id="synonym-families">
+  <title>Synonym families</title>
+
+  <para>
+    Type families appear in two flavours: (1) they can be defined on the
+    toplevel or (2) they can appear inside type classes (in which case they
+    are known as associated type synonyms).  The former is the more general
+    variant, as it lacks the requirement for the type-indexes to coincide with
+    the class parameters.  However, the latter can lead to more clearly
+    structured code and compiler warnings if some type instances were -
+    possibly accidentally - omitted.  In the following, we always discuss the
+    general toplevel form first and then cover the additional constraints
+    placed on associated types.
+  </para>
+
+  <sect3 id="type-family-declarations">
+    <title>Type family declarations</title>
+
+    <para>
+      Indexed type families are introduced by a signature, such as 
+<programlisting>
+type family Elem c :: *
+</programlisting>
+      The special <literal>family</literal> distinguishes family from standard
+      type declarations.  The result kind annotation is optional and, as
+      usual, defaults to <literal>*</literal> if omitted.  An example is 
+<programlisting>
+type family Elem c
+</programlisting>
+      Parameters can also be given explicit kind signatures if needed.  We
+      call the number of parameters in a type family declaration, the family's
+      arity, and all applications of a type family must be fully saturated
+      w.r.t. to that arity.  This requirement is unlike ordinary type synonyms
+      and it implies that the kind of a type family is not sufficient to
+      determine a family's arity, and hence in general, also insufficient to
+      determine whether a type family application is well formed.  As an
+      example, consider the following declaration: 
+<programlisting>
+type family F a b :: * -> *   -- F's arity is 2, 
+                              -- although it's overall kind is * -> * -> * -> *
+</programlisting>
+      Given this declaration the following are examples of well-formed and
+      malformed types: 
+<programlisting>
+F Char [Int]       -- OK!  Kind: * -> *
+F Char [Int] Bool  -- OK!  Kind: *
+F IO Bool          -- WRONG: kind mismatch in the first argument
+F Bool             -- WRONG: unsaturated application
+</programlisting>
+      </para>
+
+    <sect4 id="assoc-type-family-decl">
+      <title>Associated type family declarations</title>
+      <para>
+       When a type family is declared as part of a type class, we drop
+       the <literal>family</literal> special.  The <literal>Elem</literal>
+       declaration takes the following form 
+<programlisting>
+class Collects ce where
+  type Elem ce :: *
+  ...
+</programlisting>
+        The argument names of the type family must be class parameters.  Each
+        class parameter may only be used at most once per associated type, but
+        some may be omitted and they may be in an order other than in the
+        class head.  Hence, the following contrived example is admissible: 
+<programlisting>
+class C a b c where
+  type T c a :: *
+</programlisting>
+        These rules are exactly as for associated data families.
+      </para>
+    </sect4>
+  </sect3>
+
+  <sect3 id="type-instance-declarations">
+    <title>Type instance declarations</title>
+    <para>
+      Instance declarations of type families are very similar to standard type
+      synonym declarations.  The only two differences are that the
+      keyword <literal>type</literal> is followed
+      by <literal>instance</literal> and that some or all of the type
+      arguments can be non-variable types, but may not contain forall types or
+      type synonym families. However, data families are generally allowed, and
+      type synonyms are allowed as long as they are fully applied and expand
+      to a type that is admissible - these are the exact same requirements as
+      for data instances.  For example, the <literal>[e]</literal> instance
+      for <literal>Elem</literal> is 
+<programlisting>
+type instance Elem [e] = e
+</programlisting>
+    </para>
+    <para>
+      Type family instance declarations are only legitimate when an
+      appropriate family declaration is in scope - just like class instances
+      require the class declaration to be visible.  Moreover, each instance
+      declaration has to conform to the kind determined by its family
+      declaration, and the number of type parameters in an instance
+      declaration must match the number of type parameters in the family
+      declaration.   Finally, the right-hand side of a type instance must be a
+      monotype (i.e., it may not include foralls) and after the expansion of
+      all saturated vanilla type synonyms, no synonyms, except family synonyms
+      may remain.  Here are some examples of admissible and illegal type
+      instances: 
+<programlisting>
+type family F a :: *
+type instance F [Int]              = Int         -- OK!
+type instance F String             = Char        -- OK!
+type instance F (F a)              = a           -- WRONG: type parameter mentions a type family
+type instance F (forall a. (a, b)) = b           -- WRONG: a forall type appears in a type parameter
+type instance F Float              = forall a.a  -- WRONG: right-hand side may not be a forall type
+
+type family G a b :: * -> *
+type instance G Int            = (,)     -- WRONG: must be two type parameters
+type instance G Int Char Float = Double  -- WRONG: must be two type parameters
+</programlisting>
+    </para>
+
+    <sect4 id="assoc-type-instance">
+      <title>Associated type instance declarations</title>
+      <para>
+       When an associated family instance is declared within a type class
+       instance, we drop the <literal>instance</literal> keyword in the family
+       instance.  So, the <literal>[e]</literal> instance
+       for <literal>Elem</literal> becomes: 
+<programlisting>
+instance (Eq (Elem [e])) => Collects ([e]) where
+  type Elem [e] = e
+  ...
+</programlisting>
+        The most important point about associated family instances is that the
+       type indexes corresponding to class parameters must be identical to the
+        type given in the instance head; here this is <literal>[e]</literal>,
+        which coincides with the only class parameter. 
+      </para>
+      <para>
+        Instances for an associated family can only appear as part of  instances
+       declarations of the class in which the family was declared - just as
+       with the equations of the methods of a class.  Also in correspondence to
+       how methods are handled, declarations of associated types can be omitted
+       in class instances.  If an associated family instance is omitted, the
+       corresponding instance type is not inhabited; i.e., only diverging
+       expressions, such as <literal>undefined</literal>, can assume the type. 
+      </para>
+    </sect4>
+
+    <sect4 id="type-family-overlap">
+      <title>Overlap of type synonym instances</title>
+      <para>
+       The instance declarations of a type family used in a single program
+       may only overlap if the right-hand sides of the overlapping instances
+       coincide for the overlapping types.  More formally, two instance
+       declarations overlap if there is a substitution that makes the
+       left-hand sides of the instances syntactically the same.  Whenever
+       that is the case, the right-hand sides of the instances must also be
+       syntactically equal under the same substitution.  This condition is
+       independent of whether the type family is associated or not, and it is
+       not only a matter of consistency, but one of type safety. 
+      </para>
+      <para>
+       Here are two example to illustrate the condition under which overlap
+       is permitted. 
+<programlisting>
+type instance F (a, Int) = [a]
+type instance F (Int, b) = [b]   -- overlap permitted
+
+type instance G (a, Int)  = [a]
+type instance G (Char, a) = [a]  -- ILLEGAL overlap, as [Char] /= [Int]
+</programlisting>
+      </para>
+    </sect4>
+
+    <sect4 id="type-family-decidability">
+      <title>Decidability of type synonym instances</title>
+      <para>
+       In order to guarantee that type inference in the presence of type
+       families decidable, we need to place a number of additional
+       restrictions on the formation of type instance declarations (c.f.,
+       Definition 5 (Relaxed Conditions) of &ldquo;<ulink 
+        url="http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html">Type
+         Checking with Open Type Functions</ulink>&rdquo;).  Instance
+         declarations have the general form 
+<programlisting>
+type instance F t1 .. tn = t
+</programlisting>
+        where we require that for every type family application <literal>(G s1
+        .. sm)</literal> in <literal>t</literal>,  
+       <orderedlist>
+         <listitem>
+           <para><literal>s1 .. sm</literal> do not contain any type family
+           constructors,</para>
+         </listitem>
+         <listitem>
+           <para>the total number of symbols (data type constructors and type
+           variables) in <literal>s1 .. sm</literal> is strictly smaller than
+           in <literal>t1 .. tn</literal>, and</para> 
+         </listitem>
+         <listitem>
+           <para>for every type
+           variable <literal>a</literal>, <literal>a</literal> occurs
+           in <literal>s1 .. sm</literal> at most as often as in <literal>t1
+           .. tn</literal>.</para>
+         </listitem>
+       </orderedlist>
+       These restrictions are easily verified and ensure termination of type
+       inference.  However, they are not sufficient to guarantee completeness
+       of type inference in the presence of, so called, ''loopy equalities'',
+       such as <literal>a ~ [F a]</literal>, where a recursive occurrence of
+       a type variable is underneath a family application and data
+       constructor application - see the above mentioned paper for details.   
+      </para>
+      <para>
+       If the option <option>-XUndecidableInstances</option> is passed to the
+       compiler, the above restrictions are not enforced and it is on the
+       programmer to ensure termination of the normalisation of type families
+       during type inference. 
+      </para>
+    </sect4>
+  </sect3>
+
+  <sect3 id-="equality-constraints">
+    <title>Equality constraints</title>
+    <para>
+      Type context can include equality constraints of the form <literal>t1 ~
+      t2</literal>, which denote that the types <literal>t1</literal>
+      and <literal>t2</literal> need to be the same.  In the presence of type
+      families, whether two types are equal cannot generally be decided
+      locally.  Hence, the contexts of function signatures may include
+      equality constraints, as in the following example: 
+<programlisting>
+sumCollects :: (Collects c1, Collects c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
+</programlisting>
+      where we require that the element type of <literal>c1</literal>
+      and <literal>c2</literal> are the same.  In general, the
+      types <literal>t1</literal> and <literal>t2</literal> of an equality
+      constraint may be arbitrary monotypes; i.e., they may not contain any
+      quantifiers, independent of whether higher-rank types are otherwise
+      enabled. 
+    </para>
+    <para>
+      Equality constraints can also appear in class and instance contexts.
+      The former enable a simple translation of programs using functional
+      dependencies into programs using family synonyms instead.  The general
+      idea is to rewrite a class declaration of the form 
+<programlisting>
+class C a b | a -> b
+</programlisting>
+      to
+<programlisting>
+class (F a ~ b) => C a b where
+  type F a
+</programlisting>
+      That is, we represent every functional dependency (FD) <literal>a1 .. an
+      -> b</literal> by an FD type family <literal>F a1 .. an</literal> and a
+      superclass context equality <literal>F a1 .. an ~ b</literal>,
+      essentially giving a name to the functional dependency.  In class
+      instances, we define the type instances of FD families in accordance
+      with the class head.  Method signatures are not affected by that
+      process. 
+    </para>
+    <para>
+      NB: Equalities in superclass contexts are not fully implemented in
+      GHC 6.10. 
+    </para>
+  </sect3>
+
+  <sect3 id-="ty-fams-in-instances">
+    <title>Type families and instance declarations</title>
+    <para>Type families require us to extend the rules for 
+      the form of instance heads, which are given 
+      in <xref linkend="flexible-instance-head"/>.
+      Specifically:
+<itemizedlist>
+ <listitem><para>Data type families may appear in an instance head</para></listitem>
+ <listitem><para>Type synonym families may not appear (at all) in an instance head</para></listitem>
+</itemizedlist>
+The reason for the latter restriction is that there is no way to check for. Consider
+<programlisting>
+   type family F a
+   type instance F Bool = Int
+
+   class C a
+
+   instance C Int
+   instance C (F a)
+</programlisting>
+Now a constraint <literal>(C (F Bool))</literal> would match both instances.
+The situation is especially bad because the type instance for <literal>F Bool</literal>
+might be in another module, or even in a module that is not yet written.
+</para>
+</sect3>
+</sect2>
+
+</sect1>
+
 <sect1 id="other-type-extensions">
 <title>Other type system extensions</title>
 
@@ -3649,9 +4562,11 @@ to work since it gets translated into an equality comparison.
 
 <sect3 id="flexible-contexts"><title>The context of a type signature</title>
 <para>
-Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variable)</emphasis> or
-<emphasis>(class (type-variable type-variable ...))</emphasis>.  Thus,
+The <option>-XFlexibleContexts</option> flag lifts the Haskell 98 restriction
+that the type-class constraints in a type signature must have the 
+form <emphasis>(class type-variable)</emphasis> or
+<emphasis>(class (type-variable type-variable ...))</emphasis>. 
+With <option>-XFlexibleContexts</option>
 these type signatures are perfectly OK
 <programlisting>
   g :: Eq [a] => ...
@@ -4581,9 +5496,13 @@ f xs = ys ++ ys
        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>. 
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope,
+because of the explicit <literal>forall</literal> (<xref linkend="decl-type-sigs"/>).
+The type variables bound by a <literal>forall</literal> scope over
+the entire definition of the accompanying value declaration.
+In this example, the type variable <literal>a</literal> scopes over the whole 
+definition of <literal>f</literal>, including over
+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.
@@ -4920,33 +5839,6 @@ pattern binding must have the same context.  For example, this is fine:
 </para>
 </sect2>
 
-<sect2 id="type-families">
-<title>Type families
-</title>
-
-<para>
-GHC supports the definition of type families indexed by types.  They may be
-seen as an extension of Haskell 98's class-based overloading of values to
-types.  When type families are declared in classes, they are also known as
-associated types.
-</para>
-<para>
-There are two forms of type families: data families and type synonym families.
-Currently, only the former are fully implemented, while we are still working
-on the latter.  As a result, the specification of the language extension is
-also still to some degree in flux.  Hence, a more detailed description of
-the language extension and its use is currently available
-from <ulink url="http://www.haskell.org/haskellwiki/GHC/Indexed_types">the Haskell
-wiki page on type families</ulink>.  The material will be moved to this user's
-guide when it has stabilised.
-</para>
-<para>
-Type families are enabled by the flag <option>-XTypeFamilies</option>.
-</para>
-
-
-</sect2>
-
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
   
@@ -5011,6 +5903,8 @@ Wiki page</ulink>.
                  <itemizedlist>
                    <listitem><para> an expression; the spliced expression must
                    have type <literal>Q Exp</literal></para></listitem>
+                   <listitem><para> an type; the spliced expression must
+                   have type <literal>Q Typ</literal></para></listitem>
                    <listitem><para> a list of top-level declarations; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>
                    </itemizedlist>
                </para>
@@ -5059,7 +5953,7 @@ Wiki page</ulink>.
 (Compared to the original paper, there are many differences of detail.
 The syntax for a declaration splice uses "<literal>$</literal>" not "<literal>splice</literal>".
 The type of the enclosed expression must be  <literal>Q [Dec]</literal>, not  <literal>[Q Dec]</literal>.
-Type splices are not implemented, and neither are pattern splices or quotations.
+Pattern splices and quotations are not implemented.)
 
 </sect2>
 
@@ -5276,7 +6170,7 @@ main = do { print $ eval [$expr|1 + 2|]
 module Expr where
 
 import qualified Language.Haskell.TH as TH
-import Language.Haskell.TH.Quasi
+import Language.Haskell.TH.Quote
 
 data Expr  =  IntExpr Integer
            |  AntiIntExpr String
@@ -5347,6 +6241,8 @@ For more details, see
 &ldquo;Generalising Monads to Arrows&rdquo;,
 John Hughes, in <citetitle>Science of Computer Programming</citetitle> 37,
 pp67&ndash;111, May 2000.
+The paper that introduced arrows: a friendly introduction, motivated with
+programming examples.
 </para>
 </listitem>
 
@@ -5354,6 +6250,7 @@ pp67&ndash;111, May 2000.
 <para>
 &ldquo;<ulink url="http://www.soi.city.ac.uk/~ross/papers/notation.html">A New Notation for Arrows</ulink>&rdquo;,
 Ross Paterson, in <citetitle>ICFP</citetitle>, Sep 2001.
+Introduced the notation described here.
 </para>
 </listitem>
 
@@ -5365,17 +6262,42 @@ Palgrave, 2003.
 </para>
 </listitem>
 
-</itemizedlist>
-and the arrows web page at
+<listitem>
+<para>
+&ldquo;<ulink url="http://www.cs.chalmers.se/~rjmh/afp-arrows.pdf">Programming with Arrows</ulink>&rdquo;,
+John Hughes, in <citetitle>5th International Summer School on
+Advanced Functional Programming</citetitle>,
+<citetitle>Lecture Notes in Computer Science</citetitle> vol. 3622,
+Springer, 2004.
+This paper includes another introduction to the notation,
+with practical examples.
+</para>
+</listitem>
+
+<listitem>
+<para>
+&ldquo;<ulink url="http://www.haskell.org/ghc/docs/papers/arrow-rules.pdf">Type and Translation Rules for Arrow Notation in GHC</ulink>&rdquo;,
+Ross Paterson and Simon Peyton Jones, September 16, 2004.
+A terse enumeration of the formal rules used
+(extracted from comments in the source code).
+</para>
+</listitem>
+
+<listitem>
+<para>
+The arrows web page at
 <ulink url="http://www.haskell.org/arrows/"><literal>http://www.haskell.org/arrows/</literal></ulink>.
+</para>
+</listitem>
+
+</itemizedlist>
 With the <option>-XArrows</option> flag, GHC supports the arrow
-notation described in the second of these papers.
-What follows is a brief introduction to the notation;
-it won't make much sense unless you've read Hughes's paper.
-This notation is translated to ordinary Haskell,
-using combinators from the
+notation described in the second of these papers,
+translating it using combinators from the
 <ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>
 module.
+What follows is a brief introduction to the notation;
+it won't make much sense unless you've read Hughes's paper.
 </para>
 
 <para>The extension adds a new kind of expression for defining arrows:
@@ -5649,7 +6571,8 @@ We could define our own operator
 <programlisting>
 untilA :: ArrowChoice a => a e () -> a e Bool -> a e ()
 untilA body cond = proc x ->
-        if cond x then returnA -&lt; ()
+        b &lt;- cond -&lt; x
+        if b then returnA -&lt; ()
         else do
                 body -&lt; x
                 untilA body cond -&lt; x
@@ -5831,13 +6754,24 @@ Because the preprocessor targets Haskell (rather than Core),
 <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.
+patterns</emphasis>, written <literal>!<replaceable>pat</replaceable></literal>.   
+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>
+The key change is the addition of a new rule to the 
+<ulink url="http://haskell.org/onlinereport/exps.html#sect3.17.2">semantics of pattern matching in the Haskell 98 report</ulink>.
+Add new bullet 10, saying: Matching the pattern <literal>!</literal><replaceable>pat</replaceable> 
+against a value <replaceable>v</replaceable> behaves as follows:
+<itemizedlist>
+<listitem><para>if <replaceable>v</replaceable> is bottom, the match diverges</para></listitem>
+<listitem><para>otherwise, <replaceable>pat</replaceable> is matched against <replaceable>v</replaceable>  </para></listitem>
+</itemizedlist>
+</para>
+<para>
 Bang patterns are enabled by the flag <option>-XBangPatterns</option>.
 </para>
 
@@ -5868,9 +6802,40 @@ A bang only really has an effect if it precedes a variable or wild-card pattern:
 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
+Here, <literal>f3</literal> and <literal>f4</literal> are identical; 
+putting a bang before a pattern that
 forces evaluation anyway does nothing.
-</para><para>
+</para>
+<para>
+There is one (apparent) exception to this general rule that a bang only
+makes a difference when it precedes a variable or wild-card: a bang at the
+top level of a <literal>let</literal> or <literal>where</literal>
+binding makes the binding strict, regardless of the pattern. For example:
+<programlisting>
+let ![x,y] = e in b
+</programlisting>
+is a strict binding: operationally, it evaluates <literal>e</literal>, matches
+it against the pattern <literal>[x,y]</literal>, and then evaluates <literal>b</literal>.
+(We say "apparent" exception because the Right Way to think of it is that the bang
+at the top of a binding is not part of the <emphasis>pattern</emphasis>; rather it
+is part of the syntax of the <emphasis>binding</emphasis>.)
+Nested bangs in a pattern binding behave uniformly with all other forms of 
+pattern matching.  For example
+<programlisting>
+let (!x,[y]) = e in b
+</programlisting>
+is equivalent to this:
+<programlisting>
+let { t = case e of (x,[y]) -> x `seq` (x,y)
+      x = fst t
+      y = snd t }
+in b
+</programlisting>
+The binding is lazy, but when either <literal>x</literal> or <literal>y</literal> is
+evaluated by <literal>b</literal> the entire pattern is matched, including forcing the
+evaluation of <literal>x</literal>.
+</para>
+<para>
 Bang patterns work in <literal>case</literal> expressions too, of course:
 <programlisting>
 g5 x = let y = f x in body
@@ -5880,18 +6845,6 @@ g7 x = case f x of { !y -&gt; body }
 The functions <literal>g5</literal> and <literal>g6</literal> mean exactly the same thing.  
 But <literal>g7</literal> evaluates <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>
 
@@ -6077,14 +7030,31 @@ Assertion failures can be caught, see the documentation for the
     <replaceable>word</replaceable>.  The various values for
     <replaceable>word</replaceable> that GHC understands are described
     in the following sections; any pragma encountered with an
-    unrecognised <replaceable>word</replaceable> is (silently)
+    unrecognised <replaceable>word</replaceable> is
     ignored. The layout rule applies in pragmas, so the closing <literal>#-}</literal>
     should start in a column to the right of the opening <literal>{-#</literal>. </para> 
 
-    <para>Certain pragmas are <emphasis>file-header pragmas</emphasis>.  A file-header
-      pragma must precede the <literal>module</literal> keyword in the file.  
+    <para>Certain pragmas are <emphasis>file-header pragmas</emphasis>:
+      <itemizedlist>
+      <listitem><para>
+         A file-header
+         pragma must precede the <literal>module</literal> keyword in the file.
+         </para></listitem>
+      <listitem><para>
       There can be as many file-header pragmas as you please, and they can be
-      preceded or followed by comments.</para>
+      preceded or followed by comments.  
+         </para></listitem>
+      <listitem><para>
+      File-header pragmas are read once only, before
+      pre-processing the file (e.g. with cpp).
+         </para></listitem>
+      <listitem><para>
+         The file-header pragmas are: <literal>{-# LANGUAGE #-}</literal>,
+       <literal>{-# OPTIONS_GHC #-}</literal>, and
+       <literal>{-# INCLUDE #-}</literal>.
+         </para></listitem>
+      </itemizedlist>
+      </para>
 
     <sect2 id="language-pragma">
       <title>LANGUAGE pragma</title>
@@ -6162,56 +7132,63 @@ Assertion failures can be caught, see the documentation for the
        don't recommend using this approach with GHC.</para>
     </sect2>
 
-    <sect2 id="deprecated-pragma">
-      <title>DEPRECATED pragma</title>
-      <indexterm><primary>DEPRECATED</primary>
-      </indexterm>
+    <sect2 id="warning-deprecated-pragma">
+      <title>WARNING and DEPRECATED pragmas</title>
+      <indexterm><primary>WARNING</primary></indexterm>
+      <indexterm><primary>DEPRECATED</primary></indexterm>
 
-      <para>The DEPRECATED pragma lets you specify that a particular
-      function, class, or type, is deprecated.  There are two
-      forms.
+      <para>The WARNING pragma allows you to attach an arbitrary warning
+      to a particular function, class, or type.
+      A DEPRECATED pragma lets you specify that
+      a particular function, class, or type is deprecated.
+      There are two ways of using these pragmas.
 
       <itemizedlist>
        <listitem>
-         <para>You can deprecate an entire module thus:</para>
+         <para>You can work on an entire module thus:</para>
 <programlisting>
    module Wibble {-# DEPRECATED "Use Wobble instead" #-} where
      ...
 </programlisting>
+      <para>Or:</para>
+<programlisting>
+   module Wibble {-# WARNING "This is an unstable interface." #-} where
+     ...
+</programlisting>
          <para>When you compile any module that import
           <literal>Wibble</literal>, GHC will print the specified
           message.</para>
        </listitem>
 
        <listitem>
-         <para>You can deprecate a function, class, type, or data constructor, with the
-         following top-level declaration:</para>
+         <para>You can attach a warning to a function, class, type, or data constructor, with the
+         following top-level declarations:</para>
 <programlisting>
    {-# DEPRECATED f, C, T "Don't use these" #-}
+   {-# WARNING unsafePerformIO "This is unsafe; I hope you know what you're doing" #-}
 </programlisting>
          <para>When you compile any module that imports and uses any
           of the specified entities, GHC will print the specified
           message.</para>
-         <para> You can only deprecate entities declared at top level in the module
+         <para> You can only attach to entities declared at top level in the module
          being compiled, and you can only use unqualified names in the list of
-         entities being deprecated.  A capitalised name, such as <literal>T</literal>
+         entities. A capitalised name, such as <literal>T</literal>
          refers to <emphasis>either</emphasis> the type constructor <literal>T</literal>
          <emphasis>or</emphasis> the data constructor <literal>T</literal>, or both if
-         both are in scope.  If both are in scope, there is currently no way to deprecate 
-         one without the other (c.f. fixities <xref linkend="infix-tycons"/>).</para>
+         both are in scope.  If both are in scope, there is currently no way to
+      specify one without the other (c.f. fixities
+      <xref linkend="infix-tycons"/>).</para>
        </listitem>
       </itemizedlist>
-      Any use of the deprecated item, or of anything from a deprecated
-      module, will be flagged with an appropriate message.  However,
-      deprecations are not reported for
-      (a) uses of a deprecated function within its defining module, and
-      (b) uses of a deprecated function in an export list.
+      Warnings and deprecations are not reported for
+      (a) uses within the defining module, and
+      (b) uses in an export list.
       The latter reduces spurious complaints within a library
       in which one module gathers together and re-exports 
       the exports of several others.
       </para>
       <para>You can suppress the warnings with the flag
-      <option>-fno-warn-deprecations</option>.</para>
+      <option>-fno-warn-warnings-deprecations</option>.</para>
     </sect2>
 
     <sect2 id="inline-noinline-pragma">
@@ -6385,6 +7362,83 @@ happen.
       </sect3>
     </sect2>
 
+    <sect2 id="annotation-pragmas">
+      <title>ANN pragmas</title>
+      
+      <para>GHC offers the ability to annotate various code constructs with additional
+      data by using three pragmas.  This data can then be inspected at a later date by
+      using GHC-as-a-library.</para>
+            
+      <sect3 id="ann-pragma">
+        <title>Annotating values</title>
+        
+        <indexterm><primary>ANN</primary></indexterm>
+        
+        <para>Any expression that has both <literal>Typeable</literal> and <literal>Data</literal> instances may be attached to a top-level value
+        binding using an <literal>ANN</literal> pragma. In particular, this means you can use <literal>ANN</literal>
+        to annotate data constructors (e.g. <literal>Just</literal>) as well as normal values (e.g. <literal>take</literal>).
+        By way of example, to annotate the function <literal>foo</literal> with the annotation <literal>Just "Hello"</literal>
+        you would do this:</para>
+        
+<programlisting>
+{-# ANN foo (Just "Hello") #-}
+foo = ...
+</programlisting>
+        
+        <para>
+          A number of restrictions apply to use of annotations:
+          <itemizedlist>
+            <listitem><para>The binder being annotated must be at the top level (i.e. no nested binders)</para></listitem>
+            <listitem><para>The binder being annotated must be declared in the current module</para></listitem>
+            <listitem><para>The expression you are annotating with must have a type with <literal>Typeable</literal> and <literal>Data</literal> instances</para></listitem>
+            <listitem><para>The <ulink linkend="using-template-haskell">Template Haskell staging restrictions</ulink> apply to the
+            expression being annotated with, so for example you cannot run a function from the module being compiled.</para>
+            
+            <para>To be precise, the annotation <literal>{-# ANN x e #-}</literal> is well staged if and only if <literal>$(e)</literal> would be 
+            (disregarding the usual type restrictions of the splice syntax, and the usual restriction on splicing inside a splice - <literal>$([|1|])</literal> is fine as an annotation, albeit redundant).</para></listitem>
+          </itemizedlist>
+          
+          If you feel strongly that any of these restrictions are too onerous, <ulink url="http://hackage.haskell.org/trac/ghc/wiki/MailingListsAndIRC">
+          please give the GHC team a shout</ulink>.
+        </para>
+        
+        <para>However, apart from these restrictions, many things are allowed, including expressions which are not fully evaluated!
+        Annotation expressions will be evaluated by the compiler just like Template Haskell splices are. So, this annotation is fine:</para>
+        
+<programlisting>
+{-# ANN f SillyAnnotation { foo = (id 10) + $([| 20 |]), bar = 'f } #-}
+f = ...
+</programlisting>
+      </sect3>
+      
+      <sect3 id="typeann-pragma">
+        <title>Annotating types</title>
+        
+        <indexterm><primary>ANN type</primary></indexterm>
+        <indexterm><primary>ANN</primary></indexterm>
+        
+        <para>You can annotate types with the <literal>ANN</literal> pragma by using the <literal>type</literal> keyword. For example:</para>
+        
+<programlisting>
+{-# ANN type Foo (Just "A `Maybe String' annotation") #-}
+data Foo = ...
+</programlisting>
+      </sect3>
+      
+      <sect3 id="modann-pragma">
+        <title>Annotating modules</title>
+        
+        <indexterm><primary>ANN module</primary></indexterm>
+        <indexterm><primary>ANN</primary></indexterm>
+        
+        <para>You can annotate modules with the <literal>ANN</literal> pragma by using the <literal>module</literal> keyword. For example:</para>
+        
+<programlisting>
+{-# ANN module (Just "A `Maybe String' annotation") #-}
+</programlisting>
+      </sect3>
+    </sect2>
+
     <sect2 id="line-pragma">
       <title>LINE pragma</title>
 
@@ -6625,15 +7679,7 @@ data S = S {-# UNPACK #-} !Int {-# UNPACK #-} !Int
 
 <para>
 The programmer can specify rewrite rules as part of the source program
-(in a pragma).  GHC applies these rewrite rules wherever it can, provided (a) 
-the <option>-O</option> flag (<xref linkend="options-optimise"/>) is on, 
-and (b) the <option>-fno-rewrite-rules</option> flag
-(<xref linkend="options-f"/>) is not specified, and (c) the
-<option>-fglasgow-exts</option> (<xref linkend="options-language"/>)
-flag is active.
-</para>
-
-<para>
+(in a pragma).  
 Here is an example:
 
 <programlisting>
@@ -6753,17 +7799,40 @@ variables it mentions, though of course they need to be in scope.
 <listitem>
 
 <para>
- Rules are automatically exported from a module, just as instance declarations are.
+ All rules are implicitly exported from the module, and are therefore
+in force in any module that imports the module that defined the rule, directly
+or indirectly.  (That is, if A imports B, which imports C, then C's rules are
+in force when compiling A.)  The situation is very similar to that for instance
+declarations.
+</para>
+</listitem>
+
+<listitem>
+
+<para>
+Inside a RULE "<literal>forall</literal>" is treated as a keyword, regardless of
+any other flag settings.  Furthermore, inside a RULE, the language extension
+<option>-XScopedTypeVariables</option> is automatically enabled; see 
+<xref linkend="scoped-type-variables"/>.
 </para>
 </listitem>
+<listitem>
 
+<para>
+Like other pragmas, RULE pragmas are always checked for scope errors, and
+are typechecked. Typechecking means that the LHS and RHS of a rule are typechecked, 
+and must have the same type.  However, rules are only <emphasis>enabled</emphasis>
+if the <option>-fenable-rewrite-rules</option> flag is 
+on (see <xref linkend="rule-semantics"/>).
+</para>
+</listitem>
 </itemizedlist>
 
 </para>
 
 </sect2>
 
-<sect2>
+<sect2 id="rule-semantics">
 <title>Semantics</title>
 
 <para>
@@ -6771,9 +7840,17 @@ From a semantic point of view:
 
 <itemizedlist>
 <listitem>
-
 <para>
-Rules are only applied if you use the <option>-O</option> flag.
+Rules are enabled (that is, used during optimisation)
+by the <option>-fenable-rewrite-rules</option> flag.
+This flag is implied by <option>-O</option>, and may be switched
+off (as usual) by <option>-fno-enable-rewrite-rules</option>.
+(NB: enabling <option>-fenable-rewrite-rules</option> without <option>-O</option> 
+may not do what you expect, though, because without <option>-O</option> GHC 
+ignores all optimisation information in interface files;
+see <option>-fignore-interface-pragmas</option>, <xref linkend="options-f"/>.)
+Note that <option>-fenable-rewrite-rules</option> is an <emphasis>optimisation</emphasis> flag, and
+has no effect on parsing or typechecking.
 </para>
 </listitem>
 
@@ -6790,14 +7867,6 @@ expression by substituting for the pattern variables.
 <listitem>
 
 <para>
- The LHS and RHS of a rule are typechecked, and must have the
-same type.
-
-</para>
-</listitem>
-<listitem>
-
-<para>
  GHC makes absolutely no attempt to verify that the LHS and RHS
 of a rule have the same meaning.  That is undecidable in general, and
 infeasible in most interesting cases.  The responsibility is entirely the programmer's!
@@ -6890,17 +7959,6 @@ pragma on <literal>f</literal>, to ensure
 that it is not inlined until its RULEs have had a chance to fire.
 </para>
 </listitem>
-<listitem>
-
-<para>
- All rules are implicitly exported from the module, and are therefore
-in force in any module that imports the module that defined the rule, directly
-or indirectly.  (That is, if A imports B, which imports C, then C's rules are
-in force when compiling A.)  The situation is very similar to that for instance
-declarations.
-</para>
-</listitem>
-
 </itemizedlist>
 
 </para>
@@ -7285,7 +8343,7 @@ r) ->
 <title>Special built-in functions</title>
 <para>GHC has a few built-in functions with special behaviour.  These
 are now described in the module <ulink
-url="../libraries/base/GHC-Prim.html"><literal>GHC.Prim</literal></ulink>
+url="../libraries/ghc-prim/GHC-Prim.html"><literal>GHC.Prim</literal></ulink>
 in the library documentation.</para>
 </sect1>