GHC now allows you to write explicitly quantified types. GHC's syntax for this now agrees with Hugs's, namely:

forall a b. (Ord a, Eq b) => a -> b -> a |

The context is, of course, optional. You can't use `forall` as
a type variable any more!

Haskell type signatures are implicitly quantified. The `forall`
allows us to say exactly what this means. For example:

g :: b -> b |

means this:

g :: forall b. (b -> b) |

The two are treated identically.

In a `data` or `newtype` declaration one can quantify
the types of the constructor arguments. Here are several examples:

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]) |

The constructors now have so-called *rank 2* polymorphic
types, in which there is a for-all in the argument types.:

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 |

Notice that you don't need to use a `forall` if there's an
explicit context. For example in the first argument of the
constructor `MkSwizzle`, an implicit "`forall a.`" is
prefixed to the argument type. The implicit `forall`
quantifies all type variables that are not already in scope, and are
mentioned in the type quantified over.

As for type signatures, implicit quantification happens for non-overloaded types too. So if you write this:

data T a = MkT (Either a b) (b -> b) |

data T a = MkT (forall b. Either a b) (forall b. b -> b) |

You construct values of types `T1, MonadT, Swizzle` by applying
the constructor to suitable values, just as usual. For example,

(T1 (\xy->x) 3) :: T Int (MkSwizzle sort) :: Swizzle (MkSwizzle reverse) :: Swizzle (let r x = Just x b m k = case m of Just y -> k y Nothing -> Nothing in MkMonad r b) :: MonadT Maybe |

The type of the argument can, as usual, be more general than the type
required, as `(MkSwizzle reverse)` shows. (`reverse`
does not need the `Ord` constraint.)

When you use pattern matching, the bound variables may now have polymorphic types. For example:

f :: T a -> a -> (a, Char) f (T1 f k) x = (f k x, f '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) |

In the function `h` we use the record selectors `return`
and `bind` to extract the polymorphic bind and return functions
from the `MonadT` data structure, rather than using pattern
matching.

You cannot pattern-match against an argument that is polymorphic. For example:

newtype TIM s a = TIM (ST s (Maybe a)) runTIM :: (forall s. TIM s a) -> Maybe a runTIM (TIM m) = runST m |

Here the pattern-match fails, because you can't pattern-match against
an argument of type `(forall s. TIM s a)`. Instead you
must bind the variable and pattern match in the right hand side:

runTIM :: (forall s. TIM s a) -> Maybe a runTIM tm = case tm of { TIM m -> runST m } |

There is really only one way in which data structures with polymorphic components might surprise you: you must not partially apply them. For example, this is illegal:

map MkSwizzle [sort, reverse] |

The restriction is this: *every subexpression of the program must
have a type that has no for-alls, except that in a function
application (f e1…en) the partial applications are not subject to
this rule*. The restriction makes type inference feasible.

In the illegal example, the sub-expression `MkSwizzle` has the
polymorphic type `(Ord b => [b] -> [b]) -> Swizzle` and is not
a sub-expression of an enclosing application. On the other hand, this
expression is OK:

map (T1 (\a b -> a)) [1,2,3] |

even though it involves a partial application of `T1`, because
the sub-expression `T1 (\a b -> a)` has type `Int -> T
Int`.

Once you have data constructors with universally-quantified fields, or
constants such as `runST` that have rank-2 types, it isn't long
before you discover that you need more! Consider:

mkTs f x y = [T1 f x, T1 f y] |

`mkTs` is a fuction that constructs some values of type
`T`, using some pieces passed to it. The trouble is that since
`f` is a function argument, Haskell assumes that it is
monomorphic, so we'll get a type error when applying `T1` to
it. This is a rather silly example, but the problem really bites in
practice. Lots of people trip over the fact that you can't make
"wrappers functions" for `runST` for exactly the same reason.
In short, it is impossible to build abstractions around functions with
rank-2 types.

The solution is fairly clear. We provide the ability to give a rank-2
type signature for *ordinary* functions (not only data
constructors), thus:

mkTs :: (forall b. b -> b -> b) -> a -> [T a] mkTs f x y = [T1 f x, T1 f y] |

This type signature tells the compiler to attribute `f` with
the polymorphic type `(forall b. b -> b -> b)` when type
checking the body of `mkTs`, so now the application of
`T1` is fine.

There are two restrictions:

You can only define a rank 2 type, specified by the following grammar:

Informally, the universal quantification must all be right at the beginning, or at the top level of a function argument.rank2type ::= [forall tyvars .] [context =>] funty funty ::= ([forall tyvars .] [context =>] ty) -> funty | ty ty ::= ...current Haskell monotype syntax...

There is a restriction on the definition of a function whose type signature is a rank-2 type: the polymorphic arguments must be matched on the left hand side of the "

`=`" sign. You can't define`mkTs`like this:

The same partial-application rule applies to ordinary functions with rank-2 types as applied to data constructors.mkTs :: (forall b. b -> b -> b) -> a -> [T a] mkTs = \ f x y -> [T1 f x, T1 f y]