Hello, and thanks for the various answers! Martin Odersky writes:
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.
I'm not sure whether it would. To make things more complicated, the application I had in mind would not only require a rank-3 type and quantification over a type constructor, but also polymorphic recursion. Hmm, I wanted to use the free theorem of g's type, but rethinking I wonder what this actually *means* in the presence of quantification over type constructors. The whole story got so complicated, because I wanted to use a nested type of the form data D a = ... | forall b . F (b -> a) (D b) If I settle for the less general but still useful data D a = ... | F (a -> a) (D a) then I can do without any extensions :-) Regards, Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de