Skip to content

Commit

Permalink
[red-knot] Simplify unions of T and ~T
Browse files Browse the repository at this point in the history
  • Loading branch information
sharkdp committed Jan 10, 2025
1 parent f2c3ddc commit 29f0bf5
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 14 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -313,22 +313,24 @@ def _(

### Union of a type and its negation

Similarly, if we have both `P` and `~P` in a _union_, we could simplify that to `object`. However,
this is a rather costly operation which would require us to build the negation of each type that we
add to a union, so this is not implemented at the moment.
Similarly, if we have both `P` and `~P` in a _union_, we can simplify that to `object`.

```py
from knot_extensions import Intersection, Not

class P: ...
class Q: ...

def _(
i1: P | Not[P],
i2: Not[P] | P,
i3: P | Q | Not[P],
i4: Not[P] | Q | P,
) -> None:
# These could be simplified to `object`
reveal_type(i1) # revealed: P | ~P
reveal_type(i2) # revealed: ~P | P
reveal_type(i1) # revealed: object
reveal_type(i2) # revealed: object
reveal_type(i3) # revealed: object
reveal_type(i4) # revealed: object
```

### Negation is an involution
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,22 +21,22 @@ else:
if x and not x:
reveal_type(x) # revealed: Never
else:
reveal_type(x) # revealed: Literal[0, "", b"", -1, "foo", b"bar"] | bool | None | tuple[()]
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]

if not (x and not x):
reveal_type(x) # revealed: Literal[0, "", b"", -1, "foo", b"bar"] | bool | None | tuple[()]
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
else:
reveal_type(x) # revealed: Never

if x or not x:
reveal_type(x) # revealed: Literal[-1, "foo", b"bar", 0, "", b""] | bool | None | tuple[()]
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
else:
reveal_type(x) # revealed: Never

if not (x or not x):
reveal_type(x) # revealed: Never
else:
reveal_type(x) # revealed: Literal[-1, "foo", b"bar", 0, "", b""] | bool | None | tuple[()]
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]

if (isinstance(x, int) or isinstance(x, str)) and x:
reveal_type(x) # revealed: Literal[-1, True, "foo"]
Expand Down Expand Up @@ -87,10 +87,10 @@ def f(x: A | B):
if x and not x:
reveal_type(x) # revealed: A & ~AlwaysFalsy & ~AlwaysTruthy | B & ~AlwaysFalsy & ~AlwaysTruthy
else:
reveal_type(x) # revealed: A & ~AlwaysTruthy | B & ~AlwaysTruthy | A & ~AlwaysFalsy | B & ~AlwaysFalsy
reveal_type(x) # revealed: A | B

if x or not x:
reveal_type(x) # revealed: A & ~AlwaysFalsy | B & ~AlwaysFalsy | A & ~AlwaysTruthy | B & ~AlwaysTruthy
reveal_type(x) # revealed: A | B
else:
reveal_type(x) # revealed: A & ~AlwaysTruthy & ~AlwaysFalsy | B & ~AlwaysTruthy & ~AlwaysFalsy
```
Expand Down Expand Up @@ -214,10 +214,10 @@ if x and not x:
reveal_type(y) # revealed: A & ~AlwaysFalsy & ~AlwaysTruthy
else:
y = x
reveal_type(y) # revealed: A & ~AlwaysTruthy | A & ~AlwaysFalsy
reveal_type(y) # revealed: A

# TODO: It should be A. We should improve UnionBuilder or IntersectionBuilder. (issue #15023)
reveal_type(y) # revealed: A & ~AlwaysTruthy | A & ~AlwaysFalsy
reveal_type(y) # revealed: A
```

## Truthiness of classes
Expand Down
13 changes: 13 additions & 0 deletions crates/red_knot_python_semantic/src/types/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,8 @@ impl<'db> UnionBuilder<'db> {

let mut to_add = ty;
let mut to_remove = SmallVec::<[usize; 2]>::new();
let ty_negated = ty.negate(self.db);

for (index, element) in self.elements.iter().enumerate() {
if Some(*element) == bool_pair {
to_add = KnownClass::Bool.to_instance(self.db);
Expand All @@ -80,6 +82,17 @@ impl<'db> UnionBuilder<'db> {
return self;
} else if element.is_subtype_of(self.db, ty) {
to_remove.push(index);
} else if ty_negated.is_subtype_of(self.db, *element) {
// We add `ty` to the union. We just checked that `~ty` is a subtype of an existing `element`.
// This also means that `~ty | ty` is a subtype of `element | ty`, because both elements in the
// first union are subtypes of the corresponding elements in the second union. But `~ty | ty` is
// just `object`. Since `object` is a subtype of `element | ty`, we can only conclude that
// `element | ty` must be `object` (object has no other supertypes). This means we can simplify
// the whole union to just `object`, since all other potential elements would also be subtypes of
// `object`.
self.elements.clear();
self.elements.push(KnownClass::Object.to_instance(self.db));
return self;
}
}
match to_remove[..] {
Expand Down

0 comments on commit 29f0bf5

Please sign in to comment.