+NilSet :: Set a
+ConsSet :: Eq a => a -> Set a -> Set a
+</programlisting>
+
+<para>In GHC this feature is an extension called
+<literal>DatatypeContexts</literal>, and on by default.</para>
+</sect2>
+
+<sect2 id="infix-tycons">
+<title>Infix type constructors, classes, and type variables</title>
+
+<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