rank-2 vs. arbitrary rank types

[Ross Paterson]

On Fri, Feb 02, 2007 at 08:35:01AM +0000, Simon Peyton-Jones wrote:
> * Rank-N is really no harder to implement than rank-2.  The "Practical
> type inference.." paper gives every line of code required.  The design
> is certainly much cleaner and less ad-hoc than GHC's old rank-2 design,
> which I dumped with considerable relief.
>
> * I think it'd be a pity to have an arbitrary rank-2 restriction.
> Rank-2 allows you to abstract over a polymorphic function.  Well,
> it's not too long before you start wanting to abstract over a rank-2
> function, and there you are.

So is the proposed candidate the system described in the "Practical Type
Inference" paper, with contravariant subsumption, bi-directional inference
judgements (rather than boxes), no impredicativity, etc?  As I recall the
treatment of application expressions there (infer type of the function,
then check the argument) was considered a bit restrictive.  (It forbids
runST $ foo, for example.)

Is there a plan for GHC to have a mode that implements the proposed system?