+<sect2 id="infix-tycons">
+<title>Infix type constructors</title>
+
+<para>
+GHC allows type constructors to be operators, and to be written infix, very much
+like expressions. More specifically:
+<itemizedlist>
+<listitem><para>
+ A type constructor 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>
+ Types can be written infix. For example <literal>Int :*: Bool</literal>.
+ </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 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>
+<listitem><para>
+ Data type and type-synonym declarations can be written infix. E.g.
+<screen>
+ data a :*: b = Foo a b
+ type a :+: b = Either a b
+</screen>
+ </para></listitem>
+<listitem><para>
+ The only thing that differs between operators in types and operators in expressions is that
+ ordinary non-constructor operators, such as <literal>+</literal> and <literal>*</literal>
+ are not allowed in types. Reason: the uniform thing to do would be to make them type
+ variables, but that's not very useful. A less uniform but more useful thing would be to
+ allow them to be type <emphasis>constructors</emphasis>. But that gives trouble in export
+ lists. So for now we just exclude them.
+ </para></listitem>
+
+</itemizedlist>
+</para>
+</sect2>
+
+<sect2 id="sec-kinding">
+<title>Explicitly-kinded quantification</title>
+
+<para>
+Haskell infers the kind of each type variable. Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation,
+just as it is nice to give a type signature for a function. On some occasions,
+it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+<Screen>
+ data Set cxt a = Set [a]
+ | Unused (cxt a -> ())
+</Screen>
+The only use for the <literal>Unused</literal> constructor was to force the correct
+kind for the type variable <literal>cxt</literal>.
+</para>
+<para>
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound. Namely:
+<itemizedlist>
+<listitem><para><literal>data</literal> declarations:
+<Screen>
+ data Set (cxt :: * -> *) a = Set [a]
+</Screen></para></listitem>
+<listitem><para><literal>type</literal> declarations:
+<Screen>
+ type T (f :: * -> *) = f Int
+</Screen></para></listitem>
+<listitem><para><literal>class</literal> declarations:
+<Screen>
+ class (Eq a) => C (f :: * -> *) a where ...
+</Screen></para></listitem>
+<listitem><para><literal>forall</literal>'s in type signatures:
+<Screen>
+ f :: forall (cxt :: * -> *). Set cxt Int
+</Screen></para></listitem>
+</itemizedlist>
+</para>
+
+<para>
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write <literal>(f::*->*)</literal> you
+will get a parse error, because "<literal>::*->*</literal>" is a
+single lexeme in Haskell.
+</para>
+
+<para>
+As part of the same extension, you can put kind annotations in types
+as well. Thus:
+<Screen>
+ f :: (Int :: *) -> Int
+ g :: forall a. a -> (a :: *)
+</Screen>
+The syntax is
+<Screen>
+ atype ::= '(' ctype '::' kind ')
+</Screen>
+The parentheses are required.
+</para>
+</sect2>
+
+