[red-knot] Simplify object out of intersections (#15511)

This commit is contained in:
Alex Waygood 2025-01-15 20:06:48 +00:00 committed by GitHub
parent c9b99e4bee
commit 49557a9129
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 26 additions and 7 deletions

View file

@ -92,8 +92,7 @@ def _(o: object):
n = None n = None
if o is not None: if o is not None:
reveal_type(o) # revealed: object & ~None reveal_type(o) # revealed: ~None
reveal_type(o is n) # revealed: Literal[False] reveal_type(o is n) # revealed: Literal[False]
reveal_type(o is not n) # revealed: Literal[True] reveal_type(o is not n) # revealed: Literal[True]
``` ```

View file

@ -283,6 +283,21 @@ def _(
reveal_type(not_object) # revealed: Never reveal_type(not_object) # revealed: Never
``` ```
### `object & ~T` is equivalent to `~T`
A second consequence of the fact that `object` is the top type is that `object` is always redundant
in intersections, and can be eagerly simplified out. `object & P` is equivalent to `P`;
`object & ~P` is equivalent to `~P` for any type `P`.
```py
from knot_extensions import Intersection, Not, is_equivalent_to, static_assert
class P: ...
static_assert(is_equivalent_to(Intersection[object, P], P))
static_assert(is_equivalent_to(Intersection[object, Not[P]], Not[P]))
```
### Intersection of a type and its negation ### Intersection of a type and its negation
Continuing with more [complement laws], if we see both `P` and `~P` in an intersection, we can Continuing with more [complement laws], if we see both `P` and `~P` in an intersection, we can

View file

@ -91,8 +91,7 @@ if isinstance(x, (A, B)):
elif isinstance(x, (A, C)): elif isinstance(x, (A, C)):
reveal_type(x) # revealed: C & ~A & ~B reveal_type(x) # revealed: C & ~A & ~B
else: else:
# TODO: Should be simplified to ~A & ~B & ~C reveal_type(x) # revealed: ~A & ~B & ~C
reveal_type(x) # revealed: object & ~A & ~B & ~C
``` ```
## No narrowing for instances of `builtins.type` ## No narrowing for instances of `builtins.type`

View file

@ -284,10 +284,16 @@ impl<'db> InnerIntersectionBuilder<'db> {
} }
} }
_ => { _ => {
let addition_is_bool_instance = new_positive let known_instance = new_positive
.into_instance() .into_instance()
.and_then(|instance| instance.class.known(db)) .and_then(|instance| instance.class.known(db));
.is_some_and(KnownClass::is_bool);
if known_instance == Some(KnownClass::Object) {
// `object & T` -> `T`; it is always redundant to add `object` to an intersection
return;
}
let addition_is_bool_instance = known_instance == Some(KnownClass::Bool);
for (index, existing_positive) in self.positive.iter().enumerate() { for (index, existing_positive) in self.positive.iter().enumerate() {
match existing_positive { match existing_positive {