Rank-2 polymorphism & type inference

[Simon Peyton-Jones]

Musing on Zhanyong's problem some more, a solution occurs to me.
Curiously, it's exactly the solution required for another useful
extension to type classes.  Here is is, so people can shoot holes in it.

| In more detail, here's what happens.  First we typecheck the RHS of
| f, deducing the types
| 
| 	x :: a					where a is fresh
| 	y :: k a					where k is fresh
| 	y >> return x :: k a
| 	op (y >> return x) :: Bool		with constraint C (k a)
| 	\x -> op (y >> return x) :: a -> Bool	with constraint C (k a)
| 
| Now we try to generalise over a.  We need to discharge the contraint
| C (k a).  Later we will find that y::[Int], so k=[], but we 
| don't know that yet.  So we can't solve the constraint.

One bad solution I thought of was to give f the type
	
	f :: forall a. C (k a) => a -> Bool

This is bad because it's not the type signature the programmer
specified.  (It's also bad operationally because we'll pass a
dictionary at runtime, which isn't necessary.)

The good solution is to say this:

	\x -> op (y >> return x) :: a -> Bool	
					with constraint C (k a)
		(just as before)

	/\a \x -> op (y>>return x) :: forall a. a -> Bool
					with constraint (forall a. C (k a))

This requires us to permit constraints with for-alls in them.
As luck would have it, Ralf Hinze and I propose just such a thing in
our paper "Derivable Type Classes" (Section 7)
http://research.microsoft.com/~simonpj/#derive

The motivation there is this: how can you write an equality instance for

	data T k a = MkT (k (T k a))

We can try:

	instance ... => Eq (T k a) where
	  (MkT a) == (MkT b) = a == b

But what is the "..."?  We need that "k" is an equality type
constructor.  The right context is

	instance (forall a. Eq a => Eq (k a)) => Eq (T k a) where
	  ...as before...

Aha!  A constraint with a for-all.

There are some more details in the paper.

So perhaps there's a reason for adding this extension in the implementation
(to solve Zhanyong's problem) even for a Haskell 98 compiler.

Simon