Skip to content

Commit 50b66dc

Browse files
AlexWaygoodmtshiba
andauthored
[red-knot] Stabilize negation_reverses_subtype_order property test (#16801)
## Summary This is a re-creation of #16764 by @mtshiba, which I closed meaning to immediately reopen (GitHub wasn't updating the PR with the latest pushed changes), and which GitHub will not allow me to reopen for some reason. Pasting the summary from that PR below: > From #16641 > > As stated in this comment (#16641 (comment)), the current ordering implementation for intersection types is incorrect. So, I will introduce lexicographic ordering for intersection types. ## Test Plan One property test stabilised (tested locally with `QUICKCHECK_TESTS=2000000 cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::stable::negation_reverses_subtype_order`), and existing mdtests that previously failed now pass. Primarily-authored-by: [mtshiba](https://github.com/astral-sh/ruff/commits?author=mtshiba) --------- Co-authored-by: Shunsuke Shibayama <sbym1346@gmail.com>
1 parent 2470777 commit 50b66dc

File tree

4 files changed

+66
-25
lines changed

4 files changed

+66
-25
lines changed

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,6 @@ static_assert(is_gradual_equivalent_to(str | int, int | str))
4242
static_assert(
4343
is_gradual_equivalent_to(Intersection[str, int, Not[bytes], Not[None]], Intersection[int, str, Not[None], Not[bytes]])
4444
)
45-
# TODO: `~type[Any]` shoudld be gradually equivalent to `~type[Unknown]`
46-
# error: [static-assert-error]
4745
static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]], Intersection[int | str, Not[type[Unknown]]]))
4846

4947
static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes))

crates/red_knot_python_semantic/src/types.rs

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ use ruff_db::files::File;
99
use ruff_python_ast as ast;
1010
use ruff_python_ast::name::Name;
1111
use ruff_text_size::{Ranged, TextRange};
12-
use type_ordering::union_elements_ordering;
12+
use type_ordering::union_or_intersection_elements_ordering;
1313

