-<listitem>
-
-<para>
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern. We describe this set as
-the <emphasis>type variables bound by the pattern</emphasis>.
-For example:
-<programlisting>
- f (x::a) = let g (y::(a,b)) = fst y
- in
- g (x,True)
-</programlisting>
-The pattern <literal>(x::a)</literal> brings the type variable
-<literal>a</literal> into scope, as well as the term
-variable <literal>x</literal>. The pattern <literal>(y::(a,b))</literal>
-contains an occurrence of the already-in-scope type variable <literal>a</literal>,
-and brings into scope the type variable <literal>b</literal>.
-</para>
-</listitem>
-
-<listitem>
-<para>
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern. For example:
-<programlisting>
- let
- f (x::a) = <...rhs of f...>
- (p::b, q::b) = (1,2)
- in <...body of let...>
-</programlisting>
-Here, the type variable <literal>a</literal> scopes over the right hand side of <literal>f</literal>,
-just like <literal>x</literal> does; while the type variable <literal>b</literal> scopes over the
-body of the <literal>let</literal>, and all the other definitions in the <literal>let</literal>,
-just like <literal>p</literal> and <literal>q</literal> do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the <literal>let</literal> group.
-</para>
-</listitem>
-
-
-<listitem>
-<para>
-The type variables bound by the pattern may be
-mentioned in ordinary type signatures or pattern
-type signatures anywhere within their scope.
-
-</para>
-</listitem>
-
-<listitem>
-<para>
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is <emphasis>not</emphasis> universally quantified.
-
-</para>
-</listitem>
-
-<listitem>
-
-<para>
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-<programlisting>
- f :: a -> a
- f x = x::a
-</programlisting>
-
-It's illegal because <varname>a</varname> is not in scope in the body of <function>f</function>,
-so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
-and that is an incorrect typing.
-
+<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
+a <emphasis>type</emphasis>. (This is a change from GHC's earlier
+design.)</para></listitem>
+<listitem><para>Furthermore, distinct lexical type variables stand for distinct
+type variables. This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
+checker, and no inference is involved.</para></listitem>
+<listitem><para>Lexical type variables may be alpha-renamed freely, without
+changing the program.</para></listitem>
+</itemizedlist>