I think you’re pre-supposing something here that I would disagree with, and that all current type checkers in the conformance suite do behaviorally as well, though this isn’t specified other than TypeIs saying it should approximate isinstance for practical effects.
Given the types
from typing import Protocol, Iterator, Generic
from typing_extensions import TypeIs, TypeVar
X = TypeVar("X", int, float, int | float, default=int | float, covariant=True)
class A(Generic[X], Protocol):
_objs: tuple[X, ...]
def __init__(self, *objs: X):
self._objs: tuple[X, ...] = objs
def __iter__(self) -> Iterator[X]:
yield from self._objs
class B(A, Generic[X]):
def __init__(self, *objs: X, dtype: type[X] = int | float):
super().__init__(*objs)
self._dtype: type[X] = dtype
@property
def T(self) -> type[X]:
return self._dtype
Then the intersection A[int] & B should simplify to be B[int]
As T is covariant in A and B, B is a subtype of A, and int is a subtype of int | float.
(This doesn’t currently type check in any type checker for other reasons involving union assignability to type[X], one could write a protocol here instead to remedy this, but union assignability to type is currently being addressed in another discussion)
The problem with this is of course that if all of that holds, then we can chain together various evidence-based checks paired with a single indirection that loses the fact that SomeB.T exists because we are treating it as A for permissive use, and then get the wrong result
def is_Aint(s: A) -> TypeIs[A[int]]:
if not s: # while this shouldn't be needed, I'd rather not argue if that counts
# as pathological when it's irrelevant
raise ValueError("Refusing to narrow empty data container")
return all(isinstance(x, int) for x in s)
def div(n: A[X], d: int, dtype: type[X] | None = None) -> B[X]:
if isinstance(n, B):
if n.T in (float, float | int):
return B(*(i / d for i in n), dtype=n.T)
elif n.T is int:
return B(*(i // d for i in n), dtype=n.T)
else:
raise TypeError("Unsupported type for typed container {n.T!r}")
else:
return B(*(i / d for i in s))
def something_that_only_handles_int(x: B[int]):
if x.T is not int:
raise TypeError
# impl doesn't matter for this
def indirection(x: A): # this isn't implicitly Any, see default above.
if is_Aint(x):
s = div(x, 2)
something_that_only_handles_int(s) # boom
def example():
b = B(1, 2, 3)
indirection(b)
Before this is written off as a random hypothetical, this example is modeled off of numpy and how someone would handle needing types for numpy functions that allow array-like things as well, not just numpy types, without having to resort to a mypy plugin to fill in gaps.
__iter__ is used in place of full appropriate datamodel methods, substitute in all additional necessary dunders yourself, the problems still exist.
The chain of evidence-based checks can result in the wrong outcomes here because of the original narrowing on A without determining that we did not have a subtype of A that cares about more than what A does for type information.
It may or may not be possible to accidentally run into this issue, I’m inclined to think it is given how many people are still insisting that it isn’t one. I think it’s very likely to be a repeated real-world issue where people have unexpected outcomes given the time for this to start being used more, and for it to start happening in places that aren’t isolated to one codebase where someone can go “that’s not safe, we do this”, and start having types from different code bases involved in it.
Maybe it’s an acceptable issue given the tradeoffs and pragmatism various people value, but the sharp edges need documenting at a minimum.