Musing on Zhanyong's problem some more, a solution occurs to me. Curiously, it's exactly the solution required for another useful extension to type classes. Here is is, so people can shoot holes in it. | In more detail, here's what happens. First we typecheck the RHS of | f, deducing the types | | x :: a where a is fresh | y :: k a where k is fresh | y >> return x :: k a | op (y >> return x) :: Bool with constraint C (k a) | \x -> op (y >> return x) :: a -> Bool with constraint C (k a) | | Now we try to generalise over a. We need to discharge the contraint | C (k a). Later we will find that y::[Int], so k=[], but we | don't know that yet. So we can't solve the constraint. One bad solution I thought of was to give f the type f :: forall a. C (k a) => a -> Bool This is bad because it's not the type signature the programmer specified. (It's also bad operationally because we'll pass a dictionary at runtime, which isn't necessary.) The good solution is to say this: \x -> op (y >> return x) :: a -> Bool with constraint C (k a) (just as before) /\a \x -> op (y>>return x) :: forall a. a -> Bool with constraint (forall a. C (k a)) This requires us to permit constraints with for-alls in them. As luck would have it, Ralf Hinze and I propose just such a thing in our paper "Derivable Type Classes" (Section 7) http://research.microsoft.com/~simonpj/#derive The motivation there is this: how can you write an equality instance for data T k a = MkT (k (T k a)) We can try: instance ... => Eq (T k a) where (MkT a) == (MkT b) = a == b But what is the "..."? We need that "k" is an equality type constructor. The right context is instance (forall a. Eq a => Eq (k a)) => Eq (T k a) where ...as before... Aha! A constraint with a for-all. There are some more details in the paper. So perhaps there's a reason for adding this extension in the implementation (to solve Zhanyong's problem) even for a Haskell 98 compiler. Simon