Fix scoped type variables for expression type signatures
[ghc-hetmet.git] / docs / users_guide / glasgow_exts.xml
index 6b41b39..f8ad5c1 100644 (file)
@@ -116,11 +116,22 @@ documentation</ulink> describes all the libraries that come with GHC.
 
       <varlistentry>
        <term>
-          <option>-fno-monomorphism-restriction</option>:
-          <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
+          <option>-fno-monomorphism-restriction</option>,<option>-fno-monomorphism-restriction</option>:
         </term>
        <listitem>
-         <para> Switch off the Haskell 98 monomorphism restriction.
+         <para> These two flags control how generalisation is done.
+           See <xref linkend="monomorphism"/>.
+          </para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term>
+          <option>-fextended-default-rules</option>:
+          <indexterm><primary><option>-fextended-default-rules</option></primary></indexterm>
+        </term>
+       <listitem>
+         <para> 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>
@@ -140,7 +151,7 @@ documentation</ulink> describes all the libraries that come with GHC.
           <indexterm><primary><option>-fallow-incoherent-instances</option></primary></indexterm>
         </term>
        <term>
-          <option>-fcontext-stack</option>
+          <option>-fcontext-stack=N</option>
           <indexterm><primary><option>-fcontext-stack</option></primary></indexterm>
         </term>
        <listitem>
@@ -617,7 +628,7 @@ clunky env var1 var1 = case lookup env var1 of
     Nothing -&gt; fail
     Just val2 -&gt; val1 + val2
 where
-  fail = val1 + val2
+  fail = var1 + var2
 </programlisting>
 
 <para>
@@ -894,6 +905,38 @@ fromInteger :: Integer -> Bool -> Bool
             you should be all right.</para>
 
 </sect2>
