> The unfortunate fact is that a fully sound Python type system would be a pain to use.

Even beyond Python, most gradual type systems are unsound by design.