Consider not allowing materialization to Never to provide assignability

[refi64]

Summary

I feel like this is probably a dupe of something, but I can't find anything like this. playground

from typing import Any

def f(i: int) -> None:
    pass

def g(x: Any) -> None:
    if isinstance(x, str):
        f(x) # passes?

def h(x: int | str) -> None:
    if isinstance(x, str):
        f(x) # correctly fails: Expected `int`, found `str`

I'm not aware of any type-system reason f(x) in g should succeed, and it seems to get caught by other type checkers.

Version

f9ba228f6 (playground)

[carljm]

Yes, this is an area of our intersections implementation we've been discussing recently (cc @JelleZijlstra ). If we replace int and str in this example with non-disjoint types (e.g. non-final user classes A and B), then it is clearly correct for this example to not error, because the actual type of x could be a common subclass of both A and B, and the use of Any requests that we assume any possible scenario in which the usage of x could be correct.

from typing import Any

class A: ...
class B: ...

def f(i: A) -> None:
    pass

def g(x: Any) -> None:
    if isinstance(x, B):
        f(x) # passes

It's important to make the distinction here between Any and object -- we do not "narrow away" Any in this example because it is already both narrower and wider than the type B, since it represents any possible type, including a hypothetical subtype of B. So we can only narrow to the intersection B & Any, which is the gradual type with upper bound B (but may actually be any subtype of B, including a subtype that is also a subtype of A.)

With disjoint types such as int and str that cannot be multiply-inherited together, our behavior here is more questionable. Effectively what we are modeling is the possibility that if x is actually originally of type int, that would render the if block unreachable (x within that block is of type Never), and Never is assignable to int. This is all theoretically correct and obeys the gradual guarantee, but it may not be the most practically desirable behavior. Probably we should (in general) consider a gradual type not assignable to another type if Never is the only possible materialization that would allow the assignment.

[carljm]

Prior discussion was in #639

[mikeshardmind]

Probably we should (in general) consider a gradual type not assignable to another type if Never is the only possible materialization that would allow the assignment.

This interpretation is what I've been assuming with the current work to formalize intersections. In particular, it has better outcomes with intersections of bound methods and decidability of return types for a given application of the bound method, as it more cleanly separates cases that may have a returned value from those that never can.

[refi64]

If we replace int and str in this example with non-disjoint types (e.g. non-final user classes A and B), then it is clearly correct for this example to not error, because the actual type of x could be a common subclass of both A and B, and the use of Any requests that we assume any possible scenario in which the usage of x could be correct.

This does abstractly make sense (specifically wrt Any's semantics), but the fact that other type checkers do error here would make this behavior rather surprising.

More generally, we probably misuse Any a bit in the Python world, compared to e.g. TypeScript after I learned unknown existed, at least, so there are a bunch of places where you can get an unexpected Any because something was explicitly typed as such. In the case where I hit this, I had a templatelib.Template, which uses Any quite widely:

@final
class Template:  # TODO: consider making `Template` generic on `TypeVarTuple`
    strings: tuple[str, ...]
    interpolations: tuple[Interpolation[Any], ...]

    def __new__(cls, *args: str | Interpolation[Any]) -> Template: ...
    def __iter__(self) -> Iterator[str | Interpolation[Any]]: ...
    def __add__(self, other: Template, /) -> Template: ...
    def __class_getitem__(cls, item: Any, /) -> GenericAlias: ...
    @property
    def values(self) -> tuple[Any, ...]: ...  # Tuple of interpolation values, which can have any type

So just accessing an interpolation.value provided to me by the standard type hints can result in accidents.

Perhaps it might be worth adding a rule for this? Not quite as stringent as #622, but just making isinstance in cases like this behave more like elsewhere.

[carljm]

Yes, I agree that Any is over-used in typeshed; if interpolation values "can have any type", they should be typed as object, not Any.

I'm not sure that this is sufficient reason to implement somewhat arbitrary carve-outs to the semantics of Any. I think this becomes quite difficult to do once intersections are added to the type system, because it requires either breaking the invariant that type narrowing is an intersection between the prior type and the new narrowing information, or it requires breaking the semantics of Any in intersections in general. Neither of those is particularly attractive.

Adding a rule is easily done, but this is not a rule, it is a change to the semantics of types. It can still be an option, but we have to be quite cautious with such options, or we get a massive cross-product of possible type semantics to test.