+ data Person where
+ 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).
+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>
+
+<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>
+As in the case of existentials declared using the Haskell-98-like record syntax
+(<xref linkend="existential-records"/>),
+record-selector functions are generated only for those fields that have well-typed
+selectors.
+Here is the example of that section, in GADT-style syntax:
+<programlisting>
+data Counter a where
+ NewCounter { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+ :: Counter a
+</programlisting>
+As before, only one selector function is generated here, that for <literal>tag</literal>.
+Nevertheless, you can still use all the field names in pattern matching and record construction.
+</para></listitem>
+</itemizedlist></para>
+</sect2>
+
+<sect2 id="gadt">
+<title>Generalised Algebraic Data Types (GADTs)</title>
+
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types
+by allowing constructors to have richer return types. Here is an example:
+<programlisting>
+ data Term a where
+ Lit :: Int -> Term Int
+ Succ :: Term Int -> Term Int
+ IsZero :: Term Int -> Term Bool
+ If :: Term Bool -> Term a -> Term a -> Term a
+ Pair :: Term a -> Term b -> Term (a,b)
+</programlisting>
+Notice that the return type of the constructors is not always <literal>Term a</literal>, as is the
+case with ordinary data types. This generality allows us to
+write a well-typed <literal>eval</literal> function
+for these <literal>Terms</literal>:
+<programlisting>
+ eval :: Term a -> a
+ eval (Lit i) = i
+ eval (Succ t) = 1 + eval t
+ eval (IsZero t) = eval t == 0
+ eval (If b e1 e2) = if eval b then eval e1 else eval e2
+ eval (Pair e1 e2) = (eval e1, eval e2)
+</programlisting>
+The key point about GADTs is that <emphasis>pattern matching causes type refinement</emphasis>.
+For example, in the right hand side of the equation
+<programlisting>
+ eval :: Term a -> a
+ eval (Lit i) = ...
+</programlisting>
+the type <literal>a</literal> is refined to <literal>Int</literal>. That's the whole point!
+A precise specification of the type rules is beyond what this user manual aspires to,
+but the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/">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://www.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. The extension is enabled with
+<option>-XGADTs</option>. The <option>-XGADTs</option> flag also sets <option>-XRelaxedPolyRec</option>.
+<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> need not be a type variable (e.g. the <literal>Lit</literal>
+constructor).
+</para></listitem>
+
+<listitem><para>
+It 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>
+
+<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>
+
+<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>
+
+</sect2>
+</sect1>
+
+<!-- ====================== End of Generalised algebraic data types ======================= -->
+
+<sect1 id="deriving">
+<title>Extensions to the "deriving" mechanism</title>
+
+<sect2 id="deriving-inferred">
+<title>Inferred context for deriving clauses</title>
+
+<para>
+The Haskell Report is vague about exactly when a <literal>deriving</literal> clause is
+legal. For example:
+<programlisting>
+ data T0 f a = MkT0 a deriving( Eq )
+ data T1 f a = MkT1 (f a) deriving( Eq )
+ data T2 f a = MkT2 (f (f a)) deriving( Eq )
+</programlisting>
+The natural generated <literal>Eq</literal> code would result in these instance declarations:
+<programlisting>
+ instance Eq a => Eq (T0 f a) where ...
+ instance Eq (f a) => Eq (T1 f a) where ...
+ instance Eq (f (f a)) => Eq (T2 f a) where ...
+</programlisting>
+The first of these is obviously fine. The second is still fine, although less obviously.
+The third is not Haskell 98, and risks losing termination of instances.
+</para>
+<para>
+GHC takes a conservative position: it accepts the first two, but not the third. The rule is this:
+each constraint in the inferred instance context must consist only of type variables,
+with no repetitions.
+</para>
+<para>
+This rule is applied regardless of flags. If you want a more exotic context, you can write
+it yourself, using the <link linkend="stand-alone-deriving">standalone deriving mechanism</link>.
+</para>
+</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>-XStandaloneDeriving</literal>:
+<programlisting>
+ data Foo a = Bar a | Baz String
+
+ deriving instance Eq a => Eq (Foo a)
+</programlisting>
+The syntax is identical to that of an ordinary instance declaration apart from (a) the keyword
+<literal>deriving</literal>, and (b) the absence of the <literal>where</literal> part.
+Note the following points:
+<itemizedlist>
+<listitem><para>
+You must supply an explicit context (in the example the context is <literal>(Eq a)</literal>),
+exactly as you would in an ordinary instance declaration.
+(In contrast, in a <literal>deriving</literal> clause
+attached to a data type declaration, the context is inferred.)
+</para></listitem>
+
+<listitem><para>
+A <literal>deriving instance</literal> declaration
+must obey the same rules concerning form and termination as ordinary instance declarations,
+controlled by the same flags; see <xref linkend="instance-decls"/>.
+</para></listitem>
+
+<listitem><para>
+Unlike a <literal>deriving</literal>
+declaration attached to a <literal>data</literal> declaration, the instance can be more specific
+than the data type (assuming you also use
+<literal>-XFlexibleInstances</literal>, <xref linkend="instance-rules"/>). Consider
+for example
+<programlisting>
+ data Foo a = Bar a | Baz String
+
+ deriving instance Eq a => Eq (Foo [a])
+ deriving instance Eq a => Eq (Foo (Maybe a))
+</programlisting>
+This will generate a derived instance for <literal>(Foo [a])</literal> and <literal>(Foo (Maybe a))</literal>,
+but other types such as <literal>(Foo (Int,Bool))</literal> will not be an instance of <literal>Eq</literal>.
+</para></listitem>
+
+<listitem><para>
+Unlike a <literal>deriving</literal>
+declaration attached to a <literal>data</literal> declaration,
+GHC does not restrict the form of the data type. Instead, GHC simply generates the appropriate
+boilerplate code for the specified class, and typechecks it. If there is a type error, it is
+your problem. (GHC will show you the offending code if it has a type error.)
+The merit of this is that you can derive instances for GADTs and other exotic
+data types, providing only that the boilerplate code does indeed typecheck. For example:
+<programlisting>
+ data T a where
+ T1 :: T Int
+ T2 :: T Bool
+
+ deriving instance Show (T a)
+</programlisting>
+In this example, you cannot say <literal>... deriving( Show )</literal> on the
+data type declaration for <literal>T</literal>,
+because <literal>T</literal> is a GADT, but you <emphasis>can</emphasis> generate
+the instance declaration using stand-alone deriving.
+</para>
+</listitem>
+
+<listitem>
+<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)
+
+ deriving instance MonadState Int Foo
+</programlisting>
+GHC always treats the <emphasis>last</emphasis> parameter of the instance
+(<literal>Foo</literal> in this example) as the type whose instance is being derived.
+</para></listitem>
+</itemizedlist></para>
+
+</sect2>
+
+
+<sect2 id="deriving-typeable">
+<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
+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 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>.
+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>
+</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">
+<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,
+using the flag <option>-XGeneralizedNewtypeDeriving</option>,
+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