[red-knot] Incorrect subtyping behavior of Literal instances and _SpecialForm
#14731
Comments
sharkdp
added
bug
This was referenced Dec 2, 2024
sharkdp
added a commit
that referenced
this issue
Dec 3, 2024
## Summary This PR adds a new `property_tests` module with quickcheck-based tests that verify certain properties of types. The following properties are currently checked: * `is_equivalent_to`: * is reflexive: `T` is equivalent to itself * `is_subtype_of`: * is reflexive: `T` is a subtype of `T` * is antisymmetric: if `S <: T` and `T <: S`, then `S` is equivalent to `T` * is transitive: `S <: T` & `T <: U` => `S <: U` * `is_disjoint_from`: * is irreflexive: `T` is not disjoint from `T` * is symmetric: `S` disjoint from `T` => `T` disjoint from `S` * `is_assignable_to`: * is reflexive * `negate`: * is an involution: `T.negate().negate()` is equivalent to `T` There are also some tests that validate higher-level properties like: * `S <: T` implies that `S` is not disjoint from `T` * `S <: T` implies that `S` is assignable to `T` * A singleton type must also be single-valued These tests found a few bugs so far: - #14177 - #14195 - #14196 - #14210 - #14731 Some additional notes: - Quickcheck-based property tests are non-deterministic and finding counter-examples might take an arbitrary long time. This makes them bad candidates for running in CI (for every PR). We can think of running them in a cron-job way from time to time, similar to fuzzing. But for now, it's only possible to run them locally (see instructions in source code). - Some tests currently find false positive "counterexamples" because our understanding of equivalence of types is not yet complete. We do not understand that `int | str` is the same as `str | int`, for example. These tests are in a separate `property_tests::flaky` module. - Properties can not be formulated in every way possible, due to the fact that `is_disjoint_from` and `is_subtype_of` can produce false negative answers. - The current shrinking implementation is very naive, which leads to counterexamples that are very long (`str & Any & ~tuple[Any] & ~tuple[Unknown] & ~Literal[""] & ~Literal["a"] | str & int & ~tuple[Any] & ~tuple[Unknown]`), requiring the developer to simplify manually. It has not been a major issue so far, but there is a comment in the code how this can be improved. - The tests are currently implemented using a macro. This is a single commit on top which can easily be reverted, if we prefer the plain code instead. With the macro: ```rs // `S <: T` implies that `S` can be assigned to `T`. type_property_test!( subtype_of_implies_assignable_to, db, forall types s, t. s.is_subtype_of(db, t) => s.is_assignable_to(db, t) ); ``` without the macro: ```rs /// `S <: T` implies that `S` can be assigned to `T`. #[quickcheck] fn subtype_of_implies_assignable_to(s: Ty, t: Ty) -> bool { let db = get_cached_db(); let s = s.into_type(&db); let t = t.into_type(&db); !s.is_subtype_of(&*db, t) || s.is_assignable_to(&*db, t) } ``` ## Test Plan ```bash while cargo test --release -p red_knot_python_semantic --features property_tests types::property_tests; do :; done ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
We have a correct test for the subtype relationship between these two types here:
https://github.com/astral-sh/ruff/blob/6dfe125f44352f5fdff19f6d47fc33ac7a6e86ad/crates/red_knot_python_semantic/src/types.rs#L3208C9-L3208C72
But the opposite is also true, at the moment. We should fix this and add a
is_not_subtype_oftest case.The text was updated successfully, but these errors were encountered: