From bc8d770ffd7a2d5ccc9286eecad9d856af81695b Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Sat, 15 Mar 2025 11:37:07 +0900 Subject: [PATCH 1/3] fix incorrect ordering of intersection --- .../is_gradual_equivalent_to.md | 2 - crates/red_knot_python_semantic/src/types.rs | 6 +-- .../src/types/type_ordering.rs | 43 ++++++++++++++++--- 3 files changed, 41 insertions(+), 10 deletions(-) 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 795e7a5822f5a..a559e93181caa 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,8 +42,6 @@ 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(not is_gradual_equivalent_to(str | int, int | str | bytes)) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 673eb000dea71..99a3403ab247f 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; @@ -4947,7 +4947,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()) } @@ -5051,7 +5051,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 } 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 9c565b8d1d0cd..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,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 + } } } From da580d1c2336739c08890cab61038116c71527c3 Mon Sep 17 00:00:00 2001 From: Alex Waygood Date: Mon, 17 Mar 2025 11:40:14 +0000 Subject: [PATCH 2/3] minor tweaks --- crates/red_knot_python_semantic/src/types.rs | 4 ++-- .../src/types/property_tests.rs | 12 ++++++------ .../src/types/type_ordering.rs | 7 ++++--- 3 files changed, 12 insertions(+), 11 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 99a3403ab247f..f244419163758 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -4947,7 +4947,7 @@ impl<'db> UnionType<'db> { .iter() .map(|element| element.with_sorted_unions(db)) .collect(); - new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(l, r, db)); + new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); UnionType::new(db, new_elements.into_boxed_slice()) } @@ -5051,7 +5051,7 @@ impl<'db> IntersectionType<'db> { .map(|ty| ty.with_sorted_unions(db)) .collect(); - elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(l, r, db)); + elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); elements } 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 8a07ee414f877..2614ec490b548 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -420,6 +420,12 @@ mod stable { forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t) ); + // If `S <: T`, then `~T <: ~S`. + type_property_test!( + negation_reverses_subtype_order, db, + forall types s, t. s.is_subtype_of(db, t) => t.negate(db).is_subtype_of(db, s.negate(db)) + ); + // `T` is not disjoint from itself, unless `T` is `Never`. type_property_test!( disjoint_from_is_irreflexive, db, @@ -546,12 +552,6 @@ mod flaky { forall types t. t.is_fully_static(db) => t.negate(db).is_disjoint_from(db, t) ); - // If `S <: T`, then `~T <: ~S`. - type_property_test!( - negation_reverses_subtype_order, db, - forall types s, t. s.is_subtype_of(db, t) => t.negate(db).is_subtype_of(db, s.negate(db)) - ); - // For two fully static types, their intersection must be a subtype of each type in the pair. type_property_test!( all_fully_static_type_pairs_are_supertypes_of_their_intersection, db, 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 38f64470cd219..81b3832dd8994 100644 --- a/crates/red_knot_python_semantic/src/types/type_ordering.rs +++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs @@ -1,5 +1,6 @@ use std::cmp::Ordering; +use crate::db::Db; use crate::types::CallableType; use super::{ @@ -23,9 +24,9 @@ use super::{ /// [`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_or_intersection_elements_ordering<'db>( + db: &'db dyn Db, left: &Type<'db>, right: &Type<'db>, - db: &'db dyn crate::Db, ) -> Ordering { if left == right { return Ordering::Equal; @@ -289,13 +290,13 @@ pub(super) fn union_or_intersection_elements_ordering<'db>( 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); + let ordering = union_or_intersection_elements_ordering(db, left, right); 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); + let ordering = union_or_intersection_elements_ordering(db, left, right); if ordering != Ordering::Equal { return ordering; } From ca1404f4a08940301cef197fe0878d17fb8d5bcf Mon Sep 17 00:00:00 2001 From: Alex Waygood Date: Mon, 17 Mar 2025 12:05:16 +0000 Subject: [PATCH 3/3] final nits --- crates/red_knot_python_semantic/src/types.rs | 12 ++++---- .../src/types/type_ordering.rs | 29 ++++++++++++------- 2 files changed, 25 insertions(+), 16 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index f244419163758..46e0f8f99d9cd 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -494,13 +494,13 @@ impl<'db> Type<'db> { /// Return a normalized version of `self` in which all unions and intersections are sorted /// according to a canonical order, no matter how "deeply" a union/intersection may be nested. #[must_use] - pub fn with_sorted_unions(self, db: &'db dyn Db) -> Self { + pub fn with_sorted_unions_and_intersections(self, db: &'db dyn Db) -> Self { match self { Type::Union(union) => Type::Union(union.to_sorted_union(db)), Type::Intersection(intersection) => { Type::Intersection(intersection.to_sorted_intersection(db)) } - Type::Tuple(tuple) => Type::Tuple(tuple.with_sorted_unions(db)), + Type::Tuple(tuple) => Type::Tuple(tuple.with_sorted_unions_and_intersections(db)), Type::LiteralString | Type::Instance(_) | Type::AlwaysFalsy @@ -4945,7 +4945,7 @@ impl<'db> UnionType<'db> { let mut new_elements: Vec> = self .elements(db) .iter() - .map(|element| element.with_sorted_unions(db)) + .map(|element| element.with_sorted_unions_and_intersections(db)) .collect(); new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); UnionType::new(db, new_elements.into_boxed_slice()) @@ -5048,7 +5048,7 @@ impl<'db> IntersectionType<'db> { ) -> FxOrderSet> { let mut elements: FxOrderSet> = elements .iter() - .map(|ty| ty.with_sorted_unions(db)) + .map(|ty| ty.with_sorted_unions_and_intersections(db)) .collect(); elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); @@ -5317,11 +5317,11 @@ impl<'db> TupleType<'db> { /// Return a normalized version of `self` in which all unions and intersections are sorted /// according to a canonical order, no matter how "deeply" a union/intersection may be nested. #[must_use] - pub fn with_sorted_unions(self, db: &'db dyn Db) -> Self { + pub fn with_sorted_unions_and_intersections(self, db: &'db dyn Db) -> Self { let elements: Box<[Type<'db>]> = self .elements(db) .iter() - .map(|ty| ty.with_sorted_unions(db)) + .map(|ty| ty.with_sorted_unions_and_intersections(db)) .collect(); TupleType::new(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 81b3832dd8994..c80bd55170526 100644 --- a/crates/red_knot_python_semantic/src/types/type_ordering.rs +++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs @@ -12,10 +12,9 @@ use super::{ /// in an [`crate::types::IntersectionType`] or a [`crate::types::UnionType`] in order for them /// to be compared for equivalence. /// -/// 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. +/// Two intersections are compared lexicographically. Element types in the intersection must +/// already be sorted. Two unions are never compared in this function because DNF does not permit +/// nested unions. /// /// ## Why not just implement [`Ord`] on [`Type`]? /// @@ -90,7 +89,11 @@ pub(super) fn union_or_intersection_elements_ordering<'db>( (Type::Callable(CallableType::General(_)), _) => Ordering::Less, (_, Type::Callable(CallableType::General(_))) => Ordering::Greater, - (Type::Tuple(left), Type::Tuple(right)) => left.cmp(right), + (Type::Tuple(left), Type::Tuple(right)) => { + debug_assert_eq!(*left, left.with_sorted_unions_and_intersections(db)); + debug_assert_eq!(*right, right.with_sorted_unions_and_intersections(db)); + left.cmp(right) + } (Type::Tuple(_), _) => Ordering::Less, (_, Type::Tuple(_)) => Ordering::Greater, @@ -271,14 +274,19 @@ pub(super) fn union_or_intersection_elements_ordering<'db>( (Type::Dynamic(_), _) => Ordering::Less, (_, Type::Dynamic(_)) => Ordering::Greater, - (Type::Union(_), Type::Union(_)) => { + (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. + debug_assert_eq!(*left, left.to_sorted_intersection(db)); + debug_assert_eq!(*right, right.to_sorted_intersection(db)); + + if left == right { + return Ordering::Equal; + } + + // Lexicographically compare the elements of the two unequal intersections. let left_positive = left.positive(db); let right_positive = right.positive(db); if left_positive.len() != right_positive.len() { @@ -301,7 +309,8 @@ pub(super) fn union_or_intersection_elements_ordering<'db>( return ordering; } } - Ordering::Equal + + unreachable!("Two equal intersections that both have sorted elements should share the same Salsa ID") } } }