Support `isinstance` narrowing of specialized generic classes

[MatthewMckee4]

We currently narrow like this:

class A[T]: ...

def _(x: A[int] | int):
    if isinstance(x, A):
        reveal_type(x)  # revealed: (A[int] & A[Unknown]) | (int & A[Unknown])
    else:
        reveal_type(x)  # revealed: (A[int] & ~A[Unknown]) | (int & ~A[Unknown])

Ideally we would reveal:

class A[T]: ...

def _(x: A[int] | int):
    if isinstance(x, A):
        reveal_type(x)  # revealed: A[int]
    else:
        reveal_type(x)  # revealed: int

[jelle-openai]

It's perhaps debatable if you should care, but note the narrowing you propose is unsound in the positive case:

>>> from typing import reveal_type
>>> 
>>> class A[T]: ...
... 
>>> class Sneaky(A[str], int): ...
... 
>>> def _(x: A[int] | int):
...     if isinstance(x, A):
...         print("it's an A")
...     else:
...         print("it's an int")
... 
>>> _(Sneaky())
it's an A

The negative case narrowing is sound though. Seems like A[int] & ~A[Unknown] should simplify to Never.

[MatthewMckee4]

Good catch! thanks

[JelleZijlstra]

Seems like A[int] & ~A[Unknown] should simplify to Never

Thinking about it more, this is incorrect. A[Unknown] may materialize to something like A[str], which doesn't overlap with A[int]. I think the problem is instead that A[Unknown] is the wrong type to use here. After isinstance(x, A), x should be narrowed to whatever it was before & any instance of A. But the type "any instance of A" cannot always be expressed in the type system. For covariant types, it's A[object], but for invariant types there is no static type that represents a common supertype for all instantiations of A.

So the solution I'd lean towards is to add a new special internal type that represents "all instances of A".

[mikeshardmind]

So the solution I'd lean towards is to add a new special internal type that represents "all instances of A".

Might be worth specifying this as a clarification to TypeIs as well that this must negate all possible A probably can't, with how TypeIs is specified (which might indicate that this should be a typing type and not a typechecker internal for user expressibility), but otherwise I agree (and think it's unfortunate that A here automatically means A[Default or Unknown] rather than All possible A)

[carljm]

Discussed this with @dcreager in person. We agree with @JelleZijlstra that we need to be able to represent the (fully static!) type "all instances of A" in order to handle this narrowing better. We think that should probably be done by making NominalInstanceType an enum, instead of simply a wrapper around ClassType, where we add a variant of NominalInstanceType, something like AllSpecializations, to represent this type. Maybe we could display the type as something like A[*]? Definitely some naming bikesheds here.

(The alternative would be to add the new variant to ClassType, which is already an enum, but this would be more invasive because ClassType is used in more places, including in places where "all possible specializations" should not be allowed, e.g. in ClassBase.)

(As Jelle points out, we could potentially use A[object] in case A is covariant in its typevar, or A[Never] in case it is contravariant. But this might complicate the implementation, since then * would need to be a per-typevar "specialization" that we only use for invariant typevars. It seems simpler to make it all-or-nothing -- that is, it always applies across all typevars -- which is all we actually need, and what is implied by the implementation described above. I guess we could still avoid using it in the special case of arity-one generic types that are co- or contra-variant in their typevar.)

[JelleZijlstra]

What should this do?

def f(x: object):
    if isinstance(x, list):
       reveal_type(x[0])
       x[0] = 42

(Mypy and pyright reveal Any/Unknown and allow the assignment. This is unsound, because f may be passed e.g. a list[str].)

[MatthewMckee4]

the (fully static!) type "all instances of A"

One question:

class A[T: Any]: ...

def _(x: A[int] | int):
    if isinstance(x, A):
        reveal_type(x) # Is this a fully static type?

[mikeshardmind]

Maybe we could display the type as something like A[*]? Definitely some naming bikesheds here.

I still think this probably needs to go over to a typing proposal of some sort, What should the typeshed do here? (and a few other places)

https://github.com/python/typeshed/blob/6007267f68ed94a49421cff17b03e23a0177ad8c/stdlib/inspect.pyi#L234-L236

def isgenerator(object: object) -> TypeIs[GeneratorType[Any, Any, Any]]: ...
def iscoroutine(object: object) -> TypeIs[CoroutineType[Any, Any, Any]]: ...
def isawaitable(object: object) -> TypeIs[Awaitable[Any]]: ...

What should users of the standard library do here?

What should people who have TypeIs functions that work on invariant generics do?

Whatever that user-expression is should probably also be how ty presents it.

[carljm]

After thinking more about Jelle's latest example, I'm no longer convinced we should do this. It seems to require a more general existential type ("like Any, but unforgiving") for the type variable to resolve to, and adding this to the type system seems like a real can of worms. It may be that the current behavior is the best we can reasonably do, even though it introduces Unknown and can thus result in unsoundness. (I also discussed this here at PyCon sprints with the Pyrefly team, and they also feel that using Any/Unknown is the best available option here.)

I'm curious whether the OP here was motivated by some unpleasant typing behavior resulting from the complex types we currently infer, or simply by the fact that they look "too complex"? If it's the former, I'd like to see what we can do to address that. If it's the latter, I'd be inclined to say that we are already doing the best feasible thing here, and this is "behaving as expected." I think given the use of Unknown, the (lack of) simplification that we currently perform is correct (and should still provide some better behavior than type checkers which don't use intersection types.)

[mikeshardmind]

It seems to require a more general existential type ("like Any, but unforgiving") for the type variable to resolve to

I posted a suggestion for handling this over on discourse, I think a special value that's only valid to express "A[?] For All possible ?" rather than the current state where A[Any] is "A[?] for Some possible ?" and is not valid for use outside of describing generics, and is not valid as a standalone type-expression or solution for a particular materialization works here.

[carljm]

and is not valid for use outside of describing generics

The thing that convinced me this is not a can of worms we want to tackle right now, is Jelle's last question above, which indicates (especially if you extrapolate to other operations, like pulling an element from the list) that we can't actually get away with having this "existential type" limited to "describing generic types" -- it only actually works if it's a first-class type on its own.