1414
pub(crate) use self::builder::{IntersectionBuilder, UnionBuilder};
1515
pub(crate) use self::diagnostic::register_lints;
@@ -494,13 +494,13 @@ impl<'db> Type<'db> {
494494
/// Return a normalized version of `self` in which all unions and intersections are sorted
495495
/// according to a canonical order, no matter how "deeply" a union/intersection may be nested.
496496
#[must_use]
497-
pub fn with_sorted_unions(self, db: &'db dyn Db) -> Self {
497+
pub fn with_sorted_unions_and_intersections(self, db: &'db dyn Db) -> Self {
498498
match self {
499499
Type::Union(union) => Type::Union(union.to_sorted_union(db)),
500500
Type::Intersection(intersection) => {
501501
Type::Intersection(intersection.to_sorted_intersection(db))
502502
}
503-
Type::Tuple(tuple) => Type::Tuple(tuple.with_sorted_unions(db)),
503+
Type::Tuple(tuple) => Type::Tuple(tuple.with_sorted_unions_and_intersections(db)),
504504
Type::LiteralString
505505
| Type::Instance(_)
506506
| Type::AlwaysFalsy
@@ -4945,9 +4945,9 @@ impl<'db> UnionType<'db> {
49454945
let mut new_elements: Vec<Type<'db>> = self
49464946
.elements(db)
49474947
.iter()
4948-
.map(|element| element.with_sorted_unions(db))
4948+
.map(|element| element.with_sorted_unions_and_intersections(db))
49494949
.collect();
4950-
new_elements.sort_unstable_by(union_elements_ordering);
4950+
new_elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r));
49514951
UnionType::new(db, new_elements.into_boxed_slice())
49524952
}
49534953

@@ -5048,10 +5048,10 @@ impl<'db> IntersectionType<'db> {
50485048
) -> FxOrderSet<Type<'db>> {
50495049
let mut elements: FxOrderSet<Type<'db>> = elements
50505050
.iter()
5051-
.map(|ty| ty.with_sorted_unions(db))
5051+
.map(|ty| ty.with_sorted_unions_and_intersections(db))
50525052
.collect();
50535053

5054-
elements.sort_unstable_by(union_elements_ordering);
5054+
elements.sort_unstable_by(|l, r| union_or_intersection_elements_ordering(db, l, r));
50555055
elements
50565056
}
50575057

@@ -5317,11 +5317,11 @@ impl<'db> TupleType<'db> {
53175317
/// Return a normalized version of `self` in which all unions and intersections are sorted
53185318
/// according to a canonical order, no matter how "deeply" a union/intersection may be nested.
53195319
#[must_use]
5320-
pub fn with_sorted_unions(self, db: &'db dyn Db) -> Self {
5320+
pub fn with_sorted_unions_and_intersections(self, db: &'db dyn Db) -> Self {
53215321
let elements: Box<[Type<'db>]> = self
53225322
.elements(db)
53235323
.iter()
5324-
.map(|ty| ty.with_sorted_unions(db))
5324+
.map(|ty| ty.with_sorted_unions_and_intersections(db))
53255325
.collect();
53265326
TupleType::new(db, elements)
53275327
}

crates/red_knot_python_semantic/src/types/property_tests.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -420,6 +420,12 @@ mod stable {
420420
forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t)
421421
);
422422

423+
// If `S <: T`, then `~T <: ~S`.
424+
type_property_test!(
425+
negation_reverses_subtype_order, db,
426+
forall types s, t. s.is_subtype_of(db, t) => t.negate(db).is_subtype_of(db, s.negate(db))
427+
);
428+
423429
// `T` is not disjoint from itself, unless `T` is `Never`.
424430
type_property_test!(
425431
disjoint_from_is_irreflexive, db,
@@ -546,12 +552,6 @@ mod flaky {
546552
forall types t. t.is_fully_static(db) => t.negate(db).is_disjoint_from(db, t)
547553
);
548554

549-
// If `S <: T`, then `~T <: ~S`.
550-
type_property_test!(
551-
negation_reverses_subtype_order, db,
552-
forall types s, t. s.is_subtype_of(db, t) => t.negate(db).is_subtype_of(db, s.negate(db))
553-
);
554-
555555
// For two fully static types, their intersection must be a subtype of each type in the pair.
556556
type_property_test!(
557557
all_fully_static_type_pairs_are_supertypes_of_their_intersection, db,

crates/red_knot_python_semantic/src/types/type_ordering.rs

Lines changed: 51 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
use std::cmp::Ordering;
22

3+
use crate::db::Db;
34
use crate::types::CallableType;
45

56
use super::{
@@ -11,16 +12,21 @@ use super::{
1112
/// in an [`crate::types::IntersectionType`] or a [`crate::types::UnionType`] in order for them
1213
/// to be compared for equivalence.
1314
///
14-
/// Two unions with equal sets of elements will only compare equal if they have their element sets
15-
/// ordered the same way.
15+
/// Two intersections are compared lexicographically. Element types in the intersection must
16+
/// already be sorted. Two unions are never compared in this function because DNF does not permit
17+
/// nested unions.
1618
///
1719
/// ## Why not just implement [`Ord`] on [`Type`]?
1820
///
1921
/// It would be fairly easy to slap `#[derive(PartialOrd, Ord)]` on [`Type`], and the ordering we
2022
/// create here is not user-facing. However, it doesn't really "make sense" for `Type` to implement
2123
/// [`Ord`] in terms of the semantics. There are many different ways in which you could plausibly
2224
/// sort a list of types; this is only one (somewhat arbitrary, at times) possible ordering.
23-
pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'db>) -> Ordering {
25+
pub(super) fn union_or_intersection_elements_ordering<'db>(
26+
db: &'db dyn Db,
27+
left: &Type<'db>,
28+
right: &Type<'db>,
29+
) -> Ordering {
2430
if left == right {
2531
return Ordering::Equal;
2632
}
@@ -83,7 +89,11 @@ pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'db>)
8389
(Type::Callable(CallableType::General(_)), _) => Ordering::Less,
8490
(_, Type::Callable(CallableType::General(_))) => Ordering::Greater,
8591

86-
(Type::Tuple(left), Type::Tuple(right)) => left.cmp(right),
92+
(Type::Tuple(left), Type::Tuple(right)) => {
93+
debug_assert_eq!(*left, left.with_sorted_unions_and_intersections(db));
94+
debug_assert_eq!(*right, right.with_sorted_unions_and_intersections(db));
95+
left.cmp(right)
96+
}
8797
(Type::Tuple(_), _) => Ordering::Less,
8898
(_, Type::Tuple(_)) => Ordering::Greater,
8999

@@ -264,11 +274,44 @@ pub(super) fn union_elements_ordering<'db>(left: &Type<'db>, right: &Type<'db>)
264274
(Type::Dynamic(_), _) => Ordering::Less,
265275
(_, Type::Dynamic(_)) => Ordering::Greater,
266276

267-
(Type::Union(left), Type::Union(right)) => left.cmp(right),
268-
(Type::Union(_), _) => Ordering::Less,
269-
(_, Type::Union(_)) => Ordering::Greater,
277+
(Type::Union(_), _) | (_, Type::Union(_)) => {
278+
unreachable!("our type representation does not permit nested unions");
279+
}
280+
281+
(Type::Intersection(left), Type::Intersection(right)) => {
282+
debug_assert_eq!(*left, left.to_sorted_intersection(db));
283+
debug_assert_eq!(*right, right.to_sorted_intersection(db));
270284

271-
(Type::Intersection(left), Type::Intersection(right)) => left.cmp(right),
285+
if left == right {
286+
return Ordering::Equal;
287+
}
288+
289+
// Lexicographically compare the elements of the two unequal intersections.
290+
let left_positive = left.positive(db);
291+
let right_positive = right.positive(db);
292+
if left_positive.len() != right_positive.len() {
293+
return left_positive.len().cmp(&right_positive.len());
294+
}
295+
let left_negative = left.negative(db);
296+
let right_negative = right.negative(db);
297+
if left_negative.len() != right_negative.len() {
298+
return left_negative.len().cmp(&right_negative.len());
299+
}
300+
for (left, right) in left_positive.iter().zip(right_positive) {
301+
let ordering = union_or_intersection_elements_ordering(db, left, right);
302+
if ordering != Ordering::Equal {
303+
return ordering;
304+
}
305+
}
306+
for (left, right) in left_negative.iter().zip(right_negative) {
307+
let ordering = union_or_intersection_elements_ordering(db, left, right);
308+
if ordering != Ordering::Equal {
309+
return ordering;
310+
}
311+
}
312+
313+
unreachable!("Two equal intersections that both have sorted elements should share the same Salsa ID")
314+
}
272315
}
273316
}
274317

0 commit comments

Comments
 (0)