+
+<sect2 id="postfix-operators">
+<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
+<programlisting>
+  (e !)
+</programlisting> 
+is equivalent (from the point of view of both type checking and execution) to the expression
+<programlisting>
+  ((!) e)
+</programlisting> 
+(for any expression <literal>e</literal> and operator <literal>(!)</literal>.
+The strict Haskell 98 interpretation is that the section is equivalent to
+<programlisting>
+  (\y -> (!) e y)
+</programlisting> 
+That is, the operator must be a function of two arguments.  GHC allows it to
+take only one argument, and that in turn allows you to write the function
+postfix.
+</para>
+<para>Since this extension goes beyond Haskell 98, it should really be enabled
+by a flag; but in fact it is enabled all the time.  (No Haskell 98 programs
+change their behaviour, of course.)
+</para>
+<para>The extension does not extend to the left-hand side of function
+definitions; you must define such a function in prefix form.</para>
+
+</sect2>
+
 </sect1>
 
 
@@ -2022,6 +2065,11 @@ something more specific does not:
     op = ... -- Default
 </programlisting>
 </para>
+<para>You can find lots of background material about the reason for these
+restrictions in the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
+Understanding functional dependencies via Constraint Handling Rules</ulink>.
+</para>
 </sect3>
 
 <sect3 id="undecidable-instances">
@@ -2090,7 +2138,7 @@ option</primary></indexterm>, you can use arbitrary
 types in both an instance context and instance head.  Termination is ensured by having a
 fixed-depth recursion stack.  If you exceed the stack depth you get a
 sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack</option><emphasis>N</emphasis>.
+with <option>-fcontext-stack=</option><emphasis>N</emphasis>.
 </para>
 
 </sect3>
@@ -2178,8 +2226,20 @@ some other constraint.  But if the instance declaration was compiled with
 check for that declaration.
 </para></listitem>
 </itemizedlist>
-All this makes it possible for a library author to design a library that relies on 
-overlapping instances without the library client having to know.
+These rules make it possible for a library author to design a library that relies on 
+overlapping instances without the library client having to know.  
+</para>
+<para>
+If an instance declaration is compiled without
+<option>-fallow-overlapping-instances</option>,
+then that instance can never be overlapped.  This could perhaps be
+inconvenient.  Perhaps the rule should instead say that the
+<emphasis>overlapping</emphasis> instance declaration should be compiled in
+this way, rather than the <emphasis>overlapped</emphasis> one.  Perhaps overlap
+at a usage site should be permitted regardless of how the instance declarations
+are compiled, if the <option>-fallow-overlapping-instances</option> flag is
+used at the usage site.  (Mind you, the exact usage site can occasionally be
+hard to pin down.)  We are interested to receive feedback on these points.
 </para>
 <para>The <option>-fallow-incoherent-instances</option> flag implies the
 <option>-fallow-overlapping-instances</option> flag, but not vice versa.
@@ -2466,7 +2526,7 @@ function that called it. For example, our <literal>sort</literal> function might
 to pick out the least value in a list:
 <programlisting>
   least   :: (?cmp :: a -> a -> Bool) => [a] -> a
-  least xs = fst (sort xs)
+  least xs = head (sort xs)
 </programlisting>
 Without lifting a finger, the <literal>?cmp</literal> parameter is
 propagated to become a parameter of <literal>least</literal> as well. With explicit
@@ -2626,6 +2686,11 @@ inner binding of <literal>?x</literal>, so <literal>(f 9)</literal> will return
 </sect3>
 </sect2>
 
+    <!--   ======================= COMMENTED OUT ========================
+
+    We intend to remove linear implicit parameters, so I'm at least removing
+    them from the 6.6 user manual
+
 <sect2 id="linear-implicit-parameters">
 <title>Linear implicit parameters</title>
 <para>
@@ -2641,7 +2706,7 @@ problem that monads seem over-kill for certain sorts of problem, notably:
 
 <para>
 Linear implicit parameters are just like ordinary implicit parameters,
-except that they are "linear" -- that is, they cannot be copied, and
+except that they are "linear"; that is, they cannot be copied, and
 must be explicitly "split" instead.  Linear implicit parameters are
 written '<literal>%x</literal>' instead of '<literal>?x</literal>'.  
 (The '/' in the '%' suggests the split!)
@@ -2796,6 +2861,8 @@ and you'd be right.  That is why they are an experimental feature.
 
 </sect2>
 
+================ END OF Linear Implicit Parameters commented out -->
+
 <sect2 id="sec-kinding">
 <title>Explicitly-kinded quantification</title>
 
@@ -3163,228 +3230,103 @@ for rank-2 types.
 </sect2>
 
 
-
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>.  This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types.  For example:
+<programlisting>
+  f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+  f (Just g) = Just (g [3], g "hello")
+  f Nothing  = Nothing
+</programlisting>
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
+</para>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.  
+</para>
+</sect2>
 
 <sect2 id="scoped-type-variables">
-<title>Scoped type variables
+<title>Lexically scoped type variables
 </title>
 
 <para>
-A <emphasis>lexically scoped type variable</emphasis> can be bound by:
-<itemizedlist>
-<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
-<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
-<listitem><para>A result type signature (<xref linkend="result-type-sigs"/>)</para></listitem>
-</itemizedlist>
-For example:
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
 <programlisting>
-f (xs::[a]) = ys ++ ys
-           where
-              ys :: [a]
-              ys = reverse xs
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+     where
+       ys :: [a]
+       ys = reverse xs
 </programlisting>
-The pattern <literal>(xs::[a])</literal> includes a type signature for <varname>xs</varname>.
-This brings the type variable <literal>a</literal> into scope; it scopes over
-all the patterns and right hand sides for this equation for <function>f</function>.
-In particular, it is in scope at the type signature for <varname>y</varname>.
-</para>
-
-<para>
-At ordinary type signatures, such as that for <varname>ys</varname>, any type variables
-mentioned in the type signature <emphasis>that are not in scope</emphasis> are
-implicitly universally quantified.  (If there are no type variables in
-scope, all type variables mentioned in the signature are universally
-quantified, which is just as in Haskell 98.)  In this case, since <varname>a</varname>
-is in scope, it is not universally quantified, so the type of <varname>ys</varname> is
-the same as that of <varname>xs</varname>.  In Haskell 98 it is not possible to declare
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
+the entire definition of <literal>f</literal>.
+In particular, it is in scope at the type signature for <varname>ys</varname>. 
+In Haskell 98 it is not possible to declare
 a type for <varname>ys</varname>; a major benefit of scoped type variables is that
 it becomes possible to do so.
 </para>
-
-<para>
-Scoped type variables are implemented in both GHC and Hugs.  Where the
-implementations differ from the specification below, those differences
-are noted.
-</para>
-
-<para>
-So much for the basic idea.  Here are the details.
+<para>Lexically-scoped type variables are enabled by
+<option>-fglasgow-exts</option>.
 </para>
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases.  Read this section
+carefully!</para>
 
 <sect3>
-<title>What a scoped type variable means</title>
-<para>
-A lexically-scoped type variable is simply
-the name for a type.   The restriction it expresses is that all occurrences
-of the same name mean the same type.  For example:
-<programlisting>
-  f :: [Int] -> Int -> Int
-  f (xs::[a]) (y::a) = (head xs + y) :: a
-</programlisting>
-The pattern type signatures on the left hand side of
-<literal>f</literal> express the fact that <literal>xs</literal>
-must be a list of things of some type <literal>a</literal>; and that <literal>y</literal>
-must have this same type.  The type signature on the expression <literal>(head xs)</literal>
-specifies that this expression must have the same type <literal>a</literal>.
-<emphasis>There is no requirement that the type named by "<literal>a</literal>" is
-in fact a type variable</emphasis>.  Indeed, in this case, the type named by "<literal>a</literal>" is
-<literal>Int</literal>.  (This is a slight liberalisation from the original rather complex
-rules, which specified that a pattern-bound type variable should be universally quantified.)
-For example, all of these are legal:</para>
-
-<programlisting>
-  t (x::a) (y::a) = x+y*2
-
-  f (x::a) (y::b) = [x,y]       -- a unifies with b
-
-  g (x::a) = x + 1::Int         -- a unifies with Int
-
-  h x = let k (y::a) = [x,y]    -- a is free in the
-        in k x                  -- environment
-
-  k (x::a) True    = ...        -- a unifies with Int
-  k (x::Int) False = ...
-
-  w :: [b] -> [b]
-  w (x::a) = x                  -- a unifies with [b]
-</programlisting>
-
-</sect3>
-
-<sect3>
-<title>Scope and implicit quantification</title>
-
-<para>
+<title>Overview</title>
 
+<para>The design follows the following principles
 <itemizedlist>
-<listitem>
-
-<para>
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern.  We describe this set as
-the <emphasis>type variables bound by the pattern</emphasis>.
-For example:
-<programlisting>
-  f (x::a) = let g (y::(a,b)) = fst y
-             in
-             g (x,True)
-</programlisting>
-The pattern <literal>(x::a)</literal> brings the type variable
-<literal>a</literal> into scope, as well as the term 
-variable <literal>x</literal>.  The pattern <literal>(y::(a,b))</literal>
-contains an occurrence of the already-in-scope type variable <literal>a</literal>,
-and brings into scope the type variable <literal>b</literal>.
-</para>
-</listitem>
-
-<listitem>
-<para>
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern.  For example:
-<programlisting>
-  let
-    f (x::a) = &lt;...rhs of f...>
-    (p::b, q::b) = (1,2)
-  in &lt;...body of let...>
-</programlisting>
-Here, the type variable <literal>a</literal> scopes over the right hand side of <literal>f</literal>,
-just like <literal>x</literal> does; while the type variable <literal>b</literal> scopes over the
-body of the <literal>let</literal>, and all the other definitions in the <literal>let</literal>,
-just like <literal>p</literal> and <literal>q</literal> do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the <literal>let</literal> group.
-</para>
-</listitem>
-
-
-<listitem>
-<para>
-The type variables bound by the pattern may be 
-mentioned in ordinary type signatures or pattern 
-type signatures anywhere within their scope.
-
-</para>
-</listitem>
-
-<listitem>
-<para>
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is <emphasis>not</emphasis> universally quantified.
-
-</para>
-</listitem>
-
-<listitem>
-
-<para>
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-<programlisting>
-  f :: a -> a
-  f x = x::a
-</programlisting>
-
-It's illegal because <varname>a</varname> is not in scope in the body of <function>f</function>,
-so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
-and that is an incorrect typing.
-
+<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
+a <emphasis>type</emphasis>. (This is a change from GHC's earlier
+design.)</para></listitem>
+<listitem><para>Furthermore, distinct lexical type variables stand for distinct
+type variables.  This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
+checker, and no inference is involved.</para></listitem>
+<listitem><para>Lexical type variables may be alpha-renamed freely, without
+changing the program.</para></listitem>
+</itemizedlist>
 </para>
-</listitem>
-
-<listitem>
 <para>
-The pattern type signature is a monotype:
-</para>
-
+A <emphasis>lexically scoped type variable</emphasis> can be bound by:
 <itemizedlist>
-<listitem> <para> 
-A pattern type signature cannot contain any explicit <literal>forall</literal> quantification.
-</para> </listitem>
-
-<listitem>  <para> 
-The type variables bound by a pattern type signature can only be instantiated to monotypes,
-not to type schemes.
-</para> </listitem>
-
-<listitem>  <para> 
-There is no implicit universal quantification on pattern type signatures (in contrast to
-ordinary type signatures).
-</para> </listitem>
-
+<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
+<listitem><para>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
 </itemizedlist>
-
-</listitem>
-
-<listitem>
+</para>
 <para>
-
-The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
-scope over the methods defined in the <literal>where</literal> part.  For example:
-
-
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (<ulink
+url="http://haskell.org/onlinereport/decls.html#sect4.1.2">Section
+4.1.2</ulink> 
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
+quantified. For example, if type variable <literal>a</literal> is in scope,
+then
 <programlisting>
-  class C a where
-    op :: [a] -> a
-
-    op xs = let ys::[a]
-                ys = reverse xs
-            in
-            head ys
+  (e :: a -> a)     means     (e :: a -> a)
+  (e :: b -> b)     means     (e :: forall b. b->b)
+  (e :: a -> b)     means     (e :: forall b. a->b)
 </programlisting>
-
-
-(Not implemented in Hugs yet, Dec 98).
 </para>
-</listitem>
 
-</itemizedlist>
-
-</para>
 
 </sect3>
 
+
 <sect3 id="decl-type-sigs">
 <title>Declaration type signatures</title>
 <para>A declaration type signature that has <emphasis>explicit</emphasis>
@@ -3411,180 +3353,145 @@ quantification rules.
 </para>
 </sect3>
 
-<sect3 id="pattern-type-sigs">
-<title>Where a pattern type signature can occur</title>
-
-<para>
-A pattern type signature can occur in any pattern.  For example:
-<itemizedlist>
-
-<listitem>
-<para>
-A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
-
-
-<programlisting>
-  f ((x,y)::(a,b)) = (y,x) :: (b,a)
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
-
-<programlisting>
-  (\ (x::a, y) :: a -> x)
-</programlisting>
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in <literal>case</literal> expressions:
+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
 
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression.  For example:
 <programlisting>
-  case e of { ((x::a, y) :: (a,b)) -> x }
+  f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
 </programlisting>
-
-Note that the <literal>-&gt;</literal> symbol in a case alternative
-leads to difficulties when parsing a type signature in the pattern: in
-the absence of the extra parentheses in the example above, the parser
-would try to interpret the <literal>-&gt;</literal> as a function
-arrow and give a parse error later.
-
+Here, the type signature <literal>forall a. ST s Bool</literal> brings the 
+type variable <literal>s</literal> into scope, in the annotated expression 
+<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
 </para>
 
-</listitem>
+</sect3>
 
-<listitem>
+<sect3 id="pattern-type-sigs">
+<title>Pattern type signatures</title>
 <para>
-To avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort).  To see why,
-consider how one would parse this:
-
-
+A type signature may occur in any pattern; this is a <emphasis>pattern type
+signature</emphasis>.  
+For example:
 <programlisting>
-  \ x :: a -> b -> x
+  -- f and g assume that 'a' is already in scope
+  f = \(x::Int, y::a) -> x
+  g (x::a) = x
+  h ((x,y) :: (Int,Bool)) = (y,x)
 </programlisting>
-
-
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
 </para>
-</listitem>
-
-<listitem>
-
 <para>
- Pattern type signatures can bind existential type variables.
-For example:
-
-
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor.  For example:
 <programlisting>
   data T = forall a. MkT [a]
 
-  f :: T -> T
-  f (MkT [t::a]) = MkT t3
+  k :: T -> T
+  k (MkT [t::a]) = MkT t3
                  where
                    t3::[a] = [t,t,t]
 </programlisting>
-
-
+Here, the pattern type signature <literal>(t::a)</literal> mentions a lexical type
+variable that is not already in scope.  Indeed, it cannot already be in scope,
+because it is bound by the pattern match.  GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
 </para>
-</listitem>
-
-
-<listitem>
-
 <para>
-Pattern type signatures 
-can be used in pattern bindings:
-
-<programlisting>
-  f x = let (y, z::a) = x in ...
-  f1 x                = let (y, z::Int) = x in ...
-  f2 (x::(Int,a))     = let (y, z::a)   = x in ...
-  f3 :: (b->b)        = \x -> x
-</programlisting>
-
-In all such cases, the binding is not generalised over the pattern-bound
-type variables.  Thus <literal>f3</literal> is monomorphic; <literal>f3</literal>
-has type <literal>b -&gt; b</literal> for some type <literal>b</literal>, 
-and <emphasis>not</emphasis> <literal>forall b. b -&gt; b</literal>.
-In contrast, the binding
-<programlisting>
-  f4 :: b->b
-  f4 = \x -> x
-</programlisting>
-makes a polymorphic function, but <literal>b</literal> is not in scope anywhere
-in <literal>f4</literal>'s scope.
-
+If this seems a little odd, we think so too.  But we must have
+<emphasis>some</emphasis> way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
 </para>
-</listitem>
-</itemizedlist>
+<para>
+This is (now) the <emphasis>only</emphasis> situation in which a pattern type 
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both <literal>f</literal> and <literal>g</literal> would be
+illegal if <literal>a</literal> was not already in scope.
 </para>
-<para>Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures.  The two can be used independently or together.</para>
+
 
 </sect3>
 
+<!-- ==================== Commented out part about result type signatures 
+
 <sect3 id="result-type-sigs">
 <title>Result type signatures</title>
 
 <para>
-The result type of a function can be given a signature, thus:
-
+The result type of a function, lambda, or case expression alternative can be given a signature, thus:
 
 <programlisting>
-  f (x::a) :: [a] = [x,x,x]
-</programlisting>
-
+  {- f assumes that 'a' is already in scope -}
+  f x y :: [a] = [x,y,x]
 
-The final <literal>:: [a]</literal> after all the patterns gives a signature to the
-result type.  Sometimes this is the only way of naming the type variable
-you want:
+  g = \ x :: [Int] -> [3,4]
 
-
-<programlisting>
-  f :: Int -> [a] -> [a]
-  f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
-                        in \xs -> map g (reverse xs `zip` xs)
+  h :: forall a. [a] -> a
+  h xs = case xs of
+           (y:ys) :: a -> y
 </programlisting>
-
+The final <literal>:: [a]</literal> after the patterns of <literal>f</literal> gives the type of 
+the result of the function.  Similarly, the body of the lambda in the RHS of
+<literal>g</literal> is <literal>[Int]</literal>, and the RHS of the case
+alternative in <literal>h</literal> is <literal>a</literal>.
 </para>
+<para> A result type signature never brings new type variables into scope.</para>
 <para>
-The type variables bound in a result type signature scope over the right hand side
-of the definition. However, consider this corner-case:
+There are a couple of syntactic wrinkles.  First, notice that all three
+examples would parse quite differently with parentheses:
 <programlisting>
-  rev1 :: [a] -> [a] = \xs -> reverse xs
+  {- f assumes that 'a' is already in scope -}
+  f x (y :: [a]) = [x,y,x]
 
-  foo ys = rev (ys::[a])
+  g = \ (x :: [Int]) -> [3,4]
+
+  h :: forall a. [a] -> a
+  h xs = case xs of
+           ((y:ys) :: a) -> y
 </programlisting>
-The signature on <literal>rev1</literal> is considered a pattern type signature, not a result
-type signature, and the type variables it binds have the same scope as <literal>rev1</literal>
-itself (i.e. the right-hand side of <literal>rev1</literal> and the rest of the module too).
-In particular, the expression <literal>(ys::[a])</literal> is OK, because the type variable <literal>a</literal>
-is in scope (otherwise it would mean <literal>(ys::forall a.[a])</literal>, which would be rejected).  
-</para>
-<para>
-As mentioned above, <literal>rev1</literal> is made monomorphic by this scoping rule.
-For example, the following program would be rejected, because it claims that <literal>rev1</literal>
-is polymorphic:
+Now the signature is on the <emphasis>pattern</emphasis>; and
+<literal>h</literal> would certainly be ill-typed (since the pattern
+<literal>(y:ys)</literal> cannot have the type <literal>a</literal>.
+
+Second, to avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort).  To see why,
+consider how one would parse this:
 <programlisting>
-  rev1 :: [b] -> [b]
-  rev1 :: [a] -> [a] = \xs -> reverse xs
+  \ x :: a -> b -> x
 </programlisting>
 </para>
+</sect3>
 
+ -->
+
+<sect3 id="cls-inst-scoped-tyvars">
+<title>Class and instance declarations</title>
 <para>
-Result type signatures are not yet implemented in Hugs.
-</para>
 
+The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
+scope over the methods defined in the <literal>where</literal> part.  For example:
+
+
+<programlisting>
+  class C a where
+    op :: [a] -> a
+
+    op xs = let ys::[a]
+                ys = reverse xs
+            in
+            head ys
+</programlisting>
+</para>
 </sect3>
 
 </sect2>
@@ -3751,16 +3658,19 @@ declaration (after expansion of any type synonyms)
 where 
  <itemizedlist>
 <listitem><para>
-  The type <literal>t</literal> is an arbitrary type
+  The <literal>ci</literal> are partial applications of
+  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.
 </para></listitem>
 <listitem><para>
-  The <literal>vk+1...vn</literal> are type variables which do not occur in 
-  <literal>t</literal>, and
+  The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
 </para></listitem>
 <listitem><para>
-  The <literal>ci</literal> are partial applications of
-  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
-  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.
+  The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+  The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>, 
+  nor in the <literal>ci</literal>, and
 </para></listitem>
 <listitem><para>
   None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>, 
@@ -3773,13 +3683,8 @@ where
 Then, for each <literal>ci</literal>, the derived instance
 declaration is:
 <programlisting> 
-  instance ci (t vk+1...v) => ci (T v1...vp)
+  instance ci t => ci (T v1...vk)
 </programlisting>
-where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the 
-right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
-</para>
-<para>
-
 As an example which does <emphasis>not</emphasis> work, consider 
 <programlisting> 
   newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
@@ -3891,9 +3796,9 @@ pattern binding must have the same context.  For example, this is fine:
 <!-- ====================== Generalised algebraic data types =======================  -->
 
 <sect1 id="gadt">
-<title>Generalised Algebraic Data Types</title>
+<title>Generalised Algebraic Data Types (GADTs)</title>
 
-<para>Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you
 to give the type signatures of constructors explicitly.  For example:
 <programlisting>
   data Term a where
@@ -3914,9 +3819,20 @@ for these <literal>Terms</literal>:
   eval (If b e1 e2) = if eval b then eval e1 else eval e2
   eval (Pair e1 e2) = (eval e1, eval e2)
 </programlisting>
-These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.
 </para>
-<para> The extensions to GHC are these:
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs. 
+It is far from comprehensive, but the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+which appeared in ICFP 2006.
 <itemizedlist>
 <listitem><para>
   Data type declarations have a 'where' form, as exemplified above.  The type signature of
@@ -4008,8 +3924,8 @@ declaration, but only if the data type could also have been declared in
 Haskell-98 syntax.   For example, these two declarations are equivalent
 <programlisting>
   data Maybe1 a where {
-      Nothing1 :: Maybe a ;
-      Just1    :: a -> Maybe a
+      Nothing1 :: Maybe1 a ;
+      Just1    :: a -> Maybe1 a
     } deriving( Eq, Ord )
 
   data Maybe2 a = Nothing2 | Just2 a 
@@ -4059,19 +3975,26 @@ the result type of the <literal>case</literal> expression.  Hence the addition <
 <sect1 id="template-haskell">
 <title>Template Haskell</title>
 
-<para>Template Haskell allows you to do compile-time meta-programming in Haskell.  There is a "home page" for
-Template Haskell at <ulink url="http://www.haskell.org/th/">
-http://www.haskell.org/th/</ulink>, while
-the background to
+<para>Template Haskell allows you to do compile-time meta-programming in
+Haskell.  
+The background to
 the main technical innovations is discussed in "<ulink
 url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
 Template Meta-programming for Haskell</ulink>" (Proc Haskell Workshop 2002).
-The details of the Template Haskell design are still in flux.  Make sure you
-consult the <ulink url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online library reference material</ulink> 
+</para>
+<para>
+There is a Wiki page about
+Template Haskell at <ulink url="http://haskell.org/haskellwiki/Template_Haskell">
+http://www.haskell.org/th/</ulink>, and that is the best place to look for
+further details.
+You may also 
+consult the <ulink
+url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online
+Haskell library reference material</ulink> 
 (search for the type ExpQ).
 [Temporary: many changes to the original design are described in 
       <ulink url="http://research.microsoft.com/~simonpj/tmp/notes2.ps">"http://research.microsoft.com/~simonpj/tmp/notes2.ps"</ulink>.
-Not all of these changes are in GHC 6.2.]
+Not all of these changes are in GHC 6.6.]
 </para>
 
 <para> The first example from that paper is set out below as a worked example to help get you started. 
