As @Liz touched on briefly over in Revisiting variance - #37 by Liz, I think at least some of the problems here (like many of the problems that came up in the intersection PEP work) boil down to incorrect over-simplification of intersection types. Because we don’t have a formal spec for intersections (and also because the concept can be confusing for users), current type checkers don’t necessarily have a well-fleshed out internal representation for intersection types, and tend to be eager to simplify them to non-intersections, even when it isn’t correct to do so. (There were more examples of this related to Any in my PyCon typing summit talk.)
If we have a generic class MySequence which is a subtype of Sequence, but also uses the typevar in contravariant position and is thus invariant, and you have a TypeIs function that narrows Sequence[object] to Sequence[int], applying that TypeIs function to an instance of MySequence[object] should result in the type MySequence[object] & Sequence[int]. The unsafety you might observe in such a case is a result of type checkers simplifying that intersection to MySequence[int], but this is an incorrect simplification. The correct behavior is to leave the intersection type unsimplified.
The theoretical reason it is incorrect is because MySequence is invariant in its type parameter, therefore there is no subtype relationship between MySequence[object] & Sequence[int], therefore the intersection can’t be simplified.
The intuitive reason that matters in this particular case is because MySequence may have additional runtime state related to the generic type, and a runtime narrowing function meant to apply to Sequence can’t possibly know about or check the actual type of that state at runtime, it can only check the state that’s part of the Sequence type.
The result of leaving the intersection type un-simplified would be that methods present on both Sequence and MySequence that return T would end up returning object & int which does simplify to int. Whereas methods present only on MySequence would still be typed as operating on object.
So if we want to make TypeIs safe in this respect, there’s no need to change the general rules around variance and subtyping in super-disruptive ways, there’s only a need for more correct handling of intersection simplification.
(Shared mutability still remains its own problem, but that applies to type narrowing more broadly.)