[red-knot] Treat empty intersection as 'object', fix intersection simplification (#13880)

## Summary

- Properly treat the empty intersection as being of type `object`.
- Consequently, change the simplification method to explicitly add
`Never` to the positive side of the intersection when collapsing a type
such as `int & str` to `Never`, as opposed to just clearing both the
positive and the negative side.
- Minor code improvement in `bindings_ty`: use `peekable()` to check
whether the iterator over constraints is empty, instead of handling
first and subsequent elements separately.

fixes #13870

## Test Plan

- New unit tests for `IntersectionBuilder` to make sure the empty
intersection represents `object`.
- Markdown-based regression test for the original issue in #13870
This commit is contained in:
David Peter 2024-10-22 21:02:46 +02:00 committed by GitHub
parent 5d4edd61bf
commit c6ce52c29e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 37 additions and 12 deletions

View file

@ -1,5 +1,7 @@
# Narrowing for nested conditionals
## Multiple negative contributions
```py
def int_instance() -> int: ...
@ -11,3 +13,14 @@ if x != 1:
if x != 3:
reveal_type(x) # revealed: int & ~Literal[1] & ~Literal[2] & ~Literal[3]
```
## Multiple negative contributions with simplification
```py
x = 1 if flag1 else 2 if flag2 else 3
if x != 1:
reveal_type(x) # revealed: Literal[2, 3]
if x != 2:
reveal_type(x) # revealed: Literal[3]
```

View file

@ -148,18 +148,18 @@ fn bindings_ty<'db>(
binding,
constraints,
}| {
let mut constraint_tys =
constraints.filter_map(|constraint| narrowing_constraint(db, constraint, binding));
let mut constraint_tys = constraints
.filter_map(|constraint| narrowing_constraint(db, constraint, binding))
.peekable();
let binding_ty = binding_ty(db, binding);
if let Some(first_constraint_ty) = constraint_tys.next() {
let mut builder = IntersectionBuilder::new(db);
builder = builder
.add_positive(binding_ty)
.add_positive(first_constraint_ty);
for constraint_ty in constraint_tys {
builder = builder.add_positive(constraint_ty);
}
builder.build()
if constraint_tys.peek().is_some() {
constraint_tys
.fold(
IntersectionBuilder::new(db).add_positive(binding_ty),
IntersectionBuilder::add_positive,
)
.build()
} else {
binding_ty
}

View file

@ -253,6 +253,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
// A & B = Never if A and B are disjoint
if new_positive.is_disjoint_from(db, *existing_positive) {
*self = Self::new();
self.positive.insert(Type::Never);
return;
}
}
@ -265,6 +266,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
// S & ~T = Never if S <: T
if new_positive.is_subtype_of(db, *existing_negative) {
*self = Self::new();
self.positive.insert(Type::Never);
return;
}
// A & ~B = A if A and B are disjoint
@ -328,6 +330,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
// S & ~T = Never if S <: T
if existing_positive.is_subtype_of(db, new_negative) {
*self = Self::new();
self.positive.insert(Type::Never);
return;
}
// A & ~B = A if A and B are disjoint
@ -351,7 +354,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
fn build(mut self, db: &'db dyn Db) -> Type<'db> {
self.simplify_unbound();
match (self.positive.len(), self.negative.len()) {
(0, 0) => Type::Never,
(0, 0) => KnownClass::Object.to_instance(db),
(1, 0) => self.positive[0],
_ => {
self.positive.shrink_to_fit();
@ -523,6 +526,15 @@ mod tests {
assert_eq!(intersection.neg_vec(&db), &[t0]);
}
#[test]
fn build_intersection_empty_intersection_equals_object() {
let db = setup_db();
let ty = IntersectionBuilder::new(&db).build();
assert_eq!(ty, KnownClass::Object.to_instance(&db));
}
#[test]
fn build_intersection_flatten_positive() {
let db = setup_db();