Neither of the types you gave is inhabited, because the 'a' has kind * -> * .

I think what you've said about subtyping is muddled. If a type A is a subtype of B, then values of type A should be values of type B. Now let's take an example from the number class hierarchy. Consider

  1) forall a. Num a => a
  2) forall a. Integral a => a

According to what you have written, (2) should be a subtype of (1). That means that if I define

  n = 1 :: forall a. Integral a => a

then I should be able to "upcast" with:

  n :: forall a. Num a => a

However, this doesn't work, since the quantifier now ranges over types that were not in the range of the original quantifier. In the second type, I can instantiate the a to Float, while I cannot do so for the first type.

The only formal account of universal quantifiers in type theory, of which I am aware, extends the term language by introducing a capital lambda that ranges over types. So the polymorphic identity function is actually the term

  Λa. λx:a. x

which is a function that takes a type a followed by a value x:a and returns x.

This makes good sense of the way number classes work in Haskell. When you write

  n :: Num a => a
  n = 1

the actual machine representation of n is going to vary with the type of a.

EDIT: Another way of explaining the counterexample: any type in Applicative is also in Functor. But, on one informal interpretation of forall, the intersection of all applicatives is actually a proper superset of the intersection of all functors.

I wouldn't expect (Integral a, Num b) => a -> b, but I do expect the opposite. That seems to be exactly the definition of LSP.

And yeah, if you add System F type binders then you can do all of this explicitly, you just need to also manually pass around instance dictionaries. A morphism from one instance dictionary to another (which "forgets" "methods") provides your subtyping relation.

You have

  (Integral a, Num b) => a -> b

It's just the function fromIntegral. You don't have the opposite, if, by which, you mean

  (Num a, Integral b) => a -> b

I was talking about giving the same expression multiple types. So you can have:

  n :: Num a => a
  n = 1

and then do

  n :: Integral a => a

But again, we're talking about subtyping, and this isn't it. Consider the original problem, where we want a vector of objects of different concrete type. Haskell 98 doesn't help us here. The type

  Num a => [a]

is inhabited by heterogeneous lists.

The problem can be circumvented as described in the OP, or by using existential types. However, we still have hetergeneous lists, but the concrete type has been abstracted.

Okay, sorry, my arguments have been a little imprecise—the disadvantage of typing on a phone. I'll try to do better now.

(1) Given two typeclasses which have `class A x => B x` then the type `forall x . B x => x` can be coerced to `forall x . A x => x`. You can do this explicitly using existential types.

(2) Functions are a little weird since (->) is a profunctor and thus is contravariant in the first argument and covariant in the second. Thus, using the coercion above you'd note that any function where `forall x . A x => x` is an input may be replaced by `forall x . B x => x` and when it's an output then the replacement goes the other way.

(3) fromIntegral is a bad example because it relies on the specific functions in the typeclasses Integral and Num--- it's just `fromIntegral . toIntegral`.

I think this kind of stuff is a kind of subtyping. It seems to follow the Liskov Substitution Principle.

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!

Essentially I'm saying nothing more than I can change a function A -> (B, C) to a function (A, X) -> B. Typeclasses provide a way to represent a more general space of those functions. Existential types are the explicit way of writing the kind of subtyping I'm talking about—so if you need it to be an explicit hierarchy then, yes, you need extensions to Haskell98.

The best example of doing this without existential types (though it violates Haskell98 in its own way) the lens library. It absolutely provides a natural subtyping hierarchy without using existential types, though all of the coercions are implicit.

I'm very confident in my understanding of the Haskell behavior, but I'm happy to concede that my use of subtyping terminology is off. I cannot see how the behavior you see in lens doesn't provide a stellar example of LSP, though.

Ahh, hah. My mistake on the kinds. I changed it from an example on Num and Show because I don't much like how they're related.