> Both solutions have merit, but the idea of some implementations of the type checker having covariance and some contravariance is fairly disturbing.

Why can't we have both? That's the only way to properly type things, since immutable-get-style APIs are always going to be convariant, set-only style APIs (e.g. a function that takes 1 arg and returns None) are going to be contravariant and mutable get-set APIs (like most python collections) should really be invariant.