[ty] Improve exhaustiveness analysis for type variables with bounds or constraints (#21172)

This commit is contained in:
Alex Waygood 2025-10-31 16:51:11 -04:00 committed by GitHub
parent 6337e22f0c
commit a32d5b8dc4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 85 additions and 31 deletions

View file

@ -417,3 +417,55 @@ class Answer(Enum):
case Answer.NO:
return False
```
## Exhaustiveness checking for type variables with bounds or constraints
```toml
[environment]
python-version = "3.12"
```
```py
from typing import assert_never, Literal
def f[T: bool](x: T) -> T:
match x:
case True:
return x
case False:
return x
case _:
reveal_type(x) # revealed: Never
assert_never(x)
def g[T: Literal["foo", "bar"]](x: T) -> T:
match x:
case "foo":
return x
case "bar":
return x
case _:
reveal_type(x) # revealed: Never
assert_never(x)
def h[T: int | str](x: T) -> T:
if isinstance(x, int):
return x
elif isinstance(x, str):
return x
else:
reveal_type(x) # revealed: Never
assert_never(x)
def i[T: (int, str)](x: T) -> T:
match x:
case int():
pass
case str():
pass
case _:
reveal_type(x) # revealed: Never
assert_never(x)
return x
```

View file

@ -781,37 +781,6 @@ impl<'db> IntersectionBuilder<'db> {
seen_aliases,
)
}
Type::EnumLiteral(enum_literal) => {
let enum_class = enum_literal.enum_class(self.db);
let metadata =
enum_metadata(self.db, enum_class).expect("Class of enum literal is an enum");
let enum_members_in_negative_part = self
.intersections
.iter()
.flat_map(|intersection| &intersection.negative)
.filter_map(|ty| ty.as_enum_literal())
.filter(|lit| lit.enum_class(self.db) == enum_class)
.map(|lit| lit.name(self.db))
.chain(std::iter::once(enum_literal.name(self.db)))
.collect::<FxHashSet<_>>();
let all_members_are_in_negative_part = metadata
.members
.keys()
.all(|name| enum_members_in_negative_part.contains(name));
if all_members_are_in_negative_part {
for inner in &mut self.intersections {
inner.add_negative(self.db, enum_literal.enum_class_instance(self.db));
}
} else {
for inner in &mut self.intersections {
inner.add_negative(self.db, ty);
}
}
self
}
_ => {
for inner in &mut self.intersections {
inner.add_negative(self.db, ty);
@ -1177,6 +1146,39 @@ impl<'db> InnerIntersectionBuilder<'db> {
fn build(mut self, db: &'db dyn Db) -> Type<'db> {
self.simplify_constrained_typevars(db);
// If any typevars are in `self.positive`, speculatively solve all bounded type variables
// to their upper bound and all constrained type variables to the union of their constraints.
// If that speculative intersection simplifies to `Never`, this intersection must also simplify
// to `Never`.
if self.positive.iter().any(|ty| ty.is_type_var()) {
let mut speculative = IntersectionBuilder::new(db);
for pos in &self.positive {
match pos {
Type::TypeVar(type_var) => {
match type_var.typevar(db).bound_or_constraints(db) {
Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
speculative = speculative.add_positive(bound);
}
Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
speculative = speculative.add_positive(Type::Union(constraints));
}
// TypeVars without a bound or constraint implicitly have `object` as their
// upper bound, and it is always a no-op to add `object` to an intersection.
None => {}
}
}
_ => speculative = speculative.add_positive(*pos),
}
}
for neg in &self.negative {
speculative = speculative.add_negative(*neg);
}
if speculative.build().is_never() {
return Type::Never;
}
}
match (self.positive.len(), self.negative.len()) {
(0, 0) => Type::object(),
(1, 0) => self.positive[0],