rank 2-polymorphism and type checking

[Martin Odersky]

 > PS to my earlier message.  I am not at all certain that 
 > the Odersky/Laufer thing would in fact solve Janis's problem.
 > You want not only a rank-3 type, but also higher-order unification,
 > since you want to instantiate 't' to
 > 	\c. forall d . (c->d) -> d -> d 

Simon,

You are correct to have doubts. Indeed our system would not handle
this case, as type variables can only be instantiated to monomorophic
types, not to type schemes. The closest you can get to it is to wrap
the instance type in a type constructor. I.e. `t' could be
instantiated to

	T (\c. forall d . (c->d) -> d -> d)

where T was declared

	newtype T = T (\c. forall d . (c->d) -> d -> d)

But I guess that does not solve Janis's problem.

Cheers

 -- Martin