diff --git a/crates/red_knot_python_semantic/resources/mdtest/comparison/intersections.md b/crates/red_knot_python_semantic/resources/mdtest/comparison/intersections.md index c8c3ffa977..3d40f79663 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/comparison/intersections.md +++ b/crates/red_knot_python_semantic/resources/mdtest/comparison/intersections.md @@ -92,8 +92,7 @@ def _(o: object): n = 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 not n) # revealed: Literal[True] ``` diff --git a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md index a807c10a59..dfe023daa4 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md +++ b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md @@ -283,6 +283,21 @@ def _( 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 Continuing with more [complement laws], if we see both `P` and `~P` in an intersection, we can diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md index cdf3043ed3..3da4221cfa 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md +++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md @@ -91,8 +91,7 @@ if isinstance(x, (A, B)): elif isinstance(x, (A, C)): reveal_type(x) # revealed: C & ~A & ~B else: - # TODO: Should be simplified to ~A & ~B & ~C - reveal_type(x) # revealed: object & ~A & ~B & ~C + reveal_type(x) # revealed: ~A & ~B & ~C ``` ## No narrowing for instances of `builtins.type` diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs index 67d5891b4a..c19a4f06ce 100644 --- a/crates/red_knot_python_semantic/src/types/builder.rs +++ b/crates/red_knot_python_semantic/src/types/builder.rs @@ -284,10 +284,16 @@ impl<'db> InnerIntersectionBuilder<'db> { } } _ => { - let addition_is_bool_instance = new_positive + let known_instance = new_positive .into_instance() - .and_then(|instance| instance.class.known(db)) - .is_some_and(KnownClass::is_bool); + .and_then(|instance| instance.class.known(db)); + + 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() { match existing_positive {