+<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/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.