[ty] Reachability constraints (#18621)

## Summary



* Completely removes the concept of visibility constraints. Reachability
constraints are now used to model the static visibility of bindings and
declarations. Reachability constraints are *much* easier to reason about
/ work with, since they are applied at the beginning of a branch, and
not applied retroactively. Removing the duplication between visibility
and reachability constraints also leads to major code simplifications
[^1]. For an overview of how the new constraint system works, see the
updated doc comment in `reachability_constraints.rs`.
* Fixes a [control-flow modeling bug
(panic)](https://github.com/astral-sh/ty/issues/365) involving `break`
statements in loops
* Fixes a [bug where](https://github.com/astral-sh/ty/issues/624) where
`elif` branches would have wrong reachability constraints
* Fixes a [bug where](https://github.com/astral-sh/ty/issues/648) code
after infinite loops would not be considered unreachble
* Fixes a panic on the `pywin32` ecosystem project, which we should be
able to move to `good.txt` once this has been merged.
* Removes some false positives in unreachable code because we infer
`Never` more often, due to the fact that reachability constraints now
apply retroactively to *all* active bindings, not just to bindings
inside a branch.
* As one example, this removes the `division-by-zero` diagnostic from
https://github.com/astral-sh/ty/issues/443 because we now infer `Never`
for the divisor.
* Supersedes and includes similar test changes as
https://github.com/astral-sh/ruff/pull/18392


closes https://github.com/astral-sh/ty/issues/365
closes https://github.com/astral-sh/ty/issues/624
closes https://github.com/astral-sh/ty/issues/642
closes https://github.com/astral-sh/ty/issues/648

## Benchmarks

Benchmarks on black, pandas, and sympy showed that this is neither a
performance improvement, nor a regression.

## Test Plan

Regression tests for:
- [x] https://github.com/astral-sh/ty/issues/365
- [x] https://github.com/astral-sh/ty/issues/624
- [x] https://github.com/astral-sh/ty/issues/642
- [x] https://github.com/astral-sh/ty/issues/648

[^1]: I'm afraid this is something that @carljm advocated for since the
beginning, and I'm not sure anymore why we have never seriously tried
this before. So I suggest we do *not* attempt to do a historical deep
dive to find out exactly why this ever became so complicated, and just
enjoy the fact that we eventually arrived here.

---------

Co-authored-by: Carl Meyer <carl@astral.sh>
This commit is contained in:
David Peter 2025-06-17 09:24:28 +02:00 committed by GitHub
parent c22f809049
commit 3a77768f79
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
18 changed files with 683 additions and 806 deletions

View file

@ -827,8 +827,8 @@ if sys.version_info >= (3, 12):
from exporter import *
# it's correct to have no diagnostics here as this branch is unreachable
reveal_type(A) # revealed: Unknown
reveal_type(B) # revealed: bool
reveal_type(A) # revealed: Never
reveal_type(B) # revealed: Never
else:
from exporter import *

View file

@ -52,7 +52,7 @@ def _(x: A | B):
if False and isinstance(x, A):
# TODO: should emit an `unreachable code` diagnostic
reveal_type(x) # revealed: A
reveal_type(x) # revealed: Never
else:
reveal_type(x) # revealed: A | B
@ -65,7 +65,7 @@ def _(x: A | B):
reveal_type(x) # revealed: A | B
else:
# TODO: should emit an `unreachable code` diagnostic
reveal_type(x) # revealed: B & ~A
reveal_type(x) # revealed: Never
reveal_type(x) # revealed: A | B
```

View file

@ -199,7 +199,7 @@ def f(x: Literal[0, 1], y: Literal["", "hello"]):
reveal_type(y) # revealed: Literal["", "hello"]
if (x or not x) and (y and not y):
reveal_type(x) # revealed: Literal[0, 1]
reveal_type(x) # revealed: Never
reveal_type(y) # revealed: Never
else:
# ~(x or not x) or ~(y and not y)

View file

@ -127,7 +127,8 @@ class B: ...
def _[T](x: A | B):
if type(x) is A[str]:
reveal_type(x) # revealed: (A[int] & A[Unknown]) | (B & A[Unknown])
# `type()` never returns a generic alias, so `type(x)` cannot be `A[str]`
reveal_type(x) # revealed: Never
else:
reveal_type(x) # revealed: A[int] | B
```

View file

@ -994,6 +994,39 @@ else:
reveal_type(x) # revealed: Literal[1]
```
#### `if` nested inside `while True`
These are regression test for <https://github.com/astral-sh/ty/issues/365>. First, make sure that we
do not panic in the original scenario:
```py
def flag() -> bool:
return True
while True:
if flag():
break
else:
c = 1
break
c # error: [possibly-unresolved-reference]
```
And also check that we understand control flow correctly:
```py
c = 1
while True:
if False:
c = 2
break
break
reveal_type(c) # revealed: Literal[1]
```
## `match` statements
```toml

View file

@ -72,6 +72,17 @@ def f2():
# TODO: we should mark this as unreachable
print("unreachable")
def f3():
if False:
return
elif True:
return
else:
pass
# TODO: we should mark this as unreachable
print("unreachable")
```
### `Never` / `NoReturn`
@ -211,9 +222,8 @@ reachable or not. Some developers like to use things like early `return` stateme
and for this use case, it is helpful to still see some diagnostics in unreachable sections.
We currently follow the second approach, but we do not attempt to provide the full set of
diagnostics in unreachable sections. In fact, we silence a certain category of diagnostics
(`unresolved-reference`, `unresolved-attribute`, …), in order to avoid *incorrect* diagnostics. In
the future, we may revisit this decision.
diagnostics in unreachable sections. In fact, a large number of diagnostics are suppressed in
unreachable code, simply due to the fact that we infer `Never` for most of the symbols.
### Use of variables in unreachable code
@ -301,7 +311,8 @@ elif sys.version_info >= (3, 11):
elif sys.version_info >= (3, 10):
pass
else:
pass
# This branch is also unreachable, because the previous `elif` branch is always true
ExceptionGroup # no error here
```
And for nested `if` statements:
@ -378,6 +389,18 @@ while sys.version_info >= (3, 11):
ExceptionGroup
```
### Infinite loops
We also do not emit diagnostics in unreachable code after an infinite loop:
```py
def f():
while True:
pass
ExceptionGroup # no error here
```
### Silencing errors for actually unknown symbols
We currently also silence diagnostics for symbols that are not actually defined anywhere. It is
@ -500,33 +523,26 @@ def f():
1 / 0 # error: [division-by-zero]
```
## Limitations of the current approach
### Conflicting type information
The current approach of silencing only a subset of diagnostics in unreachable code leads to some
problems, and we may want to re-evaluate this decision in the future. To illustrate, consider the
following example:
We also support cases where type information for symbols conflicts between mutually exclusive
branches:
```py
if False:
import sys
if sys.version_info >= (3, 11):
x: int = 1
else:
x: str = "a"
if False:
# TODO We currently emit a false positive here:
# error: [invalid-assignment] "Object of type `Literal["a"]` is not assignable to `int`"
if sys.version_info >= (3, 11):
other: int = x
else:
other: str = x
```
The problem here originates from the fact that the type of `x` in the `False` branch conflicts with
the visible type of `x` in the `True` branch. When we type-check the lower `False` branch, we only
see the visible definition of `x`, which has a type of `str`.
In principle, this means that all diagnostics that depend on type information from "outside" the
unreachable section should be silenced. Similar problems to the one above can occur for other rule
types as well:
This is also supported for function calls, attribute accesses, etc.:
```py
from typing import Literal
@ -554,24 +570,14 @@ else:
number: Literal[0] = 0
if False:
# TODO
# error: [invalid-argument-type]
f(2)
# TODO
# error: [unknown-argument]
g(a=2, b=3)
# TODO
# error: [invalid-assignment]
C.x = 2
d: D = D()
# TODO
# error: [call-non-callable]
d()
# TODO
# error: [division-by-zero]
1 / number
```