@@ -4772,6 +4695,150 @@ Because the preprocessor targets Haskell (rather than Core),
 
 </sect1>
 
+<!-- ==================== BANG PATTERNS =================  -->
+
+<sect1 id="sec-bang-patterns">
+<title>Bang patterns
+<indexterm><primary>Bang patterns</primary></indexterm>
+</title>
+<para>GHC supports an extension of pattern matching called <emphasis>bang
+patterns</emphasis>.   Bang patterns are under consideration for Haskell Prime.
+The <ulink
+url="http://hackage.haskell.org/trac/haskell-prime/wiki/BangPatterns">Haskell
+prime feature description</ulink> contains more discussion and examples
+than the material below.
+</para>
+<para>
+Bang patterns are enabled by the flag <option>-fbang-patterns</option>.
+</para>
+
+<sect2 id="sec-bang-patterns-informal">
+<title>Informal description of bang patterns
+</title>
+<para>
+The main idea is to add a single new production to the syntax of patterns:
+<programlisting>
+  pat ::= !pat
+</programlisting>
+Matching an expression <literal>e</literal> against a pattern <literal>!p</literal> is done by first
+evaluating <literal>e</literal> (to WHNF) and then matching the result against <literal>p</literal>.
+Example:
+<programlisting>
+f1 !x = True
+</programlisting>
+This definition makes <literal>f1</literal> is strict in <literal>x</literal>,
+whereas without the bang it would be lazy.
+Bang patterns can be nested of course:
+<programlisting>
+f2 (!x, y) = [x,y]
+</programlisting>
+Here, <literal>f2</literal> is strict in <literal>x</literal> but not in
+<literal>y</literal>.  
+A bang only really has an effect if it precedes a variable or wild-card pattern:
+<programlisting>
+f3 !(x,y) = [x,y]
+f4 (x,y)  = [x,y]
+</programlisting>
+Here, <literal>f3</literal> and <literal>f4</literal> are identical; putting a bang before a pattern that
+forces evaluation anyway does nothing.
+</para><para>
+Bang patterns work in <literal>case</literal> expressions too, of course:
+<programlisting>
+g5 x = let y = f x in body
+g6 x = case f x of { y -&gt; body }
+g7 x = case f x of { !y -&gt; body }
+</programlisting>
+The functions <literal>g5</literal> and <literal>g6</literal> mean exactly the same thing.  
+But <literal>g7</literal> evalutes <literal>(f x)</literal>, binds <literal>y</literal> to the
+result, and then evaluates <literal>body</literal>.
+</para><para>
+Bang patterns work in <literal>let</literal> and <literal>where</literal>
+definitions too. For example:
+<programlisting>
+let ![x,y] = e in b
+</programlisting>
+is a strict pattern: operationally, it evaluates <literal>e</literal>, matches
+it against the pattern <literal>[x,y]</literal>, and then evaluates <literal>b</literal>
+The "<literal>!</literal>" should not be regarded as part of the pattern; after all,
+in a function argument <literal>![x,y]</literal> means the 
+same as <literal>[x,y]</literal>.  Rather, the "<literal>!</literal>" 
+is part of the syntax of <literal>let</literal> bindings.
+</para>
+</sect2>
+
+
+<sect2 id="sec-bang-patterns-sem">
+<title>Syntax and semantics
+</title>
+<para>
+
+We add a single new production to the syntax of patterns:
+<programlisting>
+  pat ::= !pat
+</programlisting>
+There is one problem with syntactic ambiguity.  Consider:
+<programlisting>
+f !x = 3
+</programlisting>
+Is this a definition of the infix function "<literal>(!)</literal>",
+or of the "<literal>f</literal>" with a bang pattern? GHC resolves this
+ambiguity inf favour of the latter.  If you want to define
+<literal>(!)</literal> with bang-patterns enabled, you have to do so using
+prefix notation:
+<programlisting>
+(!) f x = 3
+</programlisting>
+The semantics of Haskell pattern matching is described in <ulink
+url="http://haskell.org/onlinereport/exps.html#sect3.17.2">
+Section 3.17.2</ulink> of the Haskell Report.  To this description add 
+one extra item 10, saying:
+<itemizedlist><listitem><para>Matching
+the pattern <literal>!pat</literal> against a value <literal>v</literal> behaves as follows:
+<itemizedlist><listitem><para>if <literal>v</literal> is bottom, the match diverges</para></listitem>
+               <listitem><para>otherwise, <literal>pat</literal> is matched against
+               <literal>v</literal></para></listitem>
+</itemizedlist>
+</para></listitem></itemizedlist>
+Similarly, in Figure 4 of  <ulink url="http://haskell.org/onlinereport/exps.html#sect3.17.3">
+Section 3.17.3</ulink>, add a new case (t):
+<programlisting>
+case v of { !pat -> e; _ -> e' }
+   = v `seq` case v of { pat -> e; _ -> e' }
+</programlisting>
+</para><para>
+That leaves let expressions, whose translation is given in 
+<ulink url="http://haskell.org/onlinereport/exps.html#sect3.12">Section
+3.12</ulink>
+of the Haskell Report.
+In the translation box, first apply 
+the following transformation:  for each pattern <literal>pi</literal> that is of 
+form <literal>!qi = ei</literal>, transform it to <literal>(xi,!qi) = ((),ei)</literal>, and and replace <literal>e0</literal> 
+by <literal>(xi `seq` e0)</literal>.  Then, when none of the left-hand-side patterns
+have a bang at the top, apply the rules in the existing box.
+</para>
+<para>The effect of the let rule is to force complete matching of the pattern
+<literal>qi</literal> before evaluation of the body is begun.  The bang is
+retained in the translated form in case <literal>qi</literal> is a variable,
+thus:
+<programlisting>
+  let !y = f x in b
+</programlisting>
+
+</para>
+<para>
+The let-binding can be recursive.  However, it is much more common for
+the let-binding to be non-recursive, in which case the following law holds:
+<literal>(let !p = rhs in body)</literal>
+     is equivalent to
+<literal>(case rhs of !p -> body)</literal>
+</para>
+<para>
+A pattern with a bang at the outermost level is not allowed at the top level of
+a module.
+</para>
+</sect2>
+</sect1>
+
 <!-- ==================== ASSERTIONS =================  -->
 
 <sect1 id="sec-assertions">
@@ -6016,7 +6083,7 @@ r)
                    GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
 r) ->
               tpl2})
