Suppose you want to define a combinator like this: combinator :: (forall y. Class y => y -> y) -> (forall x. Class x => x -> x) This is a function combinator which turns a polymorphic function into another polymorphic function. As you can see, there is Class constraint. So in fact we would like to define the combinator by class overloading on the x in the result type. So how do we get our hands on the x while it is explicitly quantified by forall. Well, we try with implicit quantification: class Class x where combinator' :: (forall y. Class y => y -> y) -> x -> x So far so, good: We still need to define combinator in terms of combinator'. What is the trick to do this? Sounds like a homework question? Well, I know how to do it for first-class polymorphism. So let's restart the example. We define a function type to capture the kind of functions from above: data Bar = Foo (forall x. Class x => x -> x) Hence, the rank-2 type of combinator looks a bit different: combinator :: Bar -> Bar The class looks as follows: class Class x where combinator' :: Bar -> x -> x And here is how to define combinator in terms of combinator'. combinator f = Foo (combinator' f) This works both with GHC and hugs. In the pure rank-2 setting above, one would like to define combinator accordingly: combinator f = combinator' f But GHC 5.02.2 tells me: rank2.hs:11: Could not deduce (Class x) from the context () Probable fix: Add (Class x) to the type signature(s) for combinator arising from use of `combinator'' at rank2.hs:11 In the definition of `combinator': combinator' f This is not a bug, I guess although the probable fix proposal sends you in the wrong direction I claim. I tried a few other tricks but I can't get it done although my first-class polymorphic experience makes me think that it should be possible. Anyway, can this problem be solved? Any hint appreciated. Ralf -- Dr.-Ing. Ralf Laemmel CWI & VU, Amsterdam, The Netherlands http://www.cwi.nl/~ralf/ http://www.cs.vu.nl/~ralf/