> A is a subtype of B then `Vec<A>` is a subtype of `Vec<B>`

That’s just not true. Java would permit it but then you get ArrayStoreException so this is unsound from a type system perspective. To make this sound, we need to classify each use of a type parameter to be covariant, contravariant, or invariant.