From 48e65418938da311b591bcd6e0f691f888bcb5e8 Mon Sep 17 00:00:00 2001 From: David Peter Date: Wed, 15 Jan 2025 16:32:21 +0100 Subject: [PATCH] [red-knot] Negation reverses subtyping order (#15503) ## Summary If `S <: T`, then `~T <: ~S`. This test currently fails with example like: ``` S = tuple[()] T = ~Literal[True] & ~Literal[False] ``` `T` is equivalent to `~(Literal[True] | Literal[False])` and therefore equivalent to `~bool`, but the minimal example for a failure is what is stated above. We correctly recognize that `S <: T`, but fail to see that `~T <: ~S`, i.e. `bool <: ~tuple[()]`. This is why the tests goes into the "flaky" section as well. ## Test Plan ``` export QUICKCHECK_TESTS=100000 while cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::flaky::negation_reverses_subtype_order; do :; done ``` --- crates/red_knot_python_semantic/src/types/property_tests.rs | 6 ++++++ 1 file changed, 6 insertions(+) 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 a7057d4068..d259ebb916 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -376,6 +376,12 @@ 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,