+<para>
+GHC allows type constructors, classes, and type variables to be operators, and
+to be written infix, very much like expressions. More specifically:
+<itemizedlist>
+<listitem><para>
+ A type constructor or class can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
+ The lexical syntax is the same as that for data constructors.
+ </para></listitem>
+<listitem><para>
+ Data type and type-synonym declarations can be written infix, parenthesised
+ if you want further arguments. E.g.
+<screen>
+ data a :*: b = Foo a b
+ type a :+: b = Either a b
+ class a :=: b where ...
+
+ data (a :**: b) x = Baz a b x
+ type (a :++: b) y = Either (a,b) y
+</screen>
+ </para></listitem>
+<listitem><para>
+ Types, and class constraints, can be written infix. For example
+ <screen>
+ x :: Int :*: Bool
+ f :: (a :=: b) => a -> b
+ </screen>
+ </para></listitem>
+<listitem><para>
+ A type variable can be an (unqualified) operator e.g. <literal>+</literal>.
+ The lexical syntax is the same as that for variable operators, excluding "(.)",
+ "(!)", and "(*)". In a binding position, the operator must be
+ parenthesised. For example:
+<programlisting>
+ type T (+) = Int + Int
+ f :: T Either
+ f = Left 3
+
+ liftA2 :: Arrow (~>)
+ => (a -> b -> c) -> (e ~> a) -> (e ~> b) -> (e ~> c)
+ liftA2 = ...
+</programlisting>
+ </para></listitem>
+<listitem><para>
+ Back-quotes work
+ as for expressions, both for type constructors and type variables; e.g. <literal>Int `Either` Bool</literal>, or
+ <literal>Int `a` Bool</literal>. Similarly, parentheses work the same; e.g. <literal>(:*:) Int Bool</literal>.
+ </para></listitem>
+<listitem><para>
+ Fixities may be declared for type constructors, or classes, just as for data constructors. However,
+ one cannot distinguish between the two in a fixity declaration; a fixity declaration
+ sets the fixity for a data constructor and the corresponding type constructor. For example:
+<screen>
+ infixl 7 T, :*:
+</screen>
+ sets the fixity for both type constructor <literal>T</literal> and data constructor <literal>T</literal>,
+ and similarly for <literal>:*:</literal>.
+ <literal>Int `a` Bool</literal>.
+ </para></listitem>
+<listitem><para>
+ Function arrow is <literal>infixr</literal> with fixity 0. (This might change; I'm not sure what it should be.)
+ </para></listitem>
+
+</itemizedlist>
+</para>
+</sect2>
+
+<sect2 id="type-synonyms">
+<title>Liberalised type synonyms</title>
+
+<para>
+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.
+
+<itemizedlist>
+<listitem> <para>You can write a <literal>forall</literal> (including overloading)
+in a type synonym, thus:
+<programlisting>
+ type Discard a = forall b. Show b => a -> b -> (a, String)
+
+ f :: Discard a
+ f x y = (x, show y)
+
+ g :: Discard Int -> (Int,String) -- A rank-2 type
+ g f = f 3 True
+</programlisting>
+</para>
+</listitem>
+
+<listitem><para>
+If you also use <option>-XUnboxedTuples</option>,
+you can write an unboxed tuple in a type synonym:
+<programlisting>
+ type Pr = (# Int, Int #)
+
+ h :: Int -> Pr
+ h x = (# x, x #)
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can apply a type synonym to a forall type:
+<programlisting>
+ type Foo a = a -> a -> Bool
+
+ f :: Foo (forall b. b->b)
+</programlisting>
+After expanding the synonym, <literal>f</literal> has the legal (in GHC) type:
+<programlisting>
+ f :: (forall b. b->b) -> (forall b. b->b) -> Bool
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can apply a type synonym to a partially applied type synonym:
+<programlisting>
+ type Generic i o = forall x. i x -> o x
+ type Id x = x
+
+ foo :: Generic Id []
+</programlisting>
+After expanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+<programlisting>
+ foo :: forall x. x -> [x]
+</programlisting>
+</para></listitem>
+
+</itemizedlist>
+</para>
+
+<para>
+GHC currently does kind checking before expanding synonyms (though even that
+could be changed.)
+</para>
+<para>
+After expanding type synonyms, GHC does validity checking on types, looking for
+the following mal-formedness which isn't detected simply by kind checking:
+<itemizedlist>
+<listitem><para>
+Type constructor applied to a type involving for-alls.
+</para></listitem>
+<listitem><para>
+Unboxed tuple on left of an arrow.
+</para></listitem>
+<listitem><para>
+Partially-applied type synonym.
+</para></listitem>
+</itemizedlist>
+So, for example,
+this will be rejected:
+<programlisting>
+ type Pr = (# Int, Int #)
+
+ h :: Pr -> Int
+ h x = ...
+</programlisting>
+because GHC does not allow unboxed tuples on the left of a function arrow.
+</para>
+</sect2>
+
+
+<sect2 id="existential-quantification">
+<title>Existentially quantified data constructors
+</title>
+
+<para>
+The idea of using existential quantification in data type declarations
+was suggested by Perry, and implemented in Hope+ (Nigel Perry, <emphasis>The Implementation
+of Practical Functional Programming Languages</emphasis>, PhD Thesis, University of
+London, 1991). It was later formalised by Laufer and Odersky
+(<emphasis>Polymorphic type inference and abstract data types</emphasis>,
+TOPLAS, 16(5), pp1411-1430, 1994).
+It's been in Lennart
+Augustsson's <command>hbc</command> Haskell compiler for several years, and
+proved very useful. Here's the idea. Consider the declaration:
+</para>
+
+<para>
+
+<programlisting>
+ data Foo = forall a. MkFoo a (a -> Bool)
+ | Nil
+</programlisting>
+
+</para>
+
+<para>
+The data type <literal>Foo</literal> has two constructors with types:
+</para>
+
+<para>
+
+<programlisting>
+ MkFoo :: forall a. a -> (a -> Bool) -> Foo
+ Nil :: Foo
+</programlisting>
+
+</para>
+
+<para>
+Notice that the type variable <literal>a</literal> in the type of <function>MkFoo</function>
+does not appear in the data type itself, which is plain <literal>Foo</literal>.
+For example, the following expression is fine:
+</para>
+
+<para>
+
+<programlisting>
+ [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
+</programlisting>
+
+</para>
+
+<para>
+Here, <literal>(MkFoo 3 even)</literal> packages an integer with a function
+<function>even</function> that maps an integer to <literal>Bool</literal>; and <function>MkFoo 'c'
+isUpper</function> packages a character with a compatible function. These
+two things are each of type <literal>Foo</literal> and can be put in a list.
+</para>
+
+<para>
+What can we do with a value of type <literal>Foo</literal>?. In particular,
+what happens when we pattern-match on <function>MkFoo</function>?
+</para>
+
+<para>
+
+<programlisting>
+ f (MkFoo val fn) = ???
+</programlisting>
+
+</para>
+
+<para>
+Since all we know about <literal>val</literal> and <function>fn</function> is that they
+are compatible, the only (useful) thing we can do with them is to
+apply <function>fn</function> to <literal>val</literal> to get a boolean. For example:
+</para>
+
+<para>
+
+<programlisting>
+ f :: Foo -> Bool
+ f (MkFoo val fn) = fn val
+</programlisting>
+
+</para>
+
+<para>
+What this allows us to do is to package heterogeneous values
+together with a bunch of functions that manipulate them, and then treat
+that collection of packages in a uniform manner. You can express
+quite a bit of object-oriented-like programming this way.
+</para>
+
+<sect3 id="existential">
+<title>Why existential?
+</title>
+
+<para>
+What has this to do with <emphasis>existential</emphasis> quantification?
+Simply that <function>MkFoo</function> has the (nearly) isomorphic type
+</para>
+
+<para>
+
+<programlisting>
+ MkFoo :: (exists a . (a, a -> Bool)) -> Foo
+</programlisting>
+
+</para>
+
+<para>
+But Haskell programmers can safely think of the ordinary
+<emphasis>universally</emphasis> quantified type given above, thereby avoiding
+adding a new existential quantification construct.
+</para>
+
+</sect3>
+
+<sect3 id="existential-with-context">
+<title>Existentials and type classes</title>
+
+<para>
+An easy extension is to allow
+arbitrary contexts before the constructor. For example:
+</para>
+
+<para>
+
+<programlisting>
+data Baz = forall a. Eq a => Baz1 a a
+ | forall b. Show b => Baz2 b (b -> b)
+</programlisting>
+
+</para>
+
+<para>
+The two constructors have the types you'd expect:
+</para>
+
+<para>
+
+<programlisting>
+Baz1 :: forall a. Eq a => a -> a -> Baz
+Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
+</programlisting>
+
+</para>
+
+<para>
+But when pattern matching on <function>Baz1</function> the matched values can be compared
+for equality, and when pattern matching on <function>Baz2</function> the first matched
+value can be converted to a string (as well as applying the function to it).
+So this program is legal:
+</para>
+
+<para>
+
+<programlisting>
+ f :: Baz -> String
+ f (Baz1 p q) | p == q = "Yes"
+ | otherwise = "No"
+ f (Baz2 v fn) = show (fn v)
+</programlisting>
+
+</para>
+
+<para>
+Operationally, in a dictionary-passing implementation, the
+constructors <function>Baz1</function> and <function>Baz2</function> must store the
+dictionaries for <literal>Eq</literal> and <literal>Show</literal> respectively, and
+extract it on pattern matching.
+</para>
+
+</sect3>
+
+<sect3 id="existential-records">
+<title>Record Constructors</title>
+
+<para>
+GHC allows existentials to be used with records syntax as well. For example:
+
+<programlisting>
+data Counter a = forall self. NewCounter
+ { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+</programlisting>
+Here <literal>tag</literal> is a public field, with a well-typed selector
+function <literal>tag :: Counter a -> a</literal>. The <literal>self</literal>
+type is hidden from the outside; any attempt to apply <literal>_this</literal>,
+<literal>_inc</literal> or <literal>_display</literal> as functions will raise a
+compile-time error. In other words, <emphasis>GHC defines a record selector function
+only for fields whose type does not mention the existentially-quantified variables</emphasis>.
+(This example used an underscore in the fields for which record selectors
+will not be defined, but that is only programming style; GHC ignores them.)
+</para>
+
+<para>
+To make use of these hidden fields, we need to create some helper functions:
+
+<programlisting>
+inc :: Counter a -> Counter a
+inc (NewCounter x i d t) = NewCounter
+ { _this = i x, _inc = i, _display = d, tag = t }
+
+display :: Counter a -> IO ()
+display NewCounter{ _this = x, _display = d } = d x
+</programlisting>
+
+Now we can define counters with different underlying implementations:
+
+<programlisting>
+counterA :: Counter String
+counterA = NewCounter
+ { _this = 0, _inc = (1+), _display = print, tag = "A" }
+
+counterB :: Counter String
+counterB = NewCounter
+ { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
+
+main = do
+ display (inc counterA) -- prints "1"
+ display (inc (inc counterB)) -- prints "##"
+</programlisting>
+
+Record update syntax is supported for existentials (and GADTs):
+<programlisting>
+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>
+
+
+<sect3>
+<title>Restrictions</title>
+
+<para>
+There are several restrictions on the ways in which existentially-quantified
+constructors can be use.
+</para>
+
+<para>
+
+<itemizedlist>
+<listitem>
+
+<para>
+ When pattern matching, each pattern match introduces a new,
+distinct, type for each existential type variable. These types cannot
+be unified with any other type, nor can they escape from the scope of
+the pattern match. For example, these fragments are incorrect:
+
+
+<programlisting>
+f1 (MkFoo a f) = a
+</programlisting>
+
+
+Here, the type bound by <function>MkFoo</function> "escapes", because <literal>a</literal>
+is the result of <function>f1</function>. One way to see why this is wrong is to
+ask what type <function>f1</function> has:
+
+
+<programlisting>
+ f1 :: Foo -> a -- Weird!
+</programlisting>
+
+
+What is this "<literal>a</literal>" in the result type? Clearly we don't mean
+this:
+
+
+<programlisting>
+ f1 :: forall a. Foo -> a -- Wrong!
+</programlisting>
+
+
+The original program is just plain wrong. Here's another sort of error
+
+
+<programlisting>
+ f2 (Baz1 a b) (Baz1 p q) = a==q
+</programlisting>
+
+
+It's ok to say <literal>a==b</literal> or <literal>p==q</literal>, but
+<literal>a==q</literal> is wrong because it equates the two distinct types arising
+from the two <function>Baz1</function> constructors.
+
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+You can't pattern-match on an existentially quantified
+constructor in a <literal>let</literal> or <literal>where</literal> group of
+bindings. So this is illegal:
+
+
+<programlisting>
+ f3 x = a==b where { Baz1 a b = x }
+</programlisting>
+
+Instead, use a <literal>case</literal> expression:
+
+<programlisting>
+ f3 x = case x of Baz1 a b -> a==b
+</programlisting>
+
+In general, you can only pattern-match
+on an existentially-quantified constructor in a <literal>case</literal> expression or
+in the patterns of a function definition.
+
+The reason for this restriction is really an implementation one.
+Type-checking binding groups is already a nightmare without
+existentials complicating the picture. Also an existential pattern
+binding at the top level of a module doesn't make sense, because it's
+not clear how to prevent the existentially-quantified type "escaping".
+So for now, there's a simple-to-state restriction. We'll see how
+annoying it is.
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+You can't use existential quantification for <literal>newtype</literal>
+declarations. So this is illegal:
+
+
+<programlisting>
+ newtype T = forall a. Ord a => MkT a
+</programlisting>
+
+
+Reason: a value of type <literal>T</literal> must be represented as a
+pair of a dictionary for <literal>Ord t</literal> and a value of type
+<literal>t</literal>. That contradicts the idea that
+<literal>newtype</literal> should have no concrete representation.
+You can get just the same efficiency and effect by using
+<literal>data</literal> instead of <literal>newtype</literal>. If
+there is no overloading involved, then there is more of a case for
+allowing an existentially-quantified <literal>newtype</literal>,
+because the <literal>data</literal> version does carry an
+implementation cost, but single-field existentially quantified
+constructors aren't much use. So the simple restriction (no
+existential stuff on <literal>newtype</literal>) stands, unless there
+are convincing reasons to change it.
+
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ You can't use <literal>deriving</literal> to define instances of a
+data type with existentially quantified data constructors.
+
+Reason: in most cases it would not make sense. For example:;
+
+<programlisting>
+data T = forall a. MkT [a] deriving( Eq )
+</programlisting>
+
+To derive <literal>Eq</literal> in the standard way we would need to have equality
+between the single component of two <function>MkT</function> constructors:
+
+<programlisting>
+instance Eq T where
+ (MkT a) == (MkT b) = ???
+</programlisting>
+
+But <varname>a</varname> and <varname>b</varname> have distinct types, and so can't be compared.
+It's just about possible to imagine examples in which the derived instance
+would make sense, but it seems altogether simpler simply to prohibit such
+declarations. Define your own instances!
+</para>
+</listitem>
+
+</itemizedlist>
+
+</para>
+
+</sect3>
+</sect2>
+
+<!-- ====================== Generalised algebraic data types ======================= -->
+
+<sect2 id="gadt-style">
+<title>Declaring data types with explicit constructor signatures</title>
+
+<para>GHC allows you to declare an algebraic data type by
+giving the type signatures of constructors explicitly. For example:
+<programlisting>
+ data Maybe a where
+ Nothing :: Maybe a
+ Just :: a -> Maybe a
+</programlisting>
+The form is called a "GADT-style declaration"
+because Generalised Algebraic Data Types, described in <xref linkend="gadt"/>,
+can only be declared using this form.</para>
+<para>Notice that GADT-style syntax generalises existential types (<xref linkend="existential-quantification"/>).
+For example, these two declarations are equivalent:
+<programlisting>
+ data Foo = forall a. MkFoo a (a -> Bool)
+ data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
+</programlisting>
+</para>
+<para>Any data type that can be declared in standard Haskell-98 syntax
+can also be declared using GADT-style syntax.
+The choice is largely stylistic, but GADT-style declarations differ in one important respect:
+they treat class constraints on the data constructors differently.
+Specifically, if the constructor is given a type-class context, that
+context is made available by pattern matching. For example:
+<programlisting>
+ data Set a where
+ MkSet :: Eq a => [a] -> Set a
+
+ makeSet :: Eq a => [a] -> Set a
+ makeSet xs = MkSet (nub xs)
+
+ insert :: a -> Set a -> Set a
+ insert a (MkSet as) | a `elem` as = MkSet as
+ | otherwise = MkSet (a:as)
+</programlisting>
+A use of <literal>MkSet</literal> as a constructor (e.g. in the definition of <literal>makeSet</literal>)
+gives rise to a <literal>(Eq a)</literal>
+constraint, as you would expect. The new feature is that pattern-matching on <literal>MkSet</literal>
+(as in the definition of <literal>insert</literal>) makes <emphasis>available</emphasis> an <literal>(Eq a)</literal>
+context. In implementation terms, the <literal>MkSet</literal> constructor has a hidden field that stores
+the <literal>(Eq a)</literal> dictionary that is passed to <literal>MkSet</literal>; so
+when pattern-matching that dictionary becomes available for the right-hand side of the match.
+In the example, the equality dictionary is used to satisfy the equality constraint
+generated by the call to <literal>elem</literal>, so that the type of
+<literal>insert</literal> itself has no <literal>Eq</literal> constraint.
+</para>
+<para>
+For example, one possible application is to reify dictionaries:
+<programlisting>
+ data NumInst a where
+ MkNumInst :: Num a => NumInst a
+
+ intInst :: NumInst Int
+ intInst = MkNumInst
+
+ plus :: NumInst a -> a -> a -> a
+ plus MkNumInst p q = p + q
+</programlisting>
+Here, a value of type <literal>NumInst a</literal> is equivalent
+to an explicit <literal>(Num a)</literal> dictionary.
+</para>
+<para>
+All this applies to constructors declared using the syntax of <xref linkend="existential-with-context"/>.
+For example, the <literal>NumInst</literal> data type above could equivalently be declared
+like this:
+<programlisting>
+ data NumInst a
+ = Num a => MkNumInst (NumInst a)
+</programlisting>
+Notice that, unlike the situation when declaring an existential, there is
+no <literal>forall</literal>, because the <literal>Num</literal> constrains the
+data type's universally quantified type variable <literal>a</literal>.
+A constructor may have both universal and existential type variables: for example,
+the following two declarations are equivalent:
+<programlisting>
+ data T1 a
+ = forall b. (Num a, Eq b) => MkT1 a b
+ data T2 a where
+ MkT2 :: (Num a, Eq b) => a -> b -> T2 a
+</programlisting>
+</para>
+<para>All this behaviour contrasts with Haskell 98's peculiar treatment of
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
+In Haskell 98 the definition
+<programlisting>
+ data Eq a => Set' a = MkSet' [a]
+</programlisting>
+gives <literal>MkSet'</literal> the same type as <literal>MkSet</literal> above. But instead of
+<emphasis>making available</emphasis> an <literal>(Eq a)</literal> constraint, pattern-matching
+on <literal>MkSet'</literal> <emphasis>requires</emphasis> an <literal>(Eq a)</literal> constraint!
+GHC faithfully implements this behaviour, odd though it is. But for GADT-style declarations,
+GHC's behaviour is much more useful, as well as much more intuitive.
+</para>
+
+<para>
+The rest of this section gives further details about GADT-style data
+type declarations.
+
+<itemizedlist>
+<listitem><para>
+The result type of each data constructor must begin with the type constructor being defined.
+If the result type of all constructors
+has the form <literal>T a1 ... an</literal>, where <literal>a1 ... an</literal>
+are distinct type variables, then the data type is <emphasis>ordinary</emphasis>;
+otherwise is a <emphasis>generalised</emphasis> data type (<xref linkend="gadt"/>).
+</para></listitem>
+
+<listitem><para>
+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.
+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 -> 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>
+Unlike a Haskell-98-style
+data type declaration, the type variable(s) in the "<literal>data Set a where</literal>" header
+have no scope. Indeed, one can write a kind signature instead:
+<programlisting>
+ data Set :: * -> * where ...
+</programlisting>
+or even a mixture of the two:
+<programlisting>
+ 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 Bar a (b :: * -> *) where ...
+</programlisting>
+</para></listitem>
+
+
+<listitem><para>
+You can use strictness annotations, in the obvious places
+in the constructor type:
+<programlisting>
+ data Term a where
+ Lit :: !Int -> Term Int
+ If :: Term Bool -> !(Term a) -> !(Term a) -> Term a
+ Pair :: Term a -> Term b -> Term (a,b)
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can use a <literal>deriving</literal> clause on a GADT-style data type
+declaration. For example, these two declarations are equivalent
+<programlisting>
+ data Maybe1 a where {
+ Nothing1 :: Maybe1 a ;
+ Just1 :: a -> Maybe1 a
+ } deriving( Eq, Ord )
+
+ data Maybe2 a = Nothing2 | Just2 a
+ deriving( Eq, Ord )
+</programlisting>
+</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 :: 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>