Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
64 changes: 33 additions & 31 deletions crates/ty_python_semantic/src/types/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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],
Expand Down
Loading