That's either backwards or just wrong. Perhaps you're confusing this with the syntax for existentials in data-declarations? I'm really not sure. 'forall x. A x

That's either backwards or just wrong. Perhaps you're confusing this with the syntax for existentials in data-declarations? I'm really not sure. 'forall x. A x. x' is a type of polymorphic values. Given such a value, I can instantiate the type-variable to any instance of the type class A. For instance, given x :: Num a => a I can write y :: Float y = x z :: Integer z = x Now if 'class A x => B x', then B is a subclass of A. In that case, in the type 'forall x. B x => x', the type variable x is more restricted. For instance, if I substitute "Integral" for "Num" in the type declaration for x, my code breaks. How's that for LSP? x :: forall a. Integral a => a Now I can no longer instantiate the a to Float: y :: Float y = x So I can do stuff with 'forall a. Num a' which I cannot do with 'forall a. Integral a', even though Integral is a subclass of Num. More generally, you cannot coerce a value of type 'forall x. B x => x' to one of type 'forall x. A x => x', because that would allow the type variable to range outside B. Consider: x :: forall x. Real x x = 0.5 coerce :: (forall x. Real x) -> (forall x. Num x) n :: forall x. Num x n = coerce x m :: Integer m = n This is type-correct, but semantically invalid, since the m has lost precision from x. If you want to talk about contravariance, you can note that when you add a type-class constraint of the form A x => x, you've basically got an implication, and the "A x" is in contravariant position. That's why your example is, if anything, the wrong way around. What you can do with existential types in Haskell is kind of like subtyping. At least, it's kind of like what you do in the C++ example with abstract types. But that's because abstract types are kind of like existential types. Full class hierarchies can then be mocked with Haskell type classes, existential quantifiers and explicit coercion functions, but that's because subclassing is kind of like containment which is kind of like implication which is kind of like the type of a coercion function. But by this stage, we've got a long way off from saying that type-class hierarchies in Haskell are subtype hierarchies, as you originally suggested. They're certainly not in Haskell 98, and with existential types, they don't give you the implicit upcasting that comes from values having multiple types. Even with existential types, all values have exactly one type, and this is crucial to remember when trying to reason about Haskell's type system. In other words, forget about subtypes!