+ eval :: Term a -> a
+ eval (Lit i) = i
+ eval (Succ t) = 1 + eval t
+ eval (IsZero t) = eval t == 0
+ eval (If b e1 e2) = if eval b then eval e1 else eval e2
+ eval (Pair e1 e2) = (eval e1, eval e2)
+</programlisting>
+The key point about GADTs is that <emphasis>pattern matching causes type refinement</emphasis>.
+For example, in the right hand side of the equation
+<programlisting>
+ eval :: Term a -> a
+ eval (Lit i) = ...
+</programlisting>
+the type <literal>a</literal> is refined to <literal>Int</literal>. That's the whole point!
+A precise specification of the type rules is beyond what this user manual aspires to,
+but the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+(ICFP 2006).
+The general principle is this: <emphasis>type refinement is only carried out
+based on user-supplied type annotations</emphasis>.
+So if no type signature is supplied for <literal>eval</literal>, no type refinement happens,
+and lots of obscure error messages will
+occur. However, the refinement is quite general. For example, if we had:
+<programlisting>
+ eval :: Term a -> a -> a
+ eval (Lit i) j = i+j
+</programlisting>
+the pattern match causes the type <literal>a</literal> to be refined to <literal>Int</literal> (because of the type
+of the constructor <literal>Lit</literal>), and that refinement also applies to the type of <literal>j</literal>, and
+the result type of the <literal>case</literal> expression. Hence the addition <literal>i+j</literal> is legal.
+</para>
+<para>
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.
+</para>
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs.
+<itemizedlist>
+<listitem><para>
+A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>);
+the old Haskell-98 syntax for data declarations always declares an ordinary data type.
+The result type of each constructor must begin with the type constructor being defined,
+but for a GADT the arguments to the type constructor can be arbitrary monotypes.
+For example, in the <literal>Term</literal> data
+type above, the type of each constructor must end with <literal>Term ty</literal>, but
+the <literal>ty</literal> may not be a type variable (e.g. the <literal>Lit</literal>
+constructor).
+</para></listitem>
+
+<listitem><para>
+You cannot use a <literal>deriving</literal> clause for a GADT; only for
+an ordianary data type.
+</para></listitem>
+
+<listitem><para>
+As mentioned in <xref linkend="gadt-style"/>, record syntax is supported.
+For example:
+<programlisting>
+ data Term a where
+ Lit { val :: Int } :: Term Int
+ Succ { num :: Term Int } :: Term Int
+ Pred { num :: Term Int } :: Term Int
+ IsZero { arg :: Term Int } :: Term Bool
+ Pair { arg1 :: Term a
+ , arg2 :: Term b
+ } :: Term (a,b)
+ If { cnd :: Term Bool
+ , tru :: Term a
+ , fls :: Term a
+ } :: Term a
+</programlisting>
+However, for GADTs there is the following additional constraint:
+every constructor that has a field <literal>f</literal> must have
+the same result type (modulo alpha conversion)
+Hence, in the above example, we cannot merge the <literal>num</literal>
+and <literal>arg</literal> fields above into a
+single name. Although their field types are both <literal>Term Int</literal>,
+their selector functions actually have different types:
+
+<programlisting>
+ num :: Term Int -> Term Int
+ arg :: Term Bool -> Term Int
+</programlisting>
+</para></listitem>
+
+</itemizedlist>
+</para>
+
+</sect2>
+
+<!-- ====================== End of Generalised algebraic data types ======================= -->
+
+
+<sect2 id="deriving-typeable">
+<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
+
+<para>
+Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type
+declaration, to generate a standard instance declaration for classes specified in the <literal>deriving</literal> clause.
+In Haskell 98, the only classes that may appear in the <literal>deriving</literal> clause are the standard
+classes <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal>, <literal>Ix</literal>, <literal>Bounded</literal>, <literal>Read</literal>, and <literal>Show</literal>.
+</para>
+<para>
+GHC extends this list with two more classes that may be automatically derived
+(provided the <option>-fglasgow-exts</option> flag is specified):
+<literal>Typeable</literal>, and <literal>Data</literal>. These classes are defined in the library
+modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively, and the
+appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
+</para>
+<para>An instance of <literal>Typeable</literal> can only be derived if the
+data type has seven or fewer type parameters, all of kind <literal>*</literal>.
+The reason for this is that the <literal>Typeable</literal> class is derived using the scheme
+described in
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/hmap/gmap2.ps">
+Scrap More Boilerplate: Reflection, Zips, and Generalised Casts
+</ulink>.
+(Section 7.4 of the paper describes the multiple <literal>Typeable</literal> classes that
+are used, and only <literal>Typeable1</literal> up to
+<literal>Typeable7</literal> are provided in the library.)
+In other cases, there is nothing to stop the programmer writing a <literal>TypableX</literal>
+class, whose kind suits that of the data type constructor, and
+then writing the data type instance by hand.
+</para>
+</sect2>
+
+<sect2 id="newtype-deriving">
+<title>Generalised derived instances for newtypes</title>
+
+<para>
+When you define an abstract type using <literal>newtype</literal>, you may want
+the new type to inherit some instances from its representation. In
+Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
+other classes you have to write an explicit instance declaration. For
+example, if you define
+
+<programlisting>
+ newtype Dollars = Dollars Int
+</programlisting>
+
+and you want to use arithmetic on <literal>Dollars</literal>, you have to
+explicitly define an instance of <literal>Num</literal>:
+
+<programlisting>
+ instance Num Dollars where
+ Dollars a + Dollars b = Dollars (a+b)
+ ...
+</programlisting>
+All the instance does is apply and remove the <literal>newtype</literal>
+constructor. It is particularly galling that, since the constructor
+doesn't appear at run-time, this instance declaration defines a
+dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
+dictionary, only slower!
+</para>
+
+
+<sect3> <title> Generalising the deriving clause </title>
+<para>
+GHC now permits such instances to be derived instead, so one can write
+<programlisting>
+ newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+</programlisting>
+
+and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
+for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
+derives an instance declaration of the form
+
+<programlisting>
+ instance Num Int => Num Dollars
+</programlisting>
+
+which just adds or removes the <literal>newtype</literal> constructor according to the type.
+</para>
+<para>
+
+We can also derive instances of constructor classes in a similar
+way. For example, suppose we have implemented state and failure monad
+transformers, such that
+
+<programlisting>
+ instance Monad m => Monad (State s m)
+ instance Monad m => Monad (Failure m)
+</programlisting>
+In Haskell 98, we can define a parsing monad by
+<programlisting>
+ type Parser tok m a = State [tok] (Failure m) a
+</programlisting>
+
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract,
+without needing to write an instance of class <literal>Monad</literal>, via
+
+<programlisting>
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving Monad
+</programlisting>
+In this case the derived instance declaration is of the form
+<programlisting>
+ instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
+</programlisting>
+
+Notice that, since <literal>Monad</literal> is a constructor class, the
+instance is a <emphasis>partial application</emphasis> of the new type, not the
+entire left hand side. We can imagine that the type declaration is
+``eta-converted'' to generate the context of the instance
+declaration.
+</para>
+<para>
+
+We can even derive instances of multi-parameter classes, provided the
+newtype is the last class parameter. In this case, a ``partial
+application'' of the class appears in the <literal>deriving</literal>
+clause. For example, given the class
+
+<programlisting>
+ class StateMonad s m | m -> s where ...
+ instance Monad m => StateMonad s (State s m) where ...
+</programlisting>
+then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by
+<programlisting>
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving (Monad, StateMonad [tok])
+</programlisting>
+
+The derived instance is obtained by completing the application of the
+class to the new type:
+
+<programlisting>
+ instance StateMonad [tok] (State [tok] (Failure m)) =>
+ StateMonad [tok] (Parser tok m)
+</programlisting>
+</para>
+<para>
+
+As a result of this extension, all derived instances in newtype
+ declarations are treated uniformly (and implemented just by reusing
+the dictionary for the representation type), <emphasis>except</emphasis>
+<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
+the newtype and its representation.
+</para>
+</sect3>
+
+<sect3> <title> A more precise specification </title>
+<para>
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
+
+<programlisting>
+ newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)
+</programlisting>
+
+where
+ <itemizedlist>
+<listitem><para>
+ The <literal>ci</literal> are partial applications of
+ classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+ is exactly <literal>j+1</literal>. That is, <literal>C</literal> lacks exactly one type argument.
+</para></listitem>
+<listitem><para>
+ The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
+</para></listitem>
+<listitem><para>
+ The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+ The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>,
+ nor in the <literal>ci</literal>, and
+</para></listitem>
+<listitem><para>
+ None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>,
+ <literal>Typeable</literal>, or <literal>Data</literal>. These classes
+ should not "look through" the type or its constructor. You can still
+ derive these classes for a newtype, but it happens in the usual way, not
+ via this new mechanism.
+</para></listitem>
+</itemizedlist>
+Then, for each <literal>ci</literal>, the derived instance
+declaration is:
+<programlisting>
+ instance ci t => ci (T v1...vk)
+</programlisting>
+As an example which does <emphasis>not</emphasis> work, consider
+<programlisting>
+ newtype NonMonad m s = NonMonad (State s m s) deriving Monad
+</programlisting>
+Here we cannot derive the instance
+<programlisting>
+ instance Monad (State s m) => Monad (NonMonad m)
+</programlisting>
+
+because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
+and so cannot be "eta-converted" away. It is a good thing that this
+<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
+not, in fact, a monad --- for the same reason. Try defining
+<literal>>>=</literal> with the correct type: you won't be able to.
+</para>
+<para>
+
+Notice also that the <emphasis>order</emphasis> of class parameters becomes
+important, since we can only derive instances for the last one. If the
+<literal>StateMonad</literal> class above were instead defined as
+
+<programlisting>
+ class StateMonad m s | m -> s where ...
+</programlisting>
+
+then we would not have been able to derive an instance for the
+<literal>Parser</literal> type above. We hypothesise that multi-parameter
+classes usually have one "main" parameter for which deriving new
+instances is most interesting.
+</para>
+<para>Lastly, all of this applies only for classes other than
+<literal>Read</literal>, <literal>Show</literal>, <literal>Typeable</literal>,
+and <literal>Data</literal>, for which the built-in derivation applies (section
+4.3.3. of the Haskell Report).
+(For the standard classes <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Ix</literal>, and <literal>Bounded</literal> it is immaterial whether
+the standard method is used or the one described here.)
+</para>
+</sect3>
+
+</sect2>
+
+<sect2 id="stand-alone-deriving">
+<title>Stand-alone deriving declarations</title>
+
+<para>
+GHC now allows stand-alone <literal>deriving</literal> declarations, enabled by <literal>-fglasgow-exts</literal>:
+<programlisting>
+ data Foo a = Bar a | Baz String
+
+ derive instance Eq (Foo a)
+</programlisting>
+The token "<literal>derive</literal>" is a keyword only when followed by "<literal>instance</literal>";
+you can use it as a variable name elsewhere.</para>
+<para>The stand-alone syntax is generalised for newtypes in exactly the same
+way that ordinary <literal>deriving</literal> clauses are generalised (<xref linkend="newtype-deriving"/>).
+For example:
+<programlisting>
+ newtype Foo a = MkFoo (State Int a)
+
+ derive instance MonadState Int Foo
+</programlisting>
+GHC always treats the <emphasis>last</emphasis> parameter of the instance
+(<literal>Foo</literal> in this exmample) as the type whose instance is being derived.
+</para>
+
+</sect2>
+
+</sect1>
+
+
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="other-type-extensions">
+<title>Other type system extensions</title>
+
+<sect2 id="multi-param-type-classes">
+<title>Class declarations</title>
+
+<para>
+This section, and the next one, documents GHC's type-class extensions.
+There's lots of background in the paper <ulink
+url="http://research.microsoft.com/~simonpj/Papers/type-class-design-space" >Type
+classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
+Jones, Erik Meijer).
+</para>
+<para>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>
+
+<sect3>
+<title>Multi-parameter type classes</title>
+<para>
+Multi-parameter type classes are permitted. For example:
+
+
+<programlisting>
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc.
+</programlisting>
+
+</para>
+</sect3>
+
+<sect3>
+<title>The superclasses of a class declaration</title>
+
+<para>
+There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic. So these class declarations are OK:
+
+
+<programlisting>
+ class Functor (m k) => FiniteMap m k where
+ ...
+
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
+</programlisting>
+
+
+</para>
+<para>
+As in Haskell 98, The class hierarchy must be acyclic. However, the definition
+of "acyclic" involves only the superclass relationships. For example,
+this is OK:
+
+
+<programlisting>
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
+</programlisting>
+
+
+Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
+class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>. (It
+would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
+</para>
+</sect3>
+
+
+
+
+<sect3 id="class-method-types">
+<title>Class method types</title>
+
+<para>
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
+<programlisting>
+ class Seq s a where
+ fromList :: [a] -> s a
+ elem :: Eq a => a -> s a -> Bool
+</programlisting>
+The type of <literal>elem</literal> is illegal in Haskell 98, because it
+contains the constraint <literal>Eq a</literal>, constrains only the
+class type variable (in this case <literal>a</literal>).
+GHC lifts this restriction.
+</para>
+
+
+</sect3>
+</sect2>
+
+<sect2 id="functional-dependencies">
+<title>Functional dependencies
+</title>
+
+<para> Functional dependencies are implemented as described by Mark Jones
+in “<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>”, Mark P. Jones,
+In Proceedings of the 9th European Symposium on Programming,
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
+</para>
+<para>
+Functional dependencies are introduced by a vertical bar in the syntax of a
+class declaration; e.g.
+<programlisting>
+ class (Monad m) => MonadState s m | m -> s where ...
+
+ class Foo a b c | a b -> c where ...
+</programlisting>
+There should be more documentation, but there isn't (yet). Yell if you need it.
+</para>
+
+<sect3><title>Rules for functional dependencies </title>
+<para>
+In a class declaration, all of the class type variables must be reachable (in the sense
+mentioned in <xref linkend="type-restrictions"/>)
+from the free variables of each method type.
+For example:
+
+<programlisting>
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+
+is not OK, because the type of <literal>empty</literal> doesn't mention
+<literal>a</literal>. Functional dependencies can make the type variable
+reachable:
+<programlisting>
+ class Coll s a | s -> a where
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+
+Alternatively <literal>Coll</literal> might be rewritten
+
+<programlisting>
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
+</programlisting>
+
+
+which makes the connection between the type of a collection of
+<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
+
+
+<programlisting>
+ class CollE s where
+ empty :: s
+
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>
+
+
+<sect3>
+<title>Background on functional dependencies</title>
+
+<para>The following description of the motivation and use of functional dependencies is taken
+from the Hugs user manual, reproduced here (with minor changes) by kind
+permission of Mark Jones.
+</para>
+<para>
+Consider the following class, intended as part of a
+library for collection types:
+<programlisting>
+ class Collects e ce where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
+</programlisting>
+The type variable e used here represents the element type, while ce is the type
+of the container itself. Within this framework, we might want to define
+instances of this class for lists or characteristic functions (both of which
+can be used to represent collections of any equality type), bit sets (which can
+be used to represent collections of characters), or hash tables (which can be
+used to represent any collection whose elements have a hash function). Omitting
+standard implementation details, this would lead to the following declarations:
+<programlisting>
+ instance Eq e => Collects e [e] where ...