-        (%note "foo"
+        (%note "bar"
          eta);
 </programlisting>
 
@@ -6072,7 +6139,7 @@ shortcoming is something that could be fixed, with some kind of pragma.)
 </para>
 </sect2>
 
-<sect2> <title>The <literal>inline</literal> function </title>
+<sect2> <title>The <literal>lazy</literal> function </title>
 <para>
 The <literal>lazy</literal> function restrains strictness analysis a little:
 <programlisting>
@@ -6097,15 +6164,27 @@ look strict in <literal>y</literal> which would defeat the whole
 purpose of <literal>par</literal>.
 </para>
 </sect2>
+
+<sect2> <title>The <literal>unsafeCoerce#</literal> function </title>
+<para>
+The function <literal>unsafeCoerce#</literal> allows you to side-step the
+typechecker entirely.  It has type
+<programlisting>
+  unsafeCoerce# :: a -> b
+</programlisting>
+That is, it allows you to coerce any type into any other type.  If you use this
+function, you had better get it right, otherwise segmentation faults await. 
+It is generally used when you want to write a program that you know is
+well-typed, but where Haskell's type system is not expressive enough to prove
+that it is well typed.
+</para>
+</sect2>
 </sect1>
 
 
 <sect1 id="generic-classes">
 <title>Generic classes</title>
 
