+<para>
+Linear implicit parameters are just like ordinary implicit parameters,
+except that they are "linear"; that is, they cannot be copied, and
+must be explicitly "split" instead. Linear implicit parameters are
+written '<literal>%x</literal>' instead of '<literal>?x</literal>'.
+(The '/' in the '%' suggests the split!)
+</para>
+<para>
+For example:
+<programlisting>
+ import GHC.Exts( Splittable )
+
+ data NameSupply = ...
+
+ splitNS :: NameSupply -> (NameSupply, NameSupply)
+ newName :: NameSupply -> Name
+
+ instance Splittable NameSupply where
+ split = splitNS
+
+
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+ ...more equations for f...
+</programlisting>
+Notice that the implicit parameter %ns is consumed
+<itemizedlist>
+<listitem> <para> once by the call to <literal>newName</literal> </para> </listitem>
+<listitem> <para> once by the recursive call to <literal>f</literal> </para></listitem>
+</itemizedlist>
+</para>
+<para>
+So the translation done by the type checker makes
+the parameter explicit:
+<programlisting>
+ f :: NameSupply -> Env -> Expr -> Expr
+ f ns env (Lam x e) = Lam x' (f ns1 env e)
+ where
+ (ns1,ns2) = splitNS ns
+ x' = newName ns2
+ env = extend env x x'
+</programlisting>
+Notice the call to 'split' introduced by the type checker.
+How did it know to use 'splitNS'? Because what it really did
+was to introduce a call to the overloaded function 'split',
+defined by the class <literal>Splittable</literal>:
+<programlisting>
+ class Splittable a where
+ split :: a -> (a,a)
+</programlisting>
+The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
+split for name supplies. But we can simply write
+<programlisting>
+ g x = (x, %ns, %ns)
+</programlisting>
+and GHC will infer
+<programlisting>
+ g :: (Splittable a, %ns :: a) => b -> (b,a,a)
+</programlisting>
+The <literal>Splittable</literal> class is built into GHC. It's exported by module
+<literal>GHC.Exts</literal>.
+</para>
+<para>
+Other points:
+<itemizedlist>
+<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>'
+are entirely distinct implicit parameters: you
+ can use them together and they won't interfere with each other. </para>
+</listitem>
+
+<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
+
+<listitem> <para>You cannot have implicit parameters (whether linear or not)
+ in the context of a class or instance declaration. </para></listitem>
+</itemizedlist>
+</para>
+
+<sect3><title>Warnings</title>
+
+<para>
+The monomorphism restriction is even more important than usual.
+Consider the example above:
+<programlisting>
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+</programlisting>
+If we replaced the two occurrences of x' by (newName %ns), which is
+usually a harmless thing to do, we get:
+<programlisting>
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam (newName %ns) (f env e)
+ where
+ env' = extend env x (newName %ns)
+</programlisting>
+But now the name supply is consumed in <emphasis>three</emphasis> places
+(the two calls to newName,and the recursive call to f), so
+the result is utterly different. Urk! We don't even have
+the beta rule.
+</para>
+<para>
+Well, this is an experimental change. With implicit
+parameters we have already lost beta reduction anyway, and
+(as John Launchbury puts it) we can't sensibly reason about
+Haskell programs without knowing their typing.
+</para>
+
+</sect3>
+
+<sect3><title>Recursive functions</title>
+<para>Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
+<programlisting>
+ foo :: %x::T => Int -> [Int]
+ foo 0 = []
+ foo n = %x : foo (n-1)
+</programlisting>
+where T is some type in class Splittable.</para>
+<para>
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+</para><para>
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect. Here's the
+translated term, where the implicit param is made explicit:
+<programlisting>
+ foo x 0 = []
+ foo x n = let (x1,x2) = split x
+ in x1 : foo x2 (n-1)
+</programlisting>
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work. So the translation becomes
+<programlisting>
+ foo x = let
+ foom 0 = []
+ foom n = x : foom (n-1)
+ in
+ foom
+</programlisting>
+Result: 'x' is not split, and you get a list of identical T's. So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+</para><para>
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right. That is why they are an experimental feature.
+</para>
+</sect3>
+
+</sect2>
+
+================ END OF Linear Implicit Parameters commented out -->
+
+<sect2 id="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, with the flag <option>-XKindSignatures</option>.
+</para>
+<para>
+This flag enables kind signatures in the following places:
+<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>
+
+
+<sect2 id="universal-quantification">
+<title>Arbitrary-rank polymorphism
+</title>
+
+<para>
+Haskell type signatures are implicitly quantified. The new keyword <literal>forall</literal>
+allows us to say exactly what this means. For example:
+</para>
+<para>
+<programlisting>
+ g :: b -> b
+</programlisting>
+means this:
+<programlisting>
+ g :: forall b. (b -> b)
+</programlisting>
+The two are treated identically.
+</para>
+
+<para>
+However, GHC's type system supports <emphasis>arbitrary-rank</emphasis>
+explicit universal quantification in
+types.
+For example, all the following types are legal:
+<programlisting>
+ f1 :: forall a b. a -> b -> a
+ g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
+
+ f2 :: (forall a. a->a) -> Int -> Int
+ g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+
+ f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+
+ f4 :: Int -> (forall a. a -> a)
+</programlisting>
+Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
+can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
+The <literal>forall</literal> makes explicit the universal quantification that
+is implicitly added by Haskell.
+</para>
+<para>
+The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
+the <literal>forall</literal> is on the left of a function arrow. As <literal>g2</literal>
+shows, the polymorphic type on the left of the function arrow can be overloaded.
+</para>
+<para>
+The function <literal>f3</literal> has a rank-3 type;
+it has rank-2 types on the left of a function arrow.
+</para>
+<para>
+GHC has three flags to control higher-rank types:
+<itemizedlist>
+<listitem><para>
+ <option>-XPolymorphicComponents</option>: data constructors (only) can have polymorphic argument types.
+</para></listitem>
+<listitem><para>
+ <option>-XRank2Types</option>: any function (including data constructors) can have a rank-2 type.
+</para></listitem>
+<listitem><para>
+ <option>-XRankNTypes</option>: any function (including data constructors) can have an arbitrary-rank type.
+That is, you can nest <literal>forall</literal>s
+arbitrarily deep in function arrows.
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+<itemizedlist>
+<listitem> <para> On the left or right (see <literal>f4</literal>, for example)
+of a function arrow </para> </listitem>
+<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the <literal>f1,f2,f3,g1,g2</literal> above would be valid
+field type signatures.</para> </listitem>
+<listitem> <para> As the type of an implicit parameter </para> </listitem>
+<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables"/>) </para> </listitem>
+</itemizedlist>
+</para></listitem>
+</itemizedlist>
+Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
+a type variable any more!
+</para>
+
+
+<sect3 id="univ">
+<title>Examples
+</title>
+
+<para>
+In a <literal>data</literal> or <literal>newtype</literal> declaration one can quantify
+the types of the constructor arguments. Here are several examples:
+</para>
+
+<para>
+
+<programlisting>
+data T a = T1 (forall b. b -> b -> b) a
+
+data MonadT m = MkMonad { return :: forall a. a -> m a,
+ bind :: forall a b. m a -> (a -> m b) -> m b
+ }
+
+newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+</programlisting>
+
+</para>
+
+<para>
+The constructors have rank-2 types:
+</para>
+
+<para>
+
+<programlisting>
+T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
+MkMonad :: forall m. (forall a. a -> m a)
+ -> (forall a b. m a -> (a -> m b) -> m b)
+ -> MonadT m
+MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
+</programlisting>
+
+</para>
+
+<para>
+Notice that you don't need to use a <literal>forall</literal> if there's an
+explicit context. For example in the first argument of the
+constructor <function>MkSwizzle</function>, an implicit "<literal>forall a.</literal>" is
+prefixed to the argument type. The implicit <literal>forall</literal>
+quantifies all type variables that are not already in scope, and are
+mentioned in the type quantified over.
+</para>
+
+<para>
+As for type signatures, implicit quantification happens for non-overloaded
+types too. So if you write this:
+
+<programlisting>
+ data T a = MkT (Either a b) (b -> b)
+</programlisting>
+
+it's just as if you had written this:
+
+<programlisting>
+ data T a = MkT (forall b. Either a b) (forall b. b -> b)
+</programlisting>
+
+That is, since the type variable <literal>b</literal> isn't in scope, it's
+implicitly universally quantified. (Arguably, it would be better
+to <emphasis>require</emphasis> explicit quantification on constructor arguments
+where that is what is wanted. Feedback welcomed.)
+</para>
+
+<para>
+You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
+the constructor to suitable values, just as usual. For example,
+</para>
+
+<para>
+
+<programlisting>
+ a1 :: T Int
+ a1 = T1 (\xy->x) 3
+
+ a2, a3 :: Swizzle
+ a2 = MkSwizzle sort
+ a3 = MkSwizzle reverse
+
+ a4 :: MonadT Maybe
+ a4 = let r x = Just x
+ b m k = case m of
+ Just y -> k y
+ Nothing -> Nothing
+ in
+ MkMonad r b
+
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs f x y = [T1 f x, T1 f y]
+</programlisting>
+
+</para>
+
+<para>
+The type of the argument can, as usual, be more general than the type
+required, as <literal>(MkSwizzle reverse)</literal> shows. (<function>reverse</function>
+does not need the <literal>Ord</literal> constraint.)
+</para>
+
+<para>
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
+</para>
+
+<para>
+
+<programlisting>
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
+
+ g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+ g (MkSwizzle s) xs f = s (map f (s xs))
+
+ h :: MonadT m -> [m a] -> m [a]
+ h m [] = return m []
+ h m (x:xs) = bind m x $ \y ->
+ bind m (h m xs) $ \ys ->
+ return m (y:ys)
+</programlisting>
+
+</para>
+
+<para>
+In the function <function>h</function> we use the record selectors <literal>return</literal>
+and <literal>bind</literal> to extract the polymorphic bind and return functions
+from the <literal>MonadT</literal> data structure, rather than using pattern
+matching.
+</para>
+</sect3>
+
+<sect3>
+<title>Type inference</title>
+
+<para>
+In general, type inference for arbitrary-rank types is undecidable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
+</para>
+<para>
+<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it</emphasis>.
+</para>
+<para>
+What does it mean to "provide" an explicit type for x? You can do that by
+giving a type signature for x directly, using a pattern type signature
+(<xref linkend="scoped-type-variables"/>), thus:
+<programlisting>
+ \ f :: (forall a. a->a) -> (f True, f 'c')
+</programlisting>
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
+<programlisting>
+ (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
+</programlisting>
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f. Similarly, and more commonly,
+one can give a type signature for the function itself:
+<programlisting>
+ h :: (forall a. a->a) -> (Bool,Char)
+ h f = (f True, f 'c')
+</programlisting>
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument. Here is an example we saw earlier:
+<programlisting>
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
+</programlisting>
+Here we do not need to give a type signature to <literal>w</literal>, because
+it is an argument of constructor <literal>T1</literal> and that tells GHC all
+it needs to know.
+</para>
+
+</sect3>
+
+
+<sect3 id="implicit-quant">
+<title>Implicit quantification</title>
+
+<para>
+GHC performs implicit quantification as follows. <emphasis>At the top level (only) of
+user-written types, if and only if there is no explicit <literal>forall</literal>,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them.</emphasis> For example, the following pairs are
+equivalent:
+<programlisting>
+ f :: a -> a
+ f :: forall a. a -> a
+
+ g (x::a) = let
+ h :: a -> b -> b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a -> b -> b
+ h x y = y
+ in ...
+</programlisting>
+</para>
+<para>
+Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
+point. For example:
+<programlisting>
+ f :: (a -> a) -> Int
+ -- MEANS
+ f :: forall a. (a -> a) -> Int
+ -- NOT
+ f :: (forall a. a -> a) -> Int
+
+
+ g :: (Ord a => a -> a) -> Int
+ -- MEANS the illegal type
+ g :: forall a. (Ord a => a -> a) -> Int
+ -- NOT
+ g :: (forall a. Ord a => a -> a) -> Int
+</programlisting>
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple. If you want the latter type, you
+can write your for-alls explicitly. Indeed, doing so is strongly advised
+for rank-2 types.
+</para>
+</sect3>
+</sect2>
+
+
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>,
+enabled with <option>-XImpredicativeTypes</option>.
+This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types. For example:
+<programlisting>
+ f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
+</programlisting>
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
+</para>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy/">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.
+</para>
+</sect2>
+
+<sect2 id="scoped-type-variables">
+<title>Lexically scoped type variables
+</title>
+
+<para>
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
+<programlisting>
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
+</programlisting>
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope,
+because of the explicit <literal>forall</literal> (<xref linkend="decl-type-sigs"/>).
+The type variables bound by a <literal>forall</literal> scope over
+the entire definition of the accompanying value declaration.
+In this example, the type variable <literal>a</literal> scopes over the whole
+definition of <literal>f</literal>, including over
+the type signature for <varname>ys</varname>.
+In Haskell 98 it is not possible to declare
+a type for <varname>ys</varname>; a major benefit of scoped type variables is that
+it becomes possible to do so.
+</para>
+<para>Lexically-scoped type variables are enabled by
+<option>-XScopedTypeVariables</option>. This flag implies <option>-XRelaxedPolyRec</option>.
+</para>
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases. Read this section
+carefully!</para>
+
+<sect3>
+<title>Overview</title>
+
+<para>The design follows the following principles
+<itemizedlist>
+<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
+(including 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>
+</para>
+<para>
+A <emphasis>lexically scoped type variable</emphasis> can be bound by:
+<itemizedlist>
+<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
+<listitem><para>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
+</itemizedlist>
+</para>
+<para>
+In Haskell, a programmer-written type signature is implicitly quantified over
+its free type variables (<ulink
+url="http://www.haskell.org/onlinereport/decls.html#sect4.1.2">Section
+4.1.2</ulink>
+of the Haskell Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
+quantified. For example, if type variable <literal>a</literal> is in scope,
+then
+<programlisting>
+ (e :: a -> a) means (e :: a -> a)
+ (e :: b -> b) means (e :: forall b. b->b)
+ (e :: a -> b) means (e :: forall b. a->b)
+</programlisting>