From fef3c6e8af317febff6abb0f640d454259d323d1 Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Tue, 11 Mar 2025 18:29:58 +0200 Subject: [PATCH 1/7] Improve is_disjoint for two intersections --- .../mdtest/type_properties/is_assignable_to.md | 5 +++++ .../mdtest/type_properties/is_disjoint_from.md | 14 +++++++++++++- crates/red_knot_python_semantic/src/types.rs | 14 ++++++-------- 3 files changed, 24 insertions(+), 9 deletions(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md index 97102aa6b7c226..54c313f789dba6 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md @@ -266,6 +266,10 @@ static_assert(is_assignable_to(Intersection[int, Parent], Intersection[int, Not[ static_assert(not is_assignable_to(int, Not[int])) static_assert(not is_assignable_to(int, Not[Literal[1]])) +static_assert(is_assignable_to(Not[Parent], Not[Child1])) +static_assert(not is_assignable_to(Not[Parent], Parent)) +static_assert(not is_assignable_to(Intersection[Unrelated, Not[Parent]], Parent)) + # Intersection with `Any` dominates the left hand side of intersections static_assert(is_assignable_to(Intersection[Any, Parent], Parent)) static_assert(is_assignable_to(Intersection[Any, Child1], Parent)) @@ -277,6 +281,7 @@ static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersectio # Even Any & Not[Parent] is assignable to Parent, since it could be Never static_assert(is_assignable_to(Intersection[Any, Not[Parent]], Parent)) +static_assert(is_assignable_to(Intersection[Any, Not[Parent]], Not[Parent])) # Intersection with `Any` is effectively ignored on the right hand side for the sake of assignment static_assert(is_assignable_to(Parent, Intersection[Any, Parent])) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index d88100e8b496d7..a20d6fe7e58b6c 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -96,7 +96,7 @@ static_assert(not is_disjoint_from(Literal[1, 2], Literal[2, 3])) ```py from typing_extensions import Literal, final -from knot_extensions import Intersection, is_disjoint_from, static_assert +from knot_extensions import Intersection, is_disjoint_from, static_assert, Not @final class P: ... @@ -130,6 +130,18 @@ static_assert(not is_disjoint_from(Y, Z)) static_assert(not is_disjoint_from(Intersection[X, Y], Z)) static_assert(not is_disjoint_from(Intersection[X, Z], Y)) static_assert(not is_disjoint_from(Intersection[Y, Z], X)) + +# If one side has a positive element and the other side has a negative of that element, they are disjoint +static_assert(is_disjoint_from(int, Not[int])) +static_assert(is_disjoint_from(Intersection[X, Y, Not[Z]], Intersection[X, Z])) + +class Parent: ... +class Child(Parent): ... + +static_assert(not is_disjoint_from(Parent, Child)) +static_assert(not is_disjoint_from(Parent, Not[Child])) +static_assert(not is_disjoint_from(Not[Parent], Not[Child])) +static_assert(is_disjoint_from(Not[Parent], Child)) ``` ## Special types diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 811c35aa6e6aef..01c7d70d4b1a08 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -1000,17 +1000,15 @@ impl<'db> Type<'db> { (Type::Intersection(intersection), other) | (other, Type::Intersection(intersection)) => { - if intersection + intersection .positive(db) .iter() .any(|p| p.is_disjoint_from(db, other)) - { - true - } else { - // TODO we can do better here. For example: - // X & ~Literal[1] is disjoint from Literal[1] - false - } + // A & B & Not[C] is disjoint from C + || intersection + .negative(db) + .iter() + .any(|&neg_ty| other.is_assignable_to(db, neg_ty)) } // any single-valued type is disjoint from another single-valued type From b449d831ef9d3a27633d55ab81a16301177c765c Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Tue, 11 Mar 2025 18:40:11 +0200 Subject: [PATCH 2/7] Remove unnecessary handling of double intersections from is_subtype_of --- crates/red_knot_python_semantic/src/types.rs | 37 +++----------------- 1 file changed, 5 insertions(+), 32 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 01c7d70d4b1a08..4919ad0df8022b 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -580,38 +580,6 @@ impl<'db> Type<'db> { true } - (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { - // Check that all target positive values are covered in self positive values - target_intersection - .positive(db) - .iter() - .all(|&target_pos_elem| { - self_intersection - .positive(db) - .iter() - .any(|&self_pos_elem| self_pos_elem.is_subtype_of(db, target_pos_elem)) - }) - // Check that all target negative values are excluded in self, either by being - // subtypes of a self negative value or being disjoint from a self positive value. - && target_intersection - .negative(db) - .iter() - .all(|&target_neg_elem| { - // Is target negative value is subtype of a self negative value - self_intersection.negative(db).iter().any(|&self_neg_elem| { - target_neg_elem.is_subtype_of(db, self_neg_elem) - // Is target negative value is disjoint from a self positive value? - }) || self_intersection.positive(db).iter().any(|&self_pos_elem| { - self_pos_elem.is_disjoint_from(db, target_neg_elem) - }) - }) - } - - (Type::Intersection(intersection), _) => intersection - .positive(db) - .iter() - .any(|&elem_ty| elem_ty.is_subtype_of(db, target)), - (_, Type::Intersection(intersection)) => { intersection .positive(db) @@ -623,6 +591,11 @@ impl<'db> Type<'db> { .all(|&neg_ty| self.is_disjoint_from(db, neg_ty)) } + (Type::Intersection(intersection), _) => intersection + .positive(db) + .iter() + .any(|&elem_ty| elem_ty.is_subtype_of(db, target)), + // Note that the definition of `Type::AlwaysFalsy` depends on the return value of `__bool__`. // If `__bool__` always returns True or False, it can be treated as a subtype of `AlwaysTruthy` or `AlwaysFalsy`, respectively. (left, Type::AlwaysFalsy) => left.bool(db).is_always_false(), From 6f3a85f6b0ef53dbb12d32eb27b3473a922cb492 Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Wed, 12 Mar 2025 12:14:11 +0200 Subject: [PATCH 3/7] Fix disjointness of two intersections --- .../type_properties/is_disjoint_from.md | 23 +++++++++++++++---- crates/red_knot_python_semantic/src/types.rs | 16 ++++++++++++- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index a20d6fe7e58b6c..a14e831c34c37d 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -16,6 +16,7 @@ static_assert(not is_disjoint_from(bool, object)) static_assert(not is_disjoint_from(Any, bool)) static_assert(not is_disjoint_from(Any, Any)) +static_assert(not is_disjoint_from(Any, Not[Any])) static_assert(not is_disjoint_from(LiteralString, LiteralString)) static_assert(not is_disjoint_from(str, LiteralString)) @@ -95,8 +96,8 @@ static_assert(not is_disjoint_from(Literal[1, 2], Literal[2, 3])) ## Intersections ```py -from typing_extensions import Literal, final -from knot_extensions import Intersection, is_disjoint_from, static_assert, Not +from typing_extensions import Literal, final, Any +from knot_extensions import Intersection, is_disjoint_from, is_subtype_of, static_assert, Not, TypeOf @final class P: ... @@ -131,9 +132,10 @@ static_assert(not is_disjoint_from(Intersection[X, Y], Z)) static_assert(not is_disjoint_from(Intersection[X, Z], Y)) static_assert(not is_disjoint_from(Intersection[Y, Z], X)) -# If one side has a positive element and the other side has a negative of that element, they are disjoint +# If one side has a positive fully-static element and the other side has a negative of that element, they are disjoint static_assert(is_disjoint_from(int, Not[int])) static_assert(is_disjoint_from(Intersection[X, Y, Not[Z]], Intersection[X, Z])) +static_assert(is_disjoint_from(Intersection[X, Not[Literal[1]]], Literal[1])) class Parent: ... class Child(Parent): ... @@ -142,6 +144,16 @@ static_assert(not is_disjoint_from(Parent, Child)) static_assert(not is_disjoint_from(Parent, Not[Child])) static_assert(not is_disjoint_from(Not[Parent], Not[Child])) static_assert(is_disjoint_from(Not[Parent], Child)) +static_assert(is_disjoint_from(Intersection[X, Not[Parent]], Child)) +static_assert(is_disjoint_from(Intersection[X, Not[Parent]], Intersection[X, Child])) + +static_assert(not is_disjoint_from(Intersection[Any, X], Intersection[Any, Not[Y]])) +static_assert(not is_disjoint_from(Intersection[Any, Not[Y]], Intersection[Any, X])) + +static_assert(is_disjoint_from(Intersection[int, Any], Not[int])) +static_assert(is_disjoint_from(Not[int], Intersection[int, Any])) + +# [quickcheck] TEST FAILED. Arguments: (Intersection { pos: [SubclassOfAbcClass("ABC"),Any], neg: [] }, Intersection { pos: [], neg: [SubclassOfAbcClass("ABC")] }) ``` ## Special types @@ -164,7 +176,7 @@ static_assert(is_disjoint_from(Never, object)) ```py from typing_extensions import Literal, LiteralString -from knot_extensions import is_disjoint_from, static_assert +from knot_extensions import is_disjoint_from, static_assert, Intersection, Not static_assert(is_disjoint_from(None, Literal[True])) static_assert(is_disjoint_from(None, Literal[1])) @@ -177,6 +189,9 @@ static_assert(is_disjoint_from(None, type[object])) static_assert(not is_disjoint_from(None, None)) static_assert(not is_disjoint_from(None, int | None)) static_assert(not is_disjoint_from(None, object)) + +static_assert(is_disjoint_from(Intersection[int, Not[str]], None)) +static_assert(is_disjoint_from(None, Intersection[int, Not[str]])) ``` ### Literals diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 4919ad0df8022b..e28bd626c5f0ae 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -971,6 +971,20 @@ impl<'db> Type<'db> { .iter() .all(|e| e.is_disjoint_from(db, other)), + // If we have two intersections, we test the positive elements of each one against the other intersection + // Negative elements need a positive element on the other side in order to be disjoint. + // This is similar to what would happen if we tried to build a new intersection that combines the two + (Type::Intersection(self_intersection), Type::Intersection(other_intersection)) => { + self_intersection + .positive(db) + .iter() + .any(|p| p.is_disjoint_from(db, other)) + || other_intersection + .positive(db) + .iter() + .any(|p: &Type<'_>| p.is_disjoint_from(db, self)) + } + (Type::Intersection(intersection), other) | (other, Type::Intersection(intersection)) => { intersection @@ -981,7 +995,7 @@ impl<'db> Type<'db> { || intersection .negative(db) .iter() - .any(|&neg_ty| other.is_assignable_to(db, neg_ty)) + .any(|&neg_ty| other.is_subtype_of(db, neg_ty)) } // any single-valued type is disjoint from another single-valued type From 67c5efc1b53d0d6130b708c285262e54738a2d4e Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Wed, 12 Mar 2025 12:18:04 +0200 Subject: [PATCH 4/7] Improve documentation --- crates/red_knot_python_semantic/src/types.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index e28bd626c5f0ae..c9880224120bdc 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -580,6 +580,9 @@ impl<'db> Type<'db> { true } + // If both sides are intersections we need to handle the right side first + // (A & B & C) is a subtype of (A & B) because the left is a subtype of both A and B, + // but none of A, B, or C is a subtype of (A & B). (_, Type::Intersection(intersection)) => { intersection .positive(db) @@ -775,6 +778,10 @@ impl<'db> Type<'db> { .iter() .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)), + // If both sides are intersections we need to handle the right side first + // (A & B & C) is assignable to (A & B) because the left is assignable to both A and B, + // but none of A, B, or C is assignable to (A & B). + // // A type S is assignable to an intersection type T if // S is assignable to all positive elements of T (e.g. `str & int` is assignable to `str & Any`), and // S is disjoint from all negative elements of T (e.g. `int` is not assignable to Intersection[int, Not[Literal[1]]]). From 5f20d93d0ea4c32f7c318721960cd2cc232d381c Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Mar 2025 04:41:58 -0700 Subject: [PATCH 5/7] Update crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md --- .../resources/mdtest/type_properties/is_disjoint_from.md | 1 - 1 file changed, 1 deletion(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index a14e831c34c37d..0bc14348720be3 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -153,7 +153,6 @@ static_assert(not is_disjoint_from(Intersection[Any, Not[Y]], Intersection[Any, static_assert(is_disjoint_from(Intersection[int, Any], Not[int])) static_assert(is_disjoint_from(Not[int], Intersection[int, Any])) -# [quickcheck] TEST FAILED. Arguments: (Intersection { pos: [SubclassOfAbcClass("ABC"),Any], neg: [] }, Intersection { pos: [], neg: [SubclassOfAbcClass("ABC")] }) ``` ## Special types From 91b4c0f9b1fe082c7d574da6767d527624d3acff Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Wed, 12 Mar 2025 14:05:05 +0200 Subject: [PATCH 6/7] Fix lint --- .../resources/mdtest/type_properties/is_disjoint_from.md | 1 - 1 file changed, 1 deletion(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index 0bc14348720be3..96fc02f8b7c463 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -152,7 +152,6 @@ static_assert(not is_disjoint_from(Intersection[Any, Not[Y]], Intersection[Any, static_assert(is_disjoint_from(Intersection[int, Any], Not[int])) static_assert(is_disjoint_from(Not[int], Intersection[int, Any])) - ``` ## Special types From 698e6e394da5367520a60ca43c9a8f37e0debf30 Mon Sep 17 00:00:00 2001 From: Joey Geralnik Date: Wed, 12 Mar 2025 14:07:06 +0200 Subject: [PATCH 7/7] Cleanup imports --- .../resources/mdtest/type_properties/is_disjoint_from.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index 96fc02f8b7c463..9a600816fa09c1 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -97,7 +97,7 @@ static_assert(not is_disjoint_from(Literal[1, 2], Literal[2, 3])) ```py from typing_extensions import Literal, final, Any -from knot_extensions import Intersection, is_disjoint_from, is_subtype_of, static_assert, Not, TypeOf +from knot_extensions import Intersection, is_disjoint_from, static_assert, Not @final class P: ...