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 a7f0441653aa9f..a2f1ef63587c08 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 19be965d3fdc33..a36d64c8ef1b49 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 54c313f789dba6..d3c44f6c00002a 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): ... @@ -296,6 +301,30 @@ 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]])) + +# 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, Not[Literal[""]]], AlwaysTruthy)) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) +# `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[Literal[""]]], Not[AlwaysFalsy])) +static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy])) +# `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 9a600816fa09c1..9fe632f5ed5935 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 @@ -27,7 +27,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: ... @@ -56,6 +56,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 @@ -196,7 +200,7 @@ static_assert(is_disjoint_from(None, Intersection[int, Not[str]])) ```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, AlwaysFalsy, AlwaysTruthy static_assert(is_disjoint_from(Literal[True], Literal[False])) static_assert(is_disjoint_from(Literal[True], Literal[1])) @@ -223,6 +227,35 @@ 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"])) + +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 047a45fc2fd0b8..fa45a92cc8f041 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_gradual_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md index 795e7a5822f5ab..586ea9230df020 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 3998c0a0f11b28..4ba2a4f2d728b5 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,31 @@ 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)) + +# 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, Not[Literal[""]]], AlwaysTruthy)) +static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy)) +# `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 & ~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 673eb000dea719..35d04e66e3b7eb 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; @@ -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,57 @@ 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(LiteralString, 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; + } + } + // `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() + .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 @@ -580,9 +631,137 @@ 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(self_intersection), Type::Intersection(target_intersection)) => { + // Special handlings + // `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) + .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]]])` + // `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_subtype_of(db, *pos_ty)) + { + return true; + } + } + // `LiteralString & AlwaysFalsy`, `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` + 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) + .iter() + .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; + } + } + // 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), _) => { + // Special handlings + // For example: + // `is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy)` + if target.is_equivalent_to(db, Type::AlwaysTruthy) { + 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.is_empty_literal_string(db) { + return true; + } + } + intersection + .positive(db) + .iter() + .any(|&elem_ty| elem_ty.is_subtype_of(db, target)) + } + (_, Type::Intersection(intersection)) => { intersection .positive(db) @@ -594,11 +773,6 @@ 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(), @@ -770,10 +944,191 @@ 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; + } + } + // `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() + .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)) + } + + (Type::Intersection(self_intersection), Type::Intersection(target_intersection)) => { + // Special handlings + // `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) + .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]]])` + // `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 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) + .iter() + .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; + } + } + // 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 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 ty.is_gradual_equivalent_to(db, Type::AlwaysFalsy) { + if intersection.is_empty_literal_string(db) { + return true; + } + } + intersection + .positive(db) + .iter() + .any(|elem_ty| elem_ty.is_assignable_to(db, 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, @@ -793,14 +1148,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)) => { @@ -951,10 +1298,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) + } ( Type::Callable(CallableType::General(first)), @@ -984,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() @@ -991,11 +1367,41 @@ impl<'db> Type<'db> { || other_intersection .positive(db) .iter() - .any(|p: &Type<'_>| p.is_disjoint_from(db, self)) + .any(|p| p.is_disjoint_from(db, self)) } (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() @@ -3410,6 +3816,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> { @@ -4823,6 +5243,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> @@ -4947,7 +5387,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_or_intersection_elements_ordering(l, r, db)); UnionType::new(db, new_elements.into_boxed_slice()) } @@ -4995,14 +5435,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; @@ -5051,7 +5501,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_or_intersection_elements_ordering(l, r, db)); elements } @@ -5067,6 +5517,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 @@ -5128,13 +5608,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; @@ -5251,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/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs index c8b8dc133d1e53..c7f07a66f67ca1 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 8a07ee414f8775..8d4f045136da51 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -562,7 +562,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 9c565b8d1d0cda..38f64470cd2197 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,10 @@ 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 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. /// /// ## Why not just implement [`Ord`] on [`Type`]? /// @@ -20,7 +22,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_or_intersection_elements_ordering<'db>( + left: &Type<'db>, + right: &Type<'db>, + db: &'db dyn crate::Db, +) -> Ordering { if left == right { return Ordering::Equal; } @@ -264,11 +270,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(_), 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)) => left.cmp(right), + (Type::Intersection(left), Type::Intersection(right)) => { + // Lexicographically compare the elements of the two intersections. + 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()); + } + 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.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.iter().zip(right_negative) { + let ordering = union_or_intersection_elements_ordering(left, right, db); + if ordering != Ordering::Equal { + return ordering; + } + } + Ordering::Equal + } } }