-    <para>(Note: support for generic classes is currently broken in
-    GHC 5.02).</para>
-
 <para>
 The ideas behind this extension are described in detail in "Derivable type classes",
 Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
@@ -6356,6 +6435,51 @@ Just to finish with, here's another example I rather like:
 </sect2>
 </sect1>
 
+<sect1 id="monomorphism">
+<title>Control over monomorphism</title>
+
+<para>GHC supports two flags that control the way in which generalisation is
+carried out at let and where bindings.
+</para>
+
+<sect2>
+<title>Switching off the dreaded Monomorphism Restriction</title>
+          <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
+
+<para>Haskell's monomorphism restriction (see 
+<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.5">Section
+4.5.5</ulink>
+of the Haskell Report)
+can be completely switched off by
+<option>-fno-monomorphism-restriction</option>.
+</para>
+</sect2>
+
+<sect2>
+<title>Monomorphic pattern bindings</title>
+          <indexterm><primary><option>-fno-mono-pat-binds</option></primary></indexterm>
+          <indexterm><primary><option>-fmono-pat-binds</option></primary></indexterm>
+
+         <para> As an experimental change, we are exploring the possibility of
+         making pattern bindings monomorphic; that is, not generalised at all.  
+           A pattern binding is a binding whose LHS has no function arguments,
+           and is not a simple variable.  For example:
+<programlisting>
+  f x = x                    -- Not a pattern binding
+  f = \x -> x                -- Not a pattern binding
+  f :: Int -> Int = \x -> x  -- Not a pattern binding
+
+  (g,h) = e                  -- A pattern binding
+  (f) = e                    -- A pattern binding
+  [x] = e                    -- A pattern binding
+</programlisting>
+Experimentally, GHC now makes pattern bindings monomorphic <emphasis>by
+default</emphasis>.  Use <option>-fno-mono-pat-binds</option> to recover the
+standard behaviour.
+</para>
+</sect2>
+</sect1>
+
 
 
 <!-- Emacs stuff: