+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>When the <literal>GADTSyntax</literal> extension is enabled,
+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>