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 795e7a5822..a559e93181 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 41ddaa1a4b..578c0860d7 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; @@ -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,9 +4945,9 @@ 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(union_elements_ordering); + new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); UnionType::new(db, new_elements.into_boxed_slice()) } @@ -5048,10 +5048,10 @@ 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(union_elements_ordering); + elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r)); elements } @@ -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/property_tests.rs b/crates/red_knot_python_semantic/src/types/property_tests.rs index 8a07ee414f..2614ec490b 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 9c565b8d1d..c80bd55170 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::{ @@ -11,8 +12,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 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`]? /// @@ -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>( + db: &'db dyn Db, + left: &Type<'db>, + right: &Type<'db>, +) -> Ordering { if left == right { return Ordering::Equal; } @@ -83,7 +89,11 @@ pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'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, @@ -264,11 +274,44 @@ 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(_), _) => Ordering::Less, - (_, Type::Union(_)) => Ordering::Greater, + (Type::Union(_), _) | (_, Type::Union(_)) => { + unreachable!("our type representation does not permit nested unions"); + } - (Type::Intersection(left), Type::Intersection(right)) => left.cmp(right), + (Type::Intersection(left), Type::Intersection(right)) => { + 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() { + 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(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(db, left, right); + if ordering != Ordering::Equal { + return ordering; + } + } + + unreachable!("Two equal intersections that both have sorted elements should share the same Salsa ID") + } } }