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:[EMAIL PROTECTED] _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
