From d30e8e2c0972dac54fa12bb9c7131d73052cf036 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Wed, 12 Mar 2025 01:32:14 +0900 Subject: [PATCH 1/3] stabilize `all_type_pairs_can_be_assigned_from_their_intersection`, --- .../resources/mdtest/intersection_types.md | 12 + .../resources/mdtest/type_api.md | 4 + .../type_properties/is_assignable_to.md | 56 ++- .../type_properties/is_disjoint_from.md | 12 +- .../is_gradual_equivalent_to.md | 4 +- .../mdtest/type_properties/is_subtype_of.md | 39 +- crates/red_knot_python_semantic/src/types.rs | 414 ++++++++++++++++-- .../src/types/builder.rs | 18 +- .../src/types/property_tests.rs | 1 - .../src/types/type_ordering.rs | 42 +- 10 files changed, 546 insertions(+), 56 deletions(-) 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 a7f0441653aa9..a2f1ef63587c0 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md +++ b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md @@ -663,6 +663,7 @@ to the fact that `bool` is a `@final` class at runtime that cannot be subclassed ```py from knot_extensions import Intersection, Not, AlwaysTruthy, AlwaysFalsy +from typing_extensions import Literal class P: ... @@ -686,6 +687,17 @@ def f( reveal_type(f) # revealed: Never reveal_type(g) # revealed: Never reveal_type(h) # revealed: Never + +def never( + a: Intersection[Intersection[AlwaysFalsy, Not[Literal[False]]], bool], + b: Intersection[Intersection[AlwaysTruthy, Not[Literal[True]]], bool], + c: Intersection[Intersection[Literal[True], Not[AlwaysTruthy]], bool], + d: Intersection[Intersection[Literal[False], Not[AlwaysFalsy]], bool], +): + reveal_type(a) # revealed: Never + reveal_type(b) # revealed: Never + reveal_type(c) # revealed: Never + reveal_type(d) # revealed: Never ``` ## Simplification of `LiteralString`, `AlwaysTruthy` and `AlwaysFalsy` diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_api.md b/crates/red_knot_python_semantic/resources/mdtest/type_api.md index 922ccaca06e18..90be97f57b9dd 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_api.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_api.md @@ -111,7 +111,11 @@ from typing_extensions import Literal from knot_extensions import AlwaysFalsy, AlwaysTruthy, is_subtype_of, static_assert static_assert(is_subtype_of(Literal[True], AlwaysTruthy)) +static_assert(is_subtype_of(Literal["a"], AlwaysTruthy)) +static_assert(is_subtype_of(Literal[1], AlwaysTruthy)) static_assert(is_subtype_of(Literal[False], AlwaysFalsy)) +static_assert(is_subtype_of(Literal[""], AlwaysFalsy)) +static_assert(is_subtype_of(Literal[0], AlwaysFalsy)) static_assert(not is_subtype_of(int, AlwaysFalsy)) static_assert(not is_subtype_of(str, AlwaysFalsy)) 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 97102aa6b7c22..0d62deb97a79d 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 @@ -206,8 +206,8 @@ static_assert(not is_assignable_to(tuple[Any, Literal[2]], tuple[int, str])) ## Union types ```py -from knot_extensions import static_assert, is_assignable_to, Unknown -from typing import Literal, Any +from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_assignable_to, Unknown +from typing_extensions import Literal, Any, LiteralString static_assert(is_assignable_to(int, int | str)) static_assert(is_assignable_to(str, int | str)) @@ -227,13 +227,18 @@ static_assert(not is_assignable_to(int | None, str | None)) static_assert(not is_assignable_to(Literal[1] | None, int)) static_assert(not is_assignable_to(Literal[1] | None, str | None)) static_assert(not is_assignable_to(Any | int | str, int)) + +static_assert(is_assignable_to(bool, Literal[False] | AlwaysTruthy)) +static_assert(is_assignable_to(bool, Literal[True] | AlwaysFalsy)) +static_assert(not is_assignable_to(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy)) +static_assert(is_assignable_to(LiteralString, Literal[""] | AlwaysTruthy)) ``` ## Intersection types ```py -from knot_extensions import static_assert, is_assignable_to, Intersection, Not -from typing_extensions import Any, Literal +from knot_extensions import static_assert, is_assignable_to, Intersection, Not, AlwaysTruthy, AlwaysFalsy +from typing_extensions import Any, Literal, final, LiteralString class Parent: ... class Child1(Parent): ... @@ -291,6 +296,49 @@ static_assert(is_assignable_to(Intersection[Any, Unrelated], Intersection[Any, P static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersection[Any, Parent, Unrelated])) static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]])) static_assert(is_assignable_to(Intersection[Literal[1], Any], Intersection[Unrelated, Not[Any]])) + +static_assert(is_assignable_to(Intersection[Unrelated, Not[int]], Not[int])) +static_assert(is_assignable_to(Intersection[Intersection[str, Not[Literal[""]]], int], Intersection[str, Not[Literal[""]]])) +static_assert(is_assignable_to(Intersection[Intersection[Any, Not[int]], Not[str]], Intersection[Any, Not[int]])) + +# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` +static_assert(is_assignable_to(Intersection[LiteralString, AlwaysTruthy], AlwaysTruthy)) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) +static_assert(not is_assignable_to(Intersection[object, Not[Literal[""]]], AlwaysTruthy)) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])) +# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` +static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysTruthy]], Not[AlwaysTruthy])) +static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], Not[AlwaysTruthy])) +static_assert(not is_assignable_to(Intersection[LiteralString, Literal["", "a"]], Not[AlwaysTruthy])) +static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""])) +static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], Literal[""])) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` +static_assert(is_assignable_to(Intersection[bool, Not[AlwaysTruthy]], Literal[False])) +static_assert(is_assignable_to(Intersection[bool, Not[Literal[True]]], Literal[False])) + +# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]` +static_assert(is_assignable_to(Intersection[LiteralString, AlwaysFalsy], AlwaysFalsy)) +static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], AlwaysFalsy)) +static_assert(not is_assignable_to(Intersection[LiteralString, Literal["", "a"]], AlwaysFalsy)) +static_assert(is_assignable_to(Intersection[LiteralString, AlwaysFalsy], Literal[""])) +# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` +static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysFalsy]], Not[AlwaysFalsy])) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy])) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_assignable_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) +static_assert(is_assignable_to(Intersection[bool, Not[Literal[False]]], Literal[True])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_assignable_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) +static_assert(is_assignable_to(Intersection[bool, Not[Literal[False]]], Literal[True])) + +static_assert(is_assignable_to(Intersection[bool, Literal[False] | AlwaysTruthy], Literal[False] | AlwaysTruthy)) +static_assert( + is_assignable_to( + Intersection[Intersection[AlwaysFalsy, Not[Literal[False]]], bool], Intersection[AlwaysFalsy, Not[Literal[False]]] + ) +) ``` ## General properties 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 d88100e8b496d..7b9ec4db50f91 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 @@ -26,7 +26,7 @@ static_assert(not is_disjoint_from(str, type[Any])) ## Class hierarchies ```py -from knot_extensions import is_disjoint_from, static_assert, Intersection, is_subtype_of +from knot_extensions import Intersection, Not, is_disjoint_from, static_assert, is_subtype_of from typing import final class A: ... @@ -55,6 +55,10 @@ static_assert(not is_disjoint_from(FinalSubclass, A)) # ... which makes it disjoint from B1, B2: static_assert(is_disjoint_from(B1, FinalSubclass)) static_assert(is_disjoint_from(B2, FinalSubclass)) + +static_assert(is_disjoint_from(B1, Not[B1])) +static_assert(is_disjoint_from(C, Intersection[A, Not[B1]])) +static_assert(is_disjoint_from(Intersection[A, Not[B1]], C)) ``` ## Tuple types @@ -171,7 +175,7 @@ static_assert(not is_disjoint_from(None, object)) ```py from typing_extensions import Literal, LiteralString -from knot_extensions import TypeOf, is_disjoint_from, static_assert +from knot_extensions import Intersection, Not, TypeOf, is_disjoint_from, static_assert static_assert(is_disjoint_from(Literal[True], Literal[False])) static_assert(is_disjoint_from(Literal[True], Literal[1])) @@ -198,6 +202,10 @@ static_assert(not is_disjoint_from(Literal[1], Literal[1])) static_assert(not is_disjoint_from(Literal["a"], Literal["a"])) static_assert(not is_disjoint_from(Literal["a"], LiteralString)) static_assert(not is_disjoint_from(Literal["a"], str)) + +static_assert(is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["a"])) +static_assert(is_disjoint_from(Intersection[str, Not[Literal["a", "b"]]], Literal["a"])) +static_assert(not is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["b"])) ``` ### Class, module and function literals diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md index 5dab6ebeab6a2..f91740b40717d 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md @@ -42,9 +42,9 @@ static_assert(is_gradual_equivalent_to(str | int, int | str)) static_assert( is_gradual_equivalent_to(Intersection[str, int, Not[bytes], Not[None]], Intersection[int, str, Not[None], Not[bytes]]) ) -# TODO: `~type[Any]` shoudld be gradually equivalent to `~type[Unknown]` -# error: [static-assert-error] static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]], Intersection[int | str, Not[type[Unknown]]])) +static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any)) +static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any])) static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes)) static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict)) diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md index 3998c0a0f11b2..cbaae9857eb64 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md @@ -276,8 +276,9 @@ static_assert(is_subtype_of(Never, AlwaysFalsy)) ### `AlwaysTruthy` and `AlwaysFalsy` ```py -from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert +from knot_extensions import AlwaysTruthy, AlwaysFalsy, Intersection, Not, is_subtype_of, static_assert from typing import Literal +from typing_extensions import LiteralString static_assert(is_subtype_of(Literal[1], AlwaysTruthy)) static_assert(is_subtype_of(Literal[0], AlwaysFalsy)) @@ -290,6 +291,42 @@ static_assert(not is_subtype_of(Literal[0], AlwaysTruthy)) static_assert(not is_subtype_of(str, AlwaysTruthy)) static_assert(not is_subtype_of(str, AlwaysFalsy)) + +static_assert(is_subtype_of(bool, Literal[False] | AlwaysTruthy)) +static_assert(is_subtype_of(bool, Literal[True] | AlwaysFalsy)) +static_assert(not is_subtype_of(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy)) +static_assert(is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy)) + +# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` +static_assert(is_subtype_of(Intersection[LiteralString, AlwaysTruthy], AlwaysTruthy)) +static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)) +static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) +static_assert(not is_subtype_of(Intersection[object, Not[Literal[""]]], AlwaysTruthy)) +# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` +static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysTruthy]], Not[AlwaysTruthy])) +static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], Not[AlwaysTruthy])) +static_assert(not is_subtype_of(Intersection[LiteralString, Literal["", "a"]], Not[AlwaysTruthy])) +static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""])) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` +static_assert(is_subtype_of(Intersection[bool, Not[AlwaysTruthy]], Literal[False])) +static_assert(is_subtype_of(Intersection[bool, Not[Literal[True]]], Literal[False])) + +# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]` +static_assert(is_subtype_of(Intersection[LiteralString, AlwaysFalsy], AlwaysFalsy)) +static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], AlwaysFalsy)) +static_assert(not is_subtype_of(Intersection[LiteralString, Literal["", "a"]], AlwaysFalsy)) +static_assert(is_subtype_of(Intersection[LiteralString, AlwaysFalsy], Literal[""])) +static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], Literal[""])) +# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` +static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysFalsy]], Not[AlwaysFalsy])) +static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy])) +static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_subtype_of(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) +static_assert(is_subtype_of(Intersection[bool, Not[Literal[False]]], Literal[True])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_subtype_of(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) +static_assert(is_subtype_of(Intersection[bool, Not[Literal[False]]], Literal[True])) ``` ### Module literals diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 811c35aa6e6ae..8b53027a749ae 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -300,6 +300,10 @@ impl<'db> Type<'db> { KnownClass::Object.to_instance(db) } + pub const fn is_dynamic(&self) -> bool { + matches!(self, Type::Dynamic(..)) + } + pub const fn is_unknown(&self) -> bool { matches!(self, Type::Dynamic(DynamicType::Unknown)) } @@ -567,10 +571,41 @@ impl<'db> Type<'db> { .iter() .all(|&elem_ty| elem_ty.is_subtype_of(db, target)), - (_, Type::Union(union)) => union - .elements(db) - .iter() - .any(|&elem_ty| self.is_subtype_of(db, elem_ty)), + (_, Type::Union(union)) => { + // Special handlings + // `is_subtype_of(bool, Literal[False] | AlwaysTruthy)` + if self.is_subtype_of(db, KnownClass::Bool.to_instance(db)) { + if union + .elements(db) + .iter() + .any(|elem| Type::BooleanLiteral(true).is_subtype_of(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::BooleanLiteral(false).is_subtype_of(db, *elem)) + { + return true; + } + } + // `is_subtype_of(StringLiteral, Literal[""] | AlwaysTruthy)` + else if self.is_subtype_of(db, Type::LiteralString) { + if union + .elements(db) + .iter() + .any(|elem| Type::string_literal(db, "").is_subtype_of(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::AlwaysTruthy.is_subtype_of(db, *elem)) + { + return true; + } + } + union + .elements(db) + .iter() + .any(|&elem_ty| self.is_subtype_of(db, elem_ty)) + } // `object` is the only type that can be known to be a supertype of any intersection, // even an intersection with no positive elements @@ -581,6 +616,50 @@ impl<'db> Type<'db> { } (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { + // Special handlings + // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` + if target_intersection + .positive(db) + .contains(&Type::AlwaysTruthy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysFalsy) + { + // For example: + // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` + // `not is_subtype_of(Intersection[object, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` + if self_intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) + && self_intersection + .negative(db) + .iter() + .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + { + return true; + } + } + // `LiteralString & AlwaysFalsy`, `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` + else if target_intersection + .positive(db) + .contains(&Type::AlwaysFalsy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysTruthy) + { + if self_intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) + && self_intersection + .positive(db) + .iter() + .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + { + return true; + } + } // Check that all target positive values are covered in self positive values target_intersection .positive(db) @@ -607,10 +686,42 @@ impl<'db> Type<'db> { }) } - (Type::Intersection(intersection), _) => intersection - .positive(db) - .iter() - .any(|&elem_ty| elem_ty.is_subtype_of(db, target)), + (Type::Intersection(intersection), _) => { + // Special handlings + // For example: + // `is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)` + if target.is_equivalent_to(db, Type::AlwaysTruthy) { + if intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) + && intersection + .negative(db) + .iter() + .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + { + return true; + } + } + // `is_subtype_of(Intersection[LiteralString, Literal[""]], AlwaysFalsy)` + else if target.is_equivalent_to(db, Type::AlwaysFalsy) { + if intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) + && intersection + .positive(db) + .iter() + .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + { + return true; + } + } + intersection + .positive(db) + .iter() + .any(|&elem_ty| elem_ty.is_subtype_of(db, target)) + } (_, Type::Intersection(intersection)) => { intersection @@ -797,10 +908,149 @@ impl<'db> Type<'db> { .all(|&elem_ty| elem_ty.is_assignable_to(db, ty)), // A type T is assignable to a union iff T is assignable to any element of the union. - (ty, Type::Union(union)) => union - .elements(db) - .iter() - .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)), + (ty, Type::Union(union)) => { + // Special handlings + // `is_assignable_to(bool, Literal[False] | AlwaysTruthy)` + if self.is_assignable_to(db, KnownClass::Bool.to_instance(db)) { + if union + .elements(db) + .iter() + .any(|elem| Type::BooleanLiteral(true).is_assignable_to(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::BooleanLiteral(false).is_assignable_to(db, *elem)) + { + return true; + } + } + // `is_assignable_to(StringLiteral, Literal[""] | AlwaysTruthy)` + else if self.is_assignable_to(db, Type::LiteralString) { + if union + .elements(db) + .iter() + .any(|elem| Type::string_literal(db, "").is_assignable_to(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::AlwaysTruthy.is_assignable_to(db, *elem)) + { + return true; + } + } + union + .elements(db) + .iter() + .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)) + } + + (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { + // Special handlings + // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` + if target_intersection + .positive(db) + .contains(&Type::AlwaysTruthy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysFalsy) + { + // For example: + // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` + // `not is_assignable_to(Intersection[object, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` + if self_intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) + && self_intersection.negative(db).iter().any(|neg_ty| { + Type::string_literal(db, "").is_assignable_to(db, *neg_ty) + }) + { + return true; + } + } + // `LiteralString & AlwaysFalsy`, `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` + else if target_intersection + .positive(db) + .contains(&Type::AlwaysFalsy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysTruthy) + { + if self_intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) + && self_intersection.positive(db).iter().any(|neg_ty| { + Type::string_literal(db, "").is_assignable_to(db, *neg_ty) + }) + { + return true; + } + } + // 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_assignable_to(db, target_pos_elem)) + }) + // Check that all target negative values are excluded in self, either by being + // assignable to 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 assignable to a self negative value + self_intersection.negative(db).iter().any(|&self_neg_elem| { + target_neg_elem.is_assignable_to(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) + }) + }) + } + + // An intersection type S is assignable to a type T if + // Any element of S is assignable to T (e.g. `A & B` is assignable to `A`) + // Negative elements do not have an effect on assignability - if S is assignable to T then S & ~P is also assignable to T. + (Type::Intersection(intersection), ty) => { + // Special handlings + // For example: + // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)` + // `not is_assignable_to(Intersection[object, Not[Literal[""]]], AlwaysTruthy)` + if target.is_gradual_equivalent_to(db, Type::AlwaysTruthy) { + if intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) + && intersection.negative(db).iter().any(|neg_ty| { + Type::string_literal(db, "").is_assignable_to(db, *neg_ty) + }) + { + return true; + } + } + // `is_assignable_to(Intersection[LiteralString, Literal[""]], AlwaysFalsy)` + else if target.is_gradual_equivalent_to(db, Type::AlwaysFalsy) { + if intersection + .positive(db) + .iter() + .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) + && intersection.positive(db).iter().any(|neg_ty| { + Type::string_literal(db, "").is_assignable_to(db, *neg_ty) + }) + { + return true; + } + } + intersection + .positive(db) + .iter() + .any(|elem_ty| elem_ty.is_assignable_to(db, ty)) + } // 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 @@ -816,14 +1066,6 @@ impl<'db> Type<'db> { .all(|&neg_ty| ty.is_disjoint_from(db, neg_ty)) } - // An intersection type S is assignable to a type T if - // Any element of S is assignable to T (e.g. `A & B` is assignable to `A`) - // Negative elements do not have an effect on assignability - if S is assignable to T then S & ~P is also assignable to T. - (Type::Intersection(intersection), ty) => intersection - .positive(db) - .iter() - .any(|&elem_ty| elem_ty.is_assignable_to(db, ty)), - // A tuple type S is assignable to a tuple type T if their lengths are the same, and // each element of S is assignable to the corresponding element of T. (Type::Tuple(self_tuple), Type::Tuple(target_tuple)) => { @@ -974,10 +1216,20 @@ impl<'db> Type<'db> { (Type::Tuple(first), Type::Tuple(second)) => first.is_gradual_equivalent_to(db, second), (Type::Union(first), Type::Union(second)) => first.is_gradual_equivalent_to(db, second), + (Type::Union(union), other) | (other, Type::Union(union)) => { + let normalized = union.reduce_dynamic_types(db); + normalized != Type::Union(union) && normalized.is_gradual_equivalent_to(db, other) + } (Type::Intersection(first), Type::Intersection(second)) => { first.is_gradual_equivalent_to(db, second) } + (Type::Intersection(intersection), other) + | (other, Type::Intersection(intersection)) => { + let normalized = intersection.reduce_dynamic_types(db); + normalized != Type::Intersection(intersection) + && normalized.is_gradual_equivalent_to(db, other) + } _ => false, } @@ -1000,17 +1252,16 @@ 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 - } + // is_disjoint_from(T, X & ~S) if T <: S + // since `T & ~S` is Never + || intersection + .negative(db) + .iter() + .any(|n| other.is_subtype_of(db, *n)) } // any single-valued type is disjoint from another single-valued type @@ -3256,6 +3507,20 @@ impl<'db> Type<'db> { _ => KnownClass::Str.to_instance(db), } } + + /// Reduce dynamic types in the type. + /// For example: + /// `T | Any | Unknown -> T | Any` + /// `T & Any & Unknown -> T & Any` + /// + /// This method is used to evaluate whether two types are gradually equal. + fn reduce_dynamic_types(&self, db: &'db dyn Db) -> Self { + match self { + Type::Union(union) => union.reduce_dynamic_types(db), + Type::Intersection(intersection) => intersection.reduce_dynamic_types(db), + _ => *self, + } + } } impl<'db> From<&Type<'db>> for Type<'db> { @@ -4592,6 +4857,26 @@ impl<'db> UnionType<'db> { self.elements_boxed(db) } + /// Reduce dynamic types in the union. + /// For example: + /// `int | str | Any | Unknown -> int | str | Any` + /// `Any | Unknown -> Any` + fn reduce_dynamic_types(self, db: &'db dyn Db) -> Type<'db> { + let mut builder = UnionBuilder::new(db); + + let mut dynamic_found = false; + for ty in self.elements(db) { + if !ty.is_dynamic() { + builder = builder.add(ty.reduce_dynamic_types(db)); + } else if !dynamic_found { + builder = builder.add(*ty); + dynamic_found = true; + } + } + + builder.build() + } + /// Create a union from a list of elements /// (which may be eagerly simplified into a different variant of [`Type`] altogether). pub fn from_elements(db: &'db dyn Db, elements: I) -> Type<'db> @@ -4716,7 +5001,7 @@ impl<'db> UnionType<'db> { .iter() .map(|element| element.with_sorted_unions(db)) .collect(); - new_elements.sort_unstable_by(union_elements_ordering); + new_elements.sort_unstable_by(|l, r| union_elements_ordering(l, r, db)); UnionType::new(db, new_elements.into_boxed_slice()) } @@ -4764,14 +5049,24 @@ impl<'db> UnionType<'db> { return true; } - // TODO: `T | Unknown` should be gradually equivalent to `T | Unknown | Any`, - // since they have exactly the same set of possible static materializations - // (they represent the same set of possible sets of possible runtime objects) - if self.elements(db).len() != other.elements(db).len() { + let (self_, other) = match ( + self.reduce_dynamic_types(db), + other.reduce_dynamic_types(db), + ) { + (Type::Union(self_), Type::Union(other)) => (self_, other), + (Type::Union(_), _) | (_, Type::Union(_)) => { + return false; + } + (self_, other) => { + return self_.is_gradual_equivalent_to(db, other); + } + }; + + if self_.elements(db).len() != other.elements(db).len() { return false; } - let sorted_self = self.to_sorted_union(db); + let sorted_self = self_.to_sorted_union(db); if sorted_self == other { return true; @@ -4820,7 +5115,7 @@ impl<'db> IntersectionType<'db> { .map(|ty| ty.with_sorted_unions(db)) .collect(); - elements.sort_unstable_by(union_elements_ordering); + elements.sort_unstable_by(|l, r| union_elements_ordering(l, r, db)); elements } @@ -4836,6 +5131,36 @@ impl<'db> IntersectionType<'db> { && self.negative(db).iter().all(|ty| ty.is_fully_static(db)) } + /// Reduce dynamic types in the intersection. + /// For example: + /// `int & str & Any & Unknown -> int & str & Any` + /// `Any & Unknown -> Any` + fn reduce_dynamic_types(self, db: &'db dyn Db) -> Type<'db> { + let mut builder = IntersectionBuilder::new(db); + + let mut dynamic_found = false; + for ty in self.positive(db) { + if !ty.is_dynamic() { + builder = builder.add_positive(ty.reduce_dynamic_types(db)); + } else if !dynamic_found { + builder = builder.add_positive(*ty); + dynamic_found = true; + } + } + + let mut dynamic_found = false; + for ty in self.negative(db) { + if !ty.is_dynamic() { + builder = builder.add_negative(ty.reduce_dynamic_types(db)); + } else if !dynamic_found { + builder = builder.add_negative(*ty); + dynamic_found = true; + } + } + + builder.build() + } + /// Return `true` if `self` represents exactly the same set of possible runtime objects as `other` pub fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool { /// Inlined version of [`IntersectionType::is_fully_static`] to avoid having to lookup @@ -4897,13 +5222,26 @@ impl<'db> IntersectionType<'db> { return true; } - if self.positive(db).len() != other.positive(db).len() - || self.negative(db).len() != other.negative(db).len() + let (self_, other) = match ( + self.reduce_dynamic_types(db), + other.reduce_dynamic_types(db), + ) { + (Type::Intersection(self_), Type::Intersection(other)) => (self_, other), + (Type::Intersection(_), _) | (_, Type::Intersection(_)) => { + return false; + } + (self_, other) => { + return self_.is_gradual_equivalent_to(db, other); + } + }; + + if self_.positive(db).len() != other.positive(db).len() + || self_.negative(db).len() != other.negative(db).len() { return false; } - let sorted_self = self.to_sorted_intersection(db); + let sorted_self = self_.to_sorted_intersection(db); if sorted_self == other { return true; diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs index c8b8dc133d1e5..c7f07a66f67ca 100644 --- a/crates/red_knot_python_semantic/src/types/builder.rs +++ b/crates/red_knot_python_semantic/src/types/builder.rs @@ -349,15 +349,27 @@ impl<'db> InnerIntersectionBuilder<'db> { // `bool & ~Literal[False]` -> `Literal[True]` // `bool & ~Literal[True]` -> `Literal[False]` Type::BooleanLiteral(bool_value) => { - new_positive = Type::BooleanLiteral(!bool_value); + if new_positive == Type::BooleanLiteral(*bool_value) { + new_positive = Type::Never; + } else { + new_positive = Type::BooleanLiteral(!bool_value); + } } // `bool & ~AlwaysTruthy` -> `Literal[False]` Type::AlwaysTruthy => { - new_positive = Type::BooleanLiteral(false); + if new_positive == Type::BooleanLiteral(true) { + new_positive = Type::Never; + } else { + new_positive = Type::BooleanLiteral(false); + } } // `bool & ~AlwaysFalsy` -> `Literal[True]` Type::AlwaysFalsy => { - new_positive = Type::BooleanLiteral(true); + if new_positive == Type::BooleanLiteral(false) { + new_positive = Type::Never; + } else { + new_positive = Type::BooleanLiteral(true); + } } _ => continue, } diff --git a/crates/red_knot_python_semantic/src/types/property_tests.rs b/crates/red_knot_python_semantic/src/types/property_tests.rs index b76549029c296..1b8d388600848 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -557,7 +557,6 @@ mod flaky { // And for non-fully-static types, the intersection of a pair of types // should be assignable to both types of the pair. - // Currently fails due to https://github.com/astral-sh/ruff/issues/14899 type_property_test!( all_type_pairs_can_be_assigned_from_their_intersection, db, forall types s, t. intersection(db, [s, t]).is_assignable_to(db, s) && intersection(db, [s, t]).is_assignable_to(db, t) diff --git a/crates/red_knot_python_semantic/src/types/type_ordering.rs b/crates/red_knot_python_semantic/src/types/type_ordering.rs index 6de486031f05d..bcf9eeedb106f 100644 --- a/crates/red_knot_python_semantic/src/types/type_ordering.rs +++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs @@ -11,8 +11,9 @@ use super::{ /// in an [`crate::types::IntersectionType`] or a [`crate::types::UnionType`] in order for them /// to be compared for equivalence. /// -/// Two unions with equal sets of elements will only compare equal if they have their element sets -/// ordered the same way. +/// Two unions / intersections are compared lexicographically. +/// +/// Element types must already be sorted. /// /// ## Why not just implement [`Ord`] on [`Type`]? /// @@ -20,7 +21,11 @@ use super::{ /// create here is not user-facing. However, it doesn't really "make sense" for `Type` to implement /// [`Ord`] in terms of the semantics. There are many different ways in which you could plausibly /// sort a list of types; this is only one (somewhat arbitrary, at times) possible ordering. -pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'db>) -> Ordering { +pub(super) fn union_elements_ordering<'db>( + left: &Type<'db>, + right: &Type<'db>, + db: &'db dyn crate::Db, +) -> Ordering { if left == right { return Ordering::Equal; } @@ -261,11 +266,38 @@ pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'db>) (Type::Dynamic(_), _) => Ordering::Less, (_, Type::Dynamic(_)) => Ordering::Greater, - (Type::Union(left), Type::Union(right)) => left.cmp(right), + (Type::Union(left), Type::Union(right)) => { + // Lexicographically compare the elements of the two unions. + for (left, right) in left.elements(db).iter().zip(right.elements(db)) { + let ordering = union_elements_ordering(left, right, db); + if ordering != Ordering::Equal { + return ordering; + } + } + left.elements(db).len().cmp(&right.elements(db).len()) + } (Type::Union(_), _) => Ordering::Less, (_, Type::Union(_)) => Ordering::Greater, - (Type::Intersection(left), Type::Intersection(right)) => left.cmp(right), + (Type::Intersection(left), Type::Intersection(right)) => { + // Lexicographically compare the elements of the two intersections. + for (left, right) in left.positive(db).iter().zip(right.positive(db)) { + let ordering = union_elements_ordering(left, right, db); + if ordering != Ordering::Equal { + return ordering; + } + } + if left.positive(db).len() != right.positive(db).len() { + return left.positive(db).len().cmp(&right.positive(db).len()); + } + for (left, right) in left.negative(db).iter().zip(right.negative(db)) { + let ordering = union_elements_ordering(left, right, db); + if ordering != Ordering::Equal { + return ordering; + } + } + left.negative(db).len().cmp(&right.negative(db).len()) + } } } From a089eb98c50dda8d193cbe70cdef31a03f6d1fc5 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Sat, 15 Mar 2025 03:08:04 +0900 Subject: [PATCH 2/3] fix `is_subtype_of/is_assignable_to` handling & organize test cases --- .../type_properties/is_assignable_to.md | 45 +-- .../type_properties/is_disjoint_from.md | 27 +- .../type_properties/is_equivalent_to.md | 22 ++ .../mdtest/type_properties/is_subtype_of.md | 39 +-- crates/red_knot_python_semantic/src/types.rs | 312 +++++++++++++----- .../src/types/type_ordering.rs | 16 +- 6 files changed, 312 insertions(+), 149 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 a4f4f4e3c25c5..d3c44f6c00002 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 @@ -306,44 +306,25 @@ static_assert(is_assignable_to(Intersection[Unrelated, Not[int]], Not[int])) static_assert(is_assignable_to(Intersection[Intersection[str, Not[Literal[""]]], int], Intersection[str, Not[Literal[""]]])) static_assert(is_assignable_to(Intersection[Intersection[Any, Not[int]], Not[str]], Intersection[Any, Not[int]])) +# The condition `is_assignable_to(T & U, U)` should still be satisfied after the following transformations: # `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` -static_assert(is_assignable_to(Intersection[LiteralString, AlwaysTruthy], AlwaysTruthy)) static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)) static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) -static_assert(not is_assignable_to(Intersection[object, Not[Literal[""]]], AlwaysTruthy)) -static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])) -# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` -static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysTruthy]], Not[AlwaysTruthy])) -static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], Not[AlwaysTruthy])) -static_assert(not is_assignable_to(Intersection[LiteralString, Literal["", "a"]], Not[AlwaysTruthy])) -static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""])) -static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], Literal[""])) -# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` -static_assert(is_assignable_to(Intersection[bool, Not[AlwaysTruthy]], Literal[False])) -static_assert(is_assignable_to(Intersection[bool, Not[Literal[True]]], Literal[False])) - -# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]` -static_assert(is_assignable_to(Intersection[LiteralString, AlwaysFalsy], AlwaysFalsy)) -static_assert(is_assignable_to(Intersection[LiteralString, Literal[""]], AlwaysFalsy)) -static_assert(not is_assignable_to(Intersection[LiteralString, Literal["", "a"]], AlwaysFalsy)) -static_assert(is_assignable_to(Intersection[LiteralString, AlwaysFalsy], Literal[""])) +# `LiteralString & ~AlwaysTruthy` -> `Literal[""]` +static_assert(is_assignable_to(Literal[""], Not[AlwaysTruthy])) +static_assert(not is_assignable_to(Literal["", "a"], Not[AlwaysTruthy])) +# `LiteralString & AlwaysFalsy` -> `Literal[""]` +static_assert(is_assignable_to(Literal[""], AlwaysFalsy)) +static_assert(not is_assignable_to(Literal["", "a"], AlwaysFalsy)) # `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` -static_assert(is_assignable_to(Intersection[LiteralString, Not[AlwaysFalsy]], Not[AlwaysFalsy])) static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy])) static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy])) -# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` -static_assert(is_assignable_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) -static_assert(is_assignable_to(Intersection[bool, Not[Literal[False]]], Literal[True])) -# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` -static_assert(is_assignable_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) -static_assert(is_assignable_to(Intersection[bool, Not[Literal[False]]], Literal[True])) - -static_assert(is_assignable_to(Intersection[bool, Literal[False] | AlwaysTruthy], Literal[False] | AlwaysTruthy)) -static_assert( - is_assignable_to( - Intersection[Intersection[AlwaysFalsy, Not[Literal[False]]], bool], Intersection[AlwaysFalsy, Not[Literal[False]]] - ) -) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `Literal[False]` +static_assert(is_assignable_to(Literal[False], Not[AlwaysTruthy])) +static_assert(is_assignable_to(Literal[False], Not[Literal[True]])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `Literal[True]` +static_assert(is_assignable_to(Literal[True], Not[AlwaysFalsy])) +static_assert(is_assignable_to(Literal[True], Not[Literal[False]])) ``` ## General properties 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 042757bceb907..9fe632f5ed593 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 @@ -200,7 +200,7 @@ static_assert(is_disjoint_from(None, Intersection[int, Not[str]])) ```py from typing_extensions import Literal, LiteralString -from knot_extensions import Intersection, Not, TypeOf, is_disjoint_from, static_assert +from knot_extensions import Intersection, Not, TypeOf, is_disjoint_from, static_assert, AlwaysFalsy, AlwaysTruthy static_assert(is_disjoint_from(Literal[True], Literal[False])) static_assert(is_disjoint_from(Literal[True], Literal[1])) @@ -231,6 +231,31 @@ static_assert(not is_disjoint_from(Literal["a"], str)) static_assert(is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["a"])) static_assert(is_disjoint_from(Intersection[str, Not[Literal["a", "b"]]], Literal["a"])) static_assert(not is_disjoint_from(Intersection[str, Not[Literal["a"]]], Literal["b"])) + +static_assert(is_disjoint_from(AlwaysFalsy, Intersection[LiteralString, Not[Literal[""]]])) +static_assert(is_disjoint_from(AlwaysTruthy, Literal[""])) + +static_assert(is_disjoint_from(Intersection[Not[Literal[True]], Not[Literal[False]]], bool)) +static_assert(is_disjoint_from(Intersection[AlwaysFalsy, Not[Literal[False]]], bool)) +static_assert(is_disjoint_from(Intersection[AlwaysTruthy, Not[Literal[True]]], bool)) +static_assert(is_disjoint_from(Intersection[Literal[True], Not[AlwaysTruthy]], bool)) +static_assert(is_disjoint_from(Intersection[Literal[False], Not[AlwaysFalsy]], bool)) + +# The condition `is_disjoint(T, Not[T])` must still be satisfied after the following transformations: +# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` +static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysTruthy], Not[LiteralString] | AlwaysFalsy)) +# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` +static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysTruthy]], Not[LiteralString] | AlwaysTruthy)) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` +static_assert(is_disjoint_from(Intersection[bool, Not[AlwaysTruthy]], Not[bool] | AlwaysTruthy)) +static_assert(is_disjoint_from(Intersection[bool, Not[Literal[True]]], Not[bool] | Literal[True])) +# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]` +static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysFalsy], Not[LiteralString] | AlwaysTruthy)) +# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` +static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysFalsy]], Not[LiteralString] | AlwaysFalsy)) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_disjoint_from(Intersection[bool, Not[AlwaysFalsy]], Not[bool] | AlwaysFalsy)) +static_assert(is_disjoint_from(Intersection[bool, Not[Literal[False]]], Not[bool] | Literal[False])) ``` ### Class, module and function literals diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md index 047a45fc2fd0b..fa45a92cc8f04 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md @@ -118,4 +118,26 @@ class R: ... static_assert(is_equivalent_to(Intersection[tuple[P | Q], R], Intersection[tuple[Q | P], R])) ``` +## Transformation by intersection + +```py +from knot_extensions import Intersection, Not, AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to +from typing_extensions import Literal, LiteralString + +# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` +static_assert(is_equivalent_to(Intersection[LiteralString, AlwaysTruthy], Intersection[LiteralString, Not[Literal[""]]])) +# `LiteralString & ~AlwaysTruthy` -> `Literal[""]` +static_assert(is_equivalent_to(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""])) +# `LiteralString & AlwaysFalsy` -> `Literal[""]` +static_assert(is_equivalent_to(Intersection[LiteralString, AlwaysFalsy], Literal[""])) +# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` +static_assert(is_equivalent_to(Intersection[LiteralString, Not[AlwaysFalsy]], Intersection[LiteralString, Not[Literal[""]]])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` +static_assert(is_equivalent_to(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) +static_assert(is_equivalent_to(Intersection[bool, Not[Literal[False]]], Literal[True])) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` +static_assert(is_equivalent_to(Intersection[bool, Not[AlwaysTruthy]], Literal[False])) +static_assert(is_equivalent_to(Intersection[bool, Not[Literal[True]]], Literal[False])) +``` + [the equivalence relation]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md index cbaae9857eb64..4ba2a4f2d728b 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md @@ -297,36 +297,25 @@ static_assert(is_subtype_of(bool, Literal[True] | AlwaysFalsy)) static_assert(not is_subtype_of(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy)) static_assert(is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy)) +# The condition `is_subtype_of(T & U, U)` must still be satisfied after the following transformations: # `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` -static_assert(is_subtype_of(Intersection[LiteralString, AlwaysTruthy], AlwaysTruthy)) static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)) static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) -static_assert(not is_subtype_of(Intersection[object, Not[Literal[""]]], AlwaysTruthy)) -# `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` -static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysTruthy]], Not[AlwaysTruthy])) -static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], Not[AlwaysTruthy])) -static_assert(not is_subtype_of(Intersection[LiteralString, Literal["", "a"]], Not[AlwaysTruthy])) -static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysTruthy]], Literal[""])) -# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `bool & Literal[False]` -static_assert(is_subtype_of(Intersection[bool, Not[AlwaysTruthy]], Literal[False])) -static_assert(is_subtype_of(Intersection[bool, Not[Literal[True]]], Literal[False])) - -# `LiteralString & AlwaysFalsy` -> `LiteralString & Literal[""]` -static_assert(is_subtype_of(Intersection[LiteralString, AlwaysFalsy], AlwaysFalsy)) -static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], AlwaysFalsy)) -static_assert(not is_subtype_of(Intersection[LiteralString, Literal["", "a"]], AlwaysFalsy)) -static_assert(is_subtype_of(Intersection[LiteralString, AlwaysFalsy], Literal[""])) -static_assert(is_subtype_of(Intersection[LiteralString, Literal[""]], Literal[""])) -# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` -static_assert(is_subtype_of(Intersection[LiteralString, Not[AlwaysFalsy]], Not[AlwaysFalsy])) +# `LiteralString & ~AlwaysTruthy` -> `Literal[""]` +static_assert(is_subtype_of(Literal[""], Not[AlwaysTruthy])) +static_assert(not is_subtype_of(Literal["", "a"], Not[AlwaysTruthy])) +# `LiteralString & AlwaysFalsy` -> `Literal[""]` +static_assert(is_subtype_of(Literal[""], AlwaysFalsy)) +static_assert(not is_subtype_of(Literal["", "a"], AlwaysFalsy)) +# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy])) static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy])) -# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` -static_assert(is_subtype_of(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) -static_assert(is_subtype_of(Intersection[bool, Not[Literal[False]]], Literal[True])) -# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `bool & Literal[True]` -static_assert(is_subtype_of(Intersection[bool, Not[AlwaysFalsy]], Literal[True])) -static_assert(is_subtype_of(Intersection[bool, Not[Literal[False]]], Literal[True])) +# `bool & ~AlwaysTruthy`, `bool & ~Literal[True]` -> `Literal[False]` +static_assert(is_subtype_of(Literal[False], Not[AlwaysTruthy])) +static_assert(is_subtype_of(Literal[False], Not[Literal[True]])) +# `bool & ~AlwaysFalsy`, `bool & ~Literal[False]` -> `Literal[True]` +static_assert(is_subtype_of(Literal[True], Not[AlwaysFalsy])) +static_assert(is_subtype_of(Literal[True], Not[Literal[False]])) ``` ### Module literals diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 6baec813546ef..f353a753971f9 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -587,7 +587,7 @@ impl<'db> Type<'db> { return true; } } - // `is_subtype_of(StringLiteral, Literal[""] | AlwaysTruthy)` + // `is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy)` else if self.is_subtype_of(db, Type::LiteralString) { if union .elements(db) @@ -601,6 +601,22 @@ impl<'db> Type<'db> { return true; } } + // `is_subtype_of(AlwaysFalsy, Not[LiteralString] | Literal[""])` + else if self.is_subtype_of(db, Type::AlwaysFalsy) + || self.is_subtype_of(db, Type::AlwaysTruthy.negate(db)) + { + if union + .elements(db) + .iter() + .any(|elem| Type::string_literal(db, "").is_subtype_of(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::LiteralString.negate(db).is_subtype_of(db, *elem)) + { + return true; + } + } union .elements(db) .iter() @@ -617,45 +633,84 @@ impl<'db> Type<'db> { (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { // Special handlings - // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` - if target_intersection - .positive(db) - .contains(&Type::AlwaysTruthy) - || target_intersection + // `is_subtype_of(Not[Literal[False] | AlwaysTruthy], Not[bool])` + if self_intersection + .negative(db) + .iter() + .any(|neg_ty| Type::BooleanLiteral(false).is_subtype_of(db, *neg_ty)) + && self_intersection .negative(db) - .contains(&Type::AlwaysFalsy) + .iter() + .any(|neg_ty| Type::BooleanLiteral(true).is_subtype_of(db, *neg_ty)) + && target.is_equivalent_to(db, KnownClass::Bool.to_instance(db).negate(db)) { + return true; + } + // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` + // `LiteralString` is `AlwaysTruthy` except for `Literal[""]` + else if self_intersection.is_non_empty_literal_string(db) { + let mut target_positive = target_intersection.positive(db).clone(); // For example: // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` // `not is_subtype_of(Intersection[object, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` - if self_intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) - && self_intersection + // `not is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, tuple])` + if (target_positive.remove(&Type::AlwaysTruthy) + || target_intersection .negative(db) + .contains(&Type::AlwaysFalsy)) + && target_positive .iter() - .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + .all(|pos_ty| Type::LiteralString.is_subtype_of(db, *pos_ty)) { return true; } } // `LiteralString & AlwaysFalsy`, `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` - else if target_intersection - .positive(db) - .contains(&Type::AlwaysFalsy) - || target_intersection + else if self_intersection.is_empty_literal_string(db) { + let mut target_positive = target_intersection.positive(db).clone(); + if (target_positive.remove(&Type::AlwaysFalsy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysTruthy)) + && target_positive + .iter() + .all(|pos_ty| Type::LiteralString.is_subtype_of(db, *pos_ty)) + { + return true; + } + } + // is_subtype_of(~Literal[""] & AlwaysFalsy, ~LiteralString) + // is_subtype_of(~Literal[""] & ~AlwaysTruthy, ~LiteralString) + // is_subtype_of(~Literal[""] & AlwaysFalsy, ~LiteralString & ~Literal[1]) + // not is_subtype_of(~Literal[""] & AlwaysFalsy, ~LiteralString & ~Literal[False]) + else if (self_intersection.negative(db).contains(&Type::AlwaysTruthy) + || self_intersection.positive(db).contains(&Type::AlwaysFalsy)) + && self_intersection + .negative(db) + .contains(&Type::string_literal(db, "")) + && target_intersection + .negative(db) + .contains(&Type::LiteralString) + && target_intersection .negative(db) - .contains(&Type::AlwaysTruthy) - { - if self_intersection - .positive(db) .iter() - .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) - && self_intersection - .positive(db) - .iter() - .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) + .all(|neg_ty| !neg_ty.is_subtype_of(db, Type::AlwaysFalsy)) + { + return true; + } + // is_subtype_of(~AlwaysTruthy & ~AlwaysFalsy, ~tuple[()] & ~LiteralString) + else if self_intersection.negative(db).contains(&Type::AlwaysTruthy) + && self_intersection.negative(db).contains(&Type::AlwaysFalsy) + { + let mut target_negative = target_intersection.negative(db).clone(); + if target_negative.remove(&Type::LiteralString) + && target_negative.iter().all(|&target_neg_elem| { + self_intersection.negative(db).iter().any(|&self_neg_elem| { + target_neg_elem.is_subtype_of(db, self_neg_elem) + }) || self_intersection.positive(db).iter().any(|&self_pos_elem| { + self_pos_elem.is_disjoint_from(db, target_neg_elem) + }) + }) { return true; } @@ -691,29 +746,13 @@ impl<'db> Type<'db> { // For example: // `is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)` if target.is_equivalent_to(db, Type::AlwaysTruthy) { - if intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) - && intersection - .negative(db) - .iter() - .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) - { + if intersection.is_non_empty_literal_string(db) { return true; } } // `is_subtype_of(Intersection[LiteralString, Literal[""]], AlwaysFalsy)` else if target.is_equivalent_to(db, Type::AlwaysFalsy) { - if intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_subtype_of(db, Type::LiteralString)) - && intersection - .positive(db) - .iter() - .any(|neg_ty| Type::string_literal(db, "").is_subtype_of(db, *neg_ty)) - { + if intersection.is_empty_literal_string(db) { return true; } } @@ -935,6 +974,22 @@ impl<'db> Type<'db> { return true; } } + // `is_assignable_to(AlwaysFalsy, Not[LiteralString] | Literal[""])` + else if self.is_assignable_to(db, Type::AlwaysFalsy) + || self.is_assignable_to(db, Type::AlwaysTruthy.negate(db)) + { + if union + .elements(db) + .iter() + .any(|elem| Type::string_literal(db, "").is_assignable_to(db, *elem)) + && union + .elements(db) + .iter() + .any(|elem| Type::LiteralString.negate(db).is_assignable_to(db, *elem)) + { + return true; + } + } union .elements(db) .iter() @@ -943,42 +998,82 @@ impl<'db> Type<'db> { (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { // Special handlings - // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` - if target_intersection - .positive(db) - .contains(&Type::AlwaysTruthy) - || target_intersection + // `is_subtype_of(Not[Literal[False] | AlwaysTruthy], Not[bool])` + if self_intersection + .negative(db) + .iter() + .any(|neg_ty| Type::BooleanLiteral(false).is_assignable_to(db, *neg_ty)) + && self_intersection .negative(db) - .contains(&Type::AlwaysFalsy) + .iter() + .any(|neg_ty| Type::BooleanLiteral(true).is_assignable_to(db, *neg_ty)) + && target.is_equivalent_to(db, KnownClass::Bool.to_instance(db).negate(db)) { + return true; + } + // `LiteralString & AlwaysTruthy`, `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` + // `LiteralString` is `AlwaysTruthy` except for `Literal[""]` + else if self_intersection.is_non_empty_literal_string(db) { + let mut target_positive = target_intersection.positive(db).clone(); // For example: // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` // `not is_assignable_to(Intersection[object, Not[Literal[""]]], Intersection[AlwaysTruthy, Not[Literal[1]]])` - if self_intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) - && self_intersection.negative(db).iter().any(|neg_ty| { - Type::string_literal(db, "").is_assignable_to(db, *neg_ty) - }) + // `not is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Intersection[AlwaysTruthy, tuple])` + if (target_positive.remove(&Type::AlwaysTruthy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysFalsy)) + && target_positive + .iter() + .all(|pos_ty| Type::LiteralString.is_assignable_to(db, *pos_ty)) { return true; } } // `LiteralString & AlwaysFalsy`, `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` - else if target_intersection - .positive(db) - .contains(&Type::AlwaysFalsy) - || target_intersection + else if self_intersection.is_empty_literal_string(db) { + let mut target_positive = target_intersection.positive(db).clone(); + if (target_positive.remove(&Type::AlwaysFalsy) + || target_intersection + .negative(db) + .contains(&Type::AlwaysTruthy)) + && target_positive + .iter() + .all(|pos_ty| Type::LiteralString.is_assignable_to(db, *pos_ty)) + { + return true; + } + } + // is_subtype_of(~Literal[""] & ~AlwaysTruthy, ~LiteralString) + // is_subtype_of(~Literal[""] & AlwaysFalsy, ~LiteralString & ~Literal[1]) + // not is_subtype_of(~Literal[""] & AlwaysFalsy, ~LiteralString & ~Literal[False]) + else if (self_intersection.negative(db).contains(&Type::AlwaysTruthy) + || self_intersection.positive(db).contains(&Type::AlwaysFalsy)) + && self_intersection + .negative(db) + .contains(&Type::string_literal(db, "")) + && target_intersection + .negative(db) + .contains(&Type::LiteralString) + && target_intersection .negative(db) - .contains(&Type::AlwaysTruthy) - { - if self_intersection - .positive(db) .iter() - .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) - && self_intersection.positive(db).iter().any(|neg_ty| { - Type::string_literal(db, "").is_assignable_to(db, *neg_ty) + .all(|neg_ty| !neg_ty.is_assignable_to(db, Type::AlwaysFalsy)) + { + return true; + } + // is_subtype_of(~AlwaysTruthy & ~AlwaysFalsy, ~tuple[()] & ~LiteralString) + else if self_intersection.negative(db).contains(&Type::AlwaysTruthy) + && self_intersection.negative(db).contains(&Type::AlwaysFalsy) + { + let mut target_negative = target_intersection.negative(db).clone(); + if target_negative.remove(&Type::LiteralString) + && target_negative.iter().all(|&target_neg_elem| { + self_intersection.negative(db).iter().any(|&self_neg_elem| { + target_neg_elem.is_assignable_to(db, self_neg_elem) + }) || self_intersection.positive(db).iter().any(|&self_pos_elem| { + self_pos_elem.is_disjoint_from(db, target_neg_elem) + }) }) { return true; @@ -1018,28 +1113,14 @@ impl<'db> Type<'db> { // For example: // `is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)` // `not is_assignable_to(Intersection[object, Not[Literal[""]]], AlwaysTruthy)` - if target.is_gradual_equivalent_to(db, Type::AlwaysTruthy) { - if intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) - && intersection.negative(db).iter().any(|neg_ty| { - Type::string_literal(db, "").is_assignable_to(db, *neg_ty) - }) - { + if ty.is_gradual_equivalent_to(db, Type::AlwaysTruthy) { + if intersection.is_non_empty_literal_string(db) { return true; } } // `is_assignable_to(Intersection[LiteralString, Literal[""]], AlwaysFalsy)` - else if target.is_gradual_equivalent_to(db, Type::AlwaysFalsy) { - if intersection - .positive(db) - .iter() - .any(|pos_ty| pos_ty.is_assignable_to(db, Type::LiteralString)) - && intersection.positive(db).iter().any(|neg_ty| { - Type::string_literal(db, "").is_assignable_to(db, *neg_ty) - }) - { + else if ty.is_gradual_equivalent_to(db, Type::AlwaysFalsy) { + if intersection.is_empty_literal_string(db) { return true; } } @@ -1260,6 +1341,25 @@ impl<'db> Type<'db> { // 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)) => { + // Special handlings + // `is_disjoint_from(~AlwaysTruthy & ..., LiteralString & ~Literal[""])` + // `is_disjoint_from(AlwaysFalsy & ..., LiteralString & ~Literal[""])` + if self_intersection.positive(db).contains(&Type::AlwaysFalsy) + || self_intersection.negative(db).contains(&Type::AlwaysTruthy) + { + if other_intersection.is_non_empty_literal_string(db) { + return true; + } + // `is_disjoint_from(LiteralString & ~Literal[""], AlwaysFalsy & ...)` + } else if other_intersection.positive(db).contains(&Type::AlwaysFalsy) + || other_intersection + .negative(db) + .contains(&Type::AlwaysTruthy) + { + if self_intersection.is_non_empty_literal_string(db) { + return true; + } + } self_intersection .positive(db) .iter() @@ -1272,6 +1372,36 @@ impl<'db> Type<'db> { (Type::Intersection(intersection), other) | (other, Type::Intersection(intersection)) => { + // Special handlings + // is_disjoint_from(~Literal[True] & ~Literal[False] & ..., bool) + // is_disjoint_from(AlwaysTruthy & ~Literal[True] & ..., bool) + // is_disjoint_from(AlwaysFalsy & ~Literal[False] & ..., bool) + if other.is_equivalent_to(db, KnownClass::Bool.to_instance(db)) { + if (intersection + .positive(db) + .iter() + .any(|&pos_ty| pos_ty.is_subtype_of(db, Type::AlwaysFalsy)) + || intersection + .negative(db) + .iter() + .any(|&neg_ty| Type::BooleanLiteral(true).is_subtype_of(db, neg_ty))) + && (intersection + .positive(db) + .iter() + .any(|&pos_ty| pos_ty.is_subtype_of(db, Type::AlwaysTruthy)) + || intersection.negative(db).iter().any(|&neg_ty| { + Type::BooleanLiteral(false).is_subtype_of(db, neg_ty) + })) + { + return true; + } + } + // is_disjoint_from(LiteralString & ~Literal[""], AlwaysFalsy) + else if other.is_equivalent_to(db, Type::AlwaysFalsy) { + if intersection.is_non_empty_literal_string(db) { + return true; + } + } intersection .positive(db) .iter() @@ -5614,6 +5744,16 @@ impl<'db> IntersectionType<'db> { qualifiers, } } + + fn is_empty_literal_string(self, db: &'db dyn Db) -> bool { + self.positive(db).contains(&Type::LiteralString) + && self.positive(db).contains(&Type::string_literal(db, "")) + } + + fn is_non_empty_literal_string(self, db: &'db dyn Db) -> bool { + self.positive(db).contains(&Type::LiteralString) + && self.negative(db).contains(&Type::string_literal(db, "")) + } } #[salsa::interned] diff --git a/crates/red_knot_python_semantic/src/types/type_ordering.rs b/crates/red_knot_python_semantic/src/types/type_ordering.rs index 54bd4d292b74e..8ec1a5fabe301 100644 --- a/crates/red_knot_python_semantic/src/types/type_ordering.rs +++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs @@ -270,6 +270,9 @@ pub(super) fn union_elements_ordering<'db>( (_, Type::Dynamic(_)) => Ordering::Greater, (Type::Union(left), Type::Union(right)) => { + if left.elements(db).len() != right.elements(db).len() { + return left.elements(db).len().cmp(&right.elements(db).len()); + } // Lexicographically compare the elements of the two unions. for (left, right) in left.elements(db).iter().zip(right.elements(db)) { let ordering = union_elements_ordering(left, right, db); @@ -277,29 +280,32 @@ pub(super) fn union_elements_ordering<'db>( return ordering; } } - left.elements(db).len().cmp(&right.elements(db).len()) + Ordering::Equal } (Type::Union(_), _) => Ordering::Less, (_, Type::Union(_)) => Ordering::Greater, (Type::Intersection(left), Type::Intersection(right)) => { // Lexicographically compare the elements of the two intersections. + if left.positive(db).len() != right.positive(db).len() { + return left.positive(db).len().cmp(&right.positive(db).len()); + } + if left.negative(db).len() != right.negative(db).len() { + return left.negative(db).len().cmp(&right.negative(db).len()); + } for (left, right) in left.positive(db).iter().zip(right.positive(db)) { let ordering = union_elements_ordering(left, right, db); if ordering != Ordering::Equal { return ordering; } } - if left.positive(db).len() != right.positive(db).len() { - return left.positive(db).len().cmp(&right.positive(db).len()); - } for (left, right) in left.negative(db).iter().zip(right.negative(db)) { let ordering = union_elements_ordering(left, right, db); if ordering != Ordering::Equal { return ordering; } } - left.negative(db).len().cmp(&right.negative(db).len()) + Ordering::Equal } } } From 9718536fb866598b95b868c69db4265149770888 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Sat, 15 Mar 2025 11:37:07 +0900 Subject: [PATCH 3/3] Update type_ordering.rs * exclude ordering of nested unions (which cannot exist in DNF) as unreachable codes * try to avoid performance degradation in ordering of intersections --- crates/red_knot_python_semantic/src/types.rs | 6 +-- .../src/types/type_ordering.rs | 39 ++++++++----------- 2 files changed, 20 insertions(+), 25 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index f353a753971f9..35d04e66e3b7e 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -9,7 +9,7 @@ use ruff_db::files::File; use ruff_python_ast as ast; use ruff_python_ast::name::Name; use ruff_text_size::{Ranged, TextRange}; -use type_ordering::union_elements_ordering; +use type_ordering::union_or_intersection_elements_ordering; pub(crate) use self::builder::{IntersectionBuilder, UnionBuilder}; pub(crate) use self::diagnostic::register_lints; @@ -5387,7 +5387,7 @@ impl<'db> UnionType<'db> { .iter() .map(|element| element.with_sorted_unions(db)) .collect(); - new_elements.sort_unstable_by(|l, r| union_elements_ordering(l, r, db)); + new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(l, r, db)); UnionType::new(db, new_elements.into_boxed_slice()) } @@ -5501,7 +5501,7 @@ impl<'db> IntersectionType<'db> { .map(|ty| ty.with_sorted_unions(db)) .collect(); - elements.sort_unstable_by(|l, r| union_elements_ordering(l, r, db)); + elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(l, r, db)); elements } diff --git a/crates/red_knot_python_semantic/src/types/type_ordering.rs b/crates/red_knot_python_semantic/src/types/type_ordering.rs index 8ec1a5fabe301..38f64470cd219 100644 --- a/crates/red_knot_python_semantic/src/types/type_ordering.rs +++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs @@ -11,7 +11,8 @@ use super::{ /// in an [`crate::types::IntersectionType`] or a [`crate::types::UnionType`] in order for them /// to be compared for equivalence. /// -/// Two unions / intersections are compared lexicographically. +/// Two intersections are compared lexicographically. +/// Two unions are never compared in this function because DNF does not permit nested unions. /// /// Element types must already be sorted. /// @@ -21,7 +22,7 @@ use super::{ /// create here is not user-facing. However, it doesn't really "make sense" for `Type` to implement /// [`Ord`] in terms of the semantics. There are many different ways in which you could plausibly /// sort a list of types; this is only one (somewhat arbitrary, at times) possible ordering. -pub(super) fn union_elements_ordering<'db>( +pub(super) fn union_or_intersection_elements_ordering<'db>( left: &Type<'db>, right: &Type<'db>, db: &'db dyn crate::Db, @@ -269,38 +270,32 @@ pub(super) fn union_elements_ordering<'db>( (Type::Dynamic(_), _) => Ordering::Less, (_, Type::Dynamic(_)) => Ordering::Greater, - (Type::Union(left), Type::Union(right)) => { - if left.elements(db).len() != right.elements(db).len() { - return left.elements(db).len().cmp(&right.elements(db).len()); - } - // Lexicographically compare the elements of the two unions. - for (left, right) in left.elements(db).iter().zip(right.elements(db)) { - let ordering = union_elements_ordering(left, right, db); - if ordering != Ordering::Equal { - return ordering; - } - } - Ordering::Equal + (Type::Union(_), Type::Union(_)) => { + unreachable!("our type representation does not permit nested unions"); } (Type::Union(_), _) => Ordering::Less, (_, Type::Union(_)) => Ordering::Greater, (Type::Intersection(left), Type::Intersection(right)) => { // Lexicographically compare the elements of the two intersections. - if left.positive(db).len() != right.positive(db).len() { - return left.positive(db).len().cmp(&right.positive(db).len()); + let left_positive = left.positive(db); + let right_positive = right.positive(db); + if left_positive.len() != right_positive.len() { + return left_positive.len().cmp(&right_positive.len()); } - if left.negative(db).len() != right.negative(db).len() { - return left.negative(db).len().cmp(&right.negative(db).len()); + let left_negative = left.negative(db); + let right_negative = right.negative(db); + if left_negative.len() != right_negative.len() { + return left_negative.len().cmp(&right_negative.len()); } - for (left, right) in left.positive(db).iter().zip(right.positive(db)) { - let ordering = union_elements_ordering(left, right, db); + for (left, right) in left_positive.iter().zip(right_positive) { + let ordering = union_or_intersection_elements_ordering(left, right, db); if ordering != Ordering::Equal { return ordering; } } - for (left, right) in left.negative(db).iter().zip(right.negative(db)) { - let ordering = union_elements_ordering(left, right, db); + for (left, right) in left_negative.iter().zip(right_negative) { + let ordering = union_or_intersection_elements_ordering(left, right, db); if ordering != Ordering::Equal { return ordering; }