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?