-<title>Polymorphism</title>
-
-<para>
-
-<itemizedlist>
-<listitem>
-
-<para>
- Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together. There is
-no scoping associated with the names of the type variables in a separate type signature.
-
-
-<programlisting>
- f :: [a] -> [a]
- f (xs::[b]) = reverse xs
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- The function must be polymorphic in the type variables
-bound by all its equations. Operationally, the type variables bound
-by one equation must not:
-
-
-<itemizedlist>
-<listitem>
-
-<para>
- Be unified with a type (such as <literal>Int</literal>, or <literal>[a]</literal>).
-</para>
-</listitem>
-<listitem>
-
-<para>
- Be unified with a type variable free in the environment.
-</para>
-</listitem>
-<listitem>
-
-<para>
- Be unified with each other. (They may unify with the type variables
-bound by another equation for the same function, of course.)
-</para>
-</listitem>
-
-</itemizedlist>
-
-
-For example, the following all fail to type check:
-
-
-<programlisting>
- f (x::a) (y::b) = [x,y] -- a unifies with b
-
- g (x::a) = x + 1::Int -- a unifies with Int
-
- h x = let k (y::a) = [x,y] -- a is free in the
- in k x -- environment
-
- k (x::a) True = ... -- a unifies with Int
- k (x::Int) False = ...
-
- w :: [b] -> [b]
- w (x::a) = x -- a unifies with [b]
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- The pattern-bound type variable may, however, be constrained
-by the context of the principal type, thus:
-
-
-<programlisting>
- f (x::a) (y::a) = x+y*2
-</programlisting>
-
-
-gets the inferred type: <literal>forall a. Num a => a -> a -> a</literal>.
-</para>
-</listitem>
-
-</itemizedlist>
-
-</para>
-
-</sect2>
-
-<sect2>