[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
```
This commit is contained in:
David Peter 2025-01-15 16:32:21 +01:00 committed by GitHub
parent 55a7f72035
commit 48e6541893
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -376,6 +376,12 @@ mod flaky {
forall types t. t.is_fully_static(db) => t.negate(db).is_disjoint_from(db, t) 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. // For two fully static types, their intersection must be a subtype of each type in the pair.
type_property_test!( type_property_test!(
all_fully_static_type_pairs_are_supertypes_of_their_intersection, db, all_fully_static_type_pairs_are_supertypes_of_their_intersection, db,