| So, obviously, the next version of Haskell should have a type system | with subtyping, don't you agree? :-) It's always delightful to find that some awkward fumbling has been Done Properly by someone else earlier. My claim was that forall a. Show a => T could be implemented by passing a bottom dictionary for Show. I didn't say this, but the obvious thing to do is to fix 'a' to be some vacuous type Empty, and arrange that Empty is an instance of every class, with a bottom dictionary. And you're telling us that the subtyping folk worked this out yonks ago. Excellent! (Reference, for this particular point?) In a system with subtyping this would work even if T contained a free, as you say. But even in a system *without* subtyping, if 'a' is not free in T, we can safely remove the 'forall a' and fix a=Empty. (A calling context can only "see" the types in T, so this places no constraints on the calling context, which is why we don't need subtyping.) I think this is what your PPS suggested, yes? So in fact, all we need do is: for each class, find the variance of each of its parameters in an ambiguous type, zap any positive parameters to Empty That sounds pretty easy. We don't need Haskell 2 for that. I feel a little implementation coming on. Hmm. One question. Suppose I have forall a. C (a->Int) Int => T and C is positive in its first parameter. Can I zap 'a' to Empty? It looks as if it still occurs positively. What about data types? | PS In some previous version of Haskell (1.3?), the Prelude defined an | empty type called Void, but it has since been removed. Apparently, | people didn't see the potential of Void... Void was a type with one element. What we really want here is a type with no elements. It's also useful to be able to introduce such empty types for phantom-type purposes, so GHC now lets you say data T and get a type T with no values. Simon