mirror of https://github.com/astral-sh/ruff
[red-knot] Ensure differently ordered unions and intersections are considered equivalent (#15516)
This commit is contained in:
Alex Waygood
GitHub
parent
b8e5b95423
commit
2b24b3b316
|
|
@ -110,10 +110,8 @@ python-version = "3.10"
|
|||
from typing_extensions import assert_type
|
||||
|
||||
def _(a: str | int):
|
||||
assert_type(a, str | int) # fine
|
||||
|
||||
# TODO: Order-independent union handling in type equivalence
|
||||
assert_type(a, int | str) # error: [type-assertion-failure]
|
||||
assert_type(a, str | int)
|
||||
assert_type(a, int | str)
|
||||
```
|
||||
|
||||
## Intersections
|
||||
|
|
@ -135,8 +133,6 @@ def _(a: A):
|
|||
if isinstance(a, B) and not isinstance(a, C) and not isinstance(a, D):
|
||||
reveal_type(a) # revealed: A & B & ~C & ~D
|
||||
|
||||
assert_type(a, Intersection[A, B, Not[C], Not[D]]) # fine
|
||||
|
||||
# TODO: Order-independent intersection handling in type equivalence
|
||||
assert_type(a, Intersection[B, A, Not[D], Not[C]]) # error: [type-assertion-failure]
|
||||
assert_type(a, Intersection[A, B, Not[C], Not[D]])
|
||||
assert_type(a, Intersection[B, A, Not[D], Not[C]])
|
||||
```
|
||||
|
|
|
|||
|
|
@ -32,4 +32,38 @@ static_assert(not is_equivalent_to(Literal[1, 0], Literal[1, 2]))
|
|||
static_assert(not is_equivalent_to(Literal[1, 2, 3], Literal[1, 2]))
|
||||
```
|
||||
|
||||
## Differently ordered intersections and unions are equivalent
|
||||
|
||||
```py
|
||||
from knot_extensions import is_equivalent_to, static_assert, Intersection, Not
|
||||
|
||||
class P: ...
|
||||
class Q: ...
|
||||
class R: ...
|
||||
class S: ...
|
||||
|
||||
static_assert(is_equivalent_to(P | Q | R, P | R | Q)) # 1
|
||||
static_assert(is_equivalent_to(P | Q | R, Q | P | R)) # 2
|
||||
static_assert(is_equivalent_to(P | Q | R, Q | R | P)) # 3
|
||||
static_assert(is_equivalent_to(P | Q | R, R | P | Q)) # 4
|
||||
static_assert(is_equivalent_to(P | Q | R, R | Q | P)) # 5
|
||||
static_assert(is_equivalent_to(P | R | Q, Q | P | R)) # 6
|
||||
static_assert(is_equivalent_to(P | R | Q, Q | R | P)) # 7
|
||||
static_assert(is_equivalent_to(P | R | Q, R | P | Q)) # 8
|
||||
static_assert(is_equivalent_to(P | R | Q, R | Q | P)) # 9
|
||||
static_assert(is_equivalent_to(Q | P | R, Q | R | P)) # 10
|
||||
static_assert(is_equivalent_to(Q | P | R, R | P | Q)) # 11
|
||||
static_assert(is_equivalent_to(Q | P | R, R | Q | P)) # 12
|
||||
static_assert(is_equivalent_to(Q | R | P, R | P | Q)) # 13
|
||||
static_assert(is_equivalent_to(Q | R | P, R | Q | P)) # 14
|
||||
static_assert(is_equivalent_to(R | P | Q, R | Q | P)) # 15
|
||||
|
||||
static_assert(is_equivalent_to(str | None, None | str))
|
||||
|
||||
static_assert(is_equivalent_to(Intersection[P, Q], Intersection[Q, P]))
|
||||
static_assert(is_equivalent_to(Intersection[Q, Not[P]], Intersection[Not[P], Q]))
|
||||
static_assert(is_equivalent_to(Intersection[Q, R, Not[P]], Intersection[Not[P], R, Q]))
|
||||
static_assert(is_equivalent_to(Intersection[Q | R, Not[P | S]], Intersection[Not[S | P], R | Q]))
|
||||
```
|
||||
|
||||
[the equivalence relation]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent
|
||||
|
|
|
|||
|
|
@ -38,13 +38,11 @@ from knot_extensions import Intersection, Not, Unknown, is_gradual_equivalent_to
|
|||
|
||||
static_assert(is_gradual_equivalent_to(str | int, str | int))
|
||||
static_assert(is_gradual_equivalent_to(str | int | Any, str | int | Unknown))
|
||||
|
||||
# TODO: These should pass
|
||||
static_assert(is_gradual_equivalent_to(str | int, int | str)) # error: [static-assert-error]
|
||||
# error: [static-assert-error]
|
||||
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]]]))
|
||||
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ use itertools::Itertools;
|
|||
use ruff_db::diagnostic::Severity;
|
||||
use ruff_db::files::File;
|
||||
use ruff_python_ast as ast;
|
||||
use type_ordering::union_elements_ordering;
|
||||
|
||||
pub(crate) use self::builder::{IntersectionBuilder, UnionBuilder};
|
||||
pub(crate) use self::diagnostic::register_lints;
|
||||
|
|
@ -55,6 +56,7 @@ mod signatures;
|
|||
mod slots;
|
||||
mod string_annotation;
|
||||
mod subclass_of;
|
||||
mod type_ordering;
|
||||
mod unpacker;
|
||||
|
||||
#[cfg(test)]
|
||||
|
|
@ -1112,16 +1114,15 @@ impl<'db> Type<'db> {
|
|||
///
|
||||
/// [equivalent to]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent
|
||||
pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool {
|
||||
if !(self.is_fully_static(db) && other.is_fully_static(db)) {
|
||||
return false;
|
||||
// TODO equivalent but not identical types: TypedDicts, Protocols, type aliases, etc.
|
||||
|
||||
match (self, other) {
|
||||
(Type::Union(left), Type::Union(right)) => left.is_equivalent_to(db, right),
|
||||
(Type::Intersection(left), Type::Intersection(right)) => {
|
||||
left.is_equivalent_to(db, right)
|
||||
}
|
||||
_ => self.is_fully_static(db) && other.is_fully_static(db) && self == other,
|
||||
}
|
||||
|
||||
// TODO equivalent but not identical structural types, differently-ordered unions and
|
||||
// intersections, other cases?
|
||||
|
||||
// For all other cases, types are equivalent iff they have the same internal
|
||||
// representation.
|
||||
self == other
|
||||
}
|
||||
|
||||
/// Returns true if both `self` and `other` are the same gradual form
|
||||
|
|
@ -1163,16 +1164,6 @@ impl<'db> Type<'db> {
|
|||
|
||||
(Type::Dynamic(_), Type::Dynamic(_)) => true,
|
||||
|
||||
(Type::Instance(instance), Type::SubclassOf(subclass))
|
||||
| (Type::SubclassOf(subclass), Type::Instance(instance)) => {
|
||||
let Some(base_class) = subclass.subclass_of().into_class() else {
|
||||
return false;
|
||||
};
|
||||
|
||||
instance.class.is_known(db, KnownClass::Type)
|
||||
&& base_class.is_known(db, KnownClass::Object)
|
||||
}
|
||||
|
||||
(Type::SubclassOf(first), Type::SubclassOf(second)) => {
|
||||
match (first.subclass_of(), second.subclass_of()) {
|
||||
(first, second) if first == second => true,
|
||||
|
|
@ -1189,34 +1180,10 @@ impl<'db> Type<'db> {
|
|||
&& iter::zip(first_elements, second_elements).all(equivalent)
|
||||
}
|
||||
|
||||
// TODO: Handle equivalent unions with items in different order
|
||||
(Type::Union(first), Type::Union(second)) => {
|
||||
let first_elements = first.elements(db);
|
||||
let second_elements = second.elements(db);
|
||||
(Type::Union(first), Type::Union(second)) => first.is_gradual_equivalent_to(db, second),
|
||||
|
||||
if first_elements.len() != second_elements.len() {
|
||||
return false;
|
||||
}
|
||||
|
||||
iter::zip(first_elements, second_elements).all(equivalent)
|
||||
}
|
||||
|
||||
// TODO: Handle equivalent intersections with items in different order
|
||||
(Type::Intersection(first), Type::Intersection(second)) => {
|
||||
let first_positive = first.positive(db);
|
||||
let first_negative = first.negative(db);
|
||||
|
||||
let second_positive = second.positive(db);
|
||||
let second_negative = second.negative(db);
|
||||
|
||||
if first_positive.len() != second_positive.len()
|
||||
|| first_negative.len() != second_negative.len()
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
iter::zip(first_positive, second_positive).all(equivalent)
|
||||
&& iter::zip(first_negative, second_negative).all(equivalent)
|
||||
first.is_gradual_equivalent_to(db, second)
|
||||
}
|
||||
|
||||
_ => false,
|
||||
|
|
@ -1476,7 +1443,7 @@ impl<'db> Type<'db> {
|
|||
}
|
||||
|
||||
/// Returns true if the type does not contain any gradual forms (as a sub-part).
|
||||
pub(crate) fn is_fully_static(self, db: &'db dyn Db) -> bool {
|
||||
pub(crate) fn is_fully_static(&self, db: &'db dyn Db) -> bool {
|
||||
match self {
|
||||
Type::Dynamic(_) => false,
|
||||
Type::Never
|
||||
|
|
@ -1510,20 +1477,8 @@ impl<'db> Type<'db> {
|
|||
|
||||
true
|
||||
}
|
||||
Type::Union(union) => union
|
||||
.elements(db)
|
||||
.iter()
|
||||
.all(|elem| elem.is_fully_static(db)),
|
||||
Type::Intersection(intersection) => {
|
||||
intersection
|
||||
.positive(db)
|
||||
.iter()
|
||||
.all(|elem| elem.is_fully_static(db))
|
||||
&& intersection
|
||||
.negative(db)
|
||||
.iter()
|
||||
.all(|elem| elem.is_fully_static(db))
|
||||
}
|
||||
Type::Union(union) => union.is_fully_static(db),
|
||||
Type::Intersection(intersection) => intersection.is_fully_static(db),
|
||||
Type::Tuple(tuple) => tuple
|
||||
.elements(db)
|
||||
.iter()
|
||||
|
|
@ -4316,10 +4271,11 @@ impl<'db> UnionType<'db> {
|
|||
|
||||
/// Create a union from a list of elements
|
||||
/// (which may be eagerly simplified into a different variant of [`Type`] altogether).
|
||||
pub fn from_elements<T: Into<Type<'db>>>(
|
||||
db: &'db dyn Db,
|
||||
elements: impl IntoIterator<Item = T>,
|
||||
) -> Type<'db> {
|
||||
pub fn from_elements<I, T>(db: &'db dyn Db, elements: I) -> Type<'db>
|
||||
where
|
||||
I: IntoIterator<Item = T>,
|
||||
T: Into<Type<'db>>,
|
||||
{
|
||||
elements
|
||||
.into_iter()
|
||||
.fold(UnionBuilder::new(db), |builder, element| {
|
||||
|
|
@ -4337,6 +4293,93 @@ impl<'db> UnionType<'db> {
|
|||
) -> Type<'db> {
|
||||
Self::from_elements(db, self.elements(db).iter().map(transform_fn))
|
||||
}
|
||||
|
||||
pub fn is_fully_static(self, db: &'db dyn Db) -> bool {
|
||||
self.elements(db).iter().all(|ty| ty.is_fully_static(db))
|
||||
}
|
||||
|
||||
/// Create a new union type with the elements sorted according to a canonical ordering.
|
||||
#[must_use]
|
||||
pub fn to_sorted_union(self, db: &'db dyn Db) -> Self {
|
||||
let mut new_elements = self.elements(db).to_vec();
|
||||
for element in &mut new_elements {
|
||||
if let Type::Intersection(intersection) = element {
|
||||
intersection.sort(db);
|
||||
}
|
||||
}
|
||||
new_elements.sort_unstable_by(union_elements_ordering);
|
||||
UnionType::new(db, new_elements.into_boxed_slice())
|
||||
}
|
||||
|
||||
/// Return `true` if `self` represents the exact same set of possible runtime objects as `other`
|
||||
pub fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
|
||||
/// Inlined version of [`UnionType::is_fully_static`] to avoid having to lookup
|
||||
/// `self.elements` multiple times in the Salsa db in this single method.
|
||||
#[inline]
|
||||
fn all_fully_static(db: &dyn Db, elements: &[Type]) -> bool {
|
||||
elements.iter().all(|ty| ty.is_fully_static(db))
|
||||
}
|
||||
|
||||
let self_elements = self.elements(db);
|
||||
let other_elements = other.elements(db);
|
||||
|
||||
if self_elements.len() != other_elements.len() {
|
||||
return false;
|
||||
}
|
||||
|
||||
if !all_fully_static(db, self_elements) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if !all_fully_static(db, other_elements) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
let sorted_self = self.to_sorted_union(db);
|
||||
|
||||
if sorted_self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
sorted_self == other.to_sorted_union(db)
|
||||
}
|
||||
|
||||
/// Return `true` if `self` has exactly the same set of possible static materializations as `other`
|
||||
/// (if `self` represents the same set of possible sets of possible runtime objects as `other`)
|
||||
pub fn is_gradual_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
|
||||
if self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
// TODO: `T | Unknown` should be gradually equivalent to `T | Unknown | Any`,
|
||||
// since they have exactly the same set of possible static materializations
|
||||
// (they represent the same set of possible sets of possible runtime objects)
|
||||
if self.elements(db).len() != other.elements(db).len() {
|
||||
return false;
|
||||
}
|
||||
|
||||
let sorted_self = self.to_sorted_union(db);
|
||||
|
||||
if sorted_self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
let sorted_other = other.to_sorted_union(db);
|
||||
|
||||
if sorted_self == sorted_other {
|
||||
return true;
|
||||
}
|
||||
|
||||
sorted_self
|
||||
.elements(db)
|
||||
.iter()
|
||||
.zip(sorted_other.elements(db))
|
||||
.all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
|
||||
}
|
||||
}
|
||||
|
||||
#[salsa::interned]
|
||||
|
|
@ -4354,6 +4397,105 @@ pub struct IntersectionType<'db> {
|
|||
negative: FxOrderSet<Type<'db>>,
|
||||
}
|
||||
|
||||
impl<'db> IntersectionType<'db> {
|
||||
/// Return a new `IntersectionType` instance with the positive and negative types sorted
|
||||
/// according to a canonical ordering.
|
||||
#[must_use]
|
||||
pub fn to_sorted_intersection(self, db: &'db dyn Db) -> Self {
|
||||
let mut positive = self.positive(db).clone();
|
||||
positive.sort_unstable_by(union_elements_ordering);
|
||||
|
||||
let mut negative = self.negative(db).clone();
|
||||
negative.sort_unstable_by(union_elements_ordering);
|
||||
|
||||
IntersectionType::new(db, positive, negative)
|
||||
}
|
||||
|
||||
/// Perform an in-place sort of this [`IntersectionType`] instance
|
||||
/// according to a canonical ordering.
|
||||
fn sort(&mut self, db: &'db dyn Db) {
|
||||
*self = self.to_sorted_intersection(db);
|
||||
}
|
||||
|
||||
pub fn is_fully_static(self, db: &'db dyn Db) -> bool {
|
||||
self.positive(db).iter().all(|ty| ty.is_fully_static(db))
|
||||
&& self.negative(db).iter().all(|ty| ty.is_fully_static(db))
|
||||
}
|
||||
|
||||
/// Return `true` if `self` represents exactly the same set of possible runtime objects as `other`
|
||||
pub fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
|
||||
/// Inlined version of [`IntersectionType::is_fully_static`] to avoid having to lookup
|
||||
/// `positive` and `negative` multiple times in the Salsa db in this single method.
|
||||
#[inline]
|
||||
fn all_fully_static(db: &dyn Db, elements: &FxOrderSet<Type>) -> bool {
|
||||
elements.iter().all(|ty| ty.is_fully_static(db))
|
||||
}
|
||||
|
||||
let self_positive = self.positive(db);
|
||||
if !all_fully_static(db, self_positive) {
|
||||
return false;
|
||||
}
|
||||
|
||||
let self_negative = self.negative(db);
|
||||
if !all_fully_static(db, self_negative) {
|
||||
return false;
|
||||
}
|
||||
|
||||
let other_positive = other.positive(db);
|
||||
if !all_fully_static(db, other_positive) {
|
||||
return false;
|
||||
}
|
||||
|
||||
let other_negative = other.negative(db);
|
||||
if !all_fully_static(db, other_negative) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
self_positive.set_eq(other_positive) && self_negative.set_eq(other_negative)
|
||||
}
|
||||
|
||||
/// Return `true` if `self` has exactly the same set of possible static materializations as `other`
|
||||
/// (if `self` represents the same set of possible sets of possible runtime objects as `other`)
|
||||
pub fn is_gradual_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
|
||||
if self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
if self.positive(db).len() != other.positive(db).len()
|
||||
|| self.negative(db).len() != other.negative(db).len()
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
let sorted_self = self.to_sorted_intersection(db);
|
||||
|
||||
if sorted_self == other {
|
||||
return true;
|
||||
}
|
||||
|
||||
let sorted_other = other.to_sorted_intersection(db);
|
||||
|
||||
if sorted_self == sorted_other {
|
||||
return true;
|
||||
}
|
||||
|
||||
sorted_self
|
||||
.positive(db)
|
||||
.iter()
|
||||
.zip(sorted_other.positive(db))
|
||||
.all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
|
||||
&& sorted_self
|
||||
.negative(db)
|
||||
.iter()
|
||||
.zip(sorted_other.negative(db))
|
||||
.all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
|
||||
}
|
||||
}
|
||||
|
||||
#[salsa::interned]
|
||||
pub struct StringLiteralType<'db> {
|
||||
#[return_ref]
|
||||
|
|
|
|||
|
|
@ -219,15 +219,16 @@ macro_rules! type_property_test {
|
|||
};
|
||||
}
|
||||
|
||||
fn intersection<'db>(db: &'db TestDb, s: Type<'db>, t: Type<'db>) -> Type<'db> {
|
||||
IntersectionBuilder::new(db)
|
||||
.add_positive(s)
|
||||
.add_positive(t)
|
||||
.build()
|
||||
fn intersection<'db>(db: &'db TestDb, tys: impl IntoIterator<Item = Type<'db>>) -> Type<'db> {
|
||||
let mut builder = IntersectionBuilder::new(db);
|
||||
for ty in tys {
|
||||
builder = builder.add_positive(ty);
|
||||
}
|
||||
builder.build()
|
||||
}
|
||||
|
||||
fn union<'db>(db: &'db TestDb, s: Type<'db>, t: Type<'db>) -> Type<'db> {
|
||||
UnionType::from_elements(db, [s, t])
|
||||
fn union<'db>(db: &'db TestDb, tys: impl IntoIterator<Item = Type<'db>>) -> Type<'db> {
|
||||
UnionType::from_elements(db, tys)
|
||||
}
|
||||
|
||||
mod stable {
|
||||
|
|
@ -253,6 +254,12 @@ mod stable {
|
|||
forall types s, t, u. s.is_equivalent_to(db, t) && t.is_equivalent_to(db, u) => s.is_equivalent_to(db, u)
|
||||
);
|
||||
|
||||
// Symmetry: If `S` is gradual equivalent to `T`, `T` is gradual equivalent to `S`.
|
||||
type_property_test!(
|
||||
gradual_equivalent_to_is_symmetric, db,
|
||||
forall types s, t. s.is_gradual_equivalent_to(db, t) => t.is_gradual_equivalent_to(db, s)
|
||||
);
|
||||
|
||||
// A fully static type `T` is a subtype of itself.
|
||||
type_property_test!(
|
||||
subtype_of_is_reflexive, db,
|
||||
|
|
@ -265,6 +272,12 @@ mod stable {
|
|||
forall types s, t, u. s.is_subtype_of(db, t) && t.is_subtype_of(db, u) => s.is_subtype_of(db, u)
|
||||
);
|
||||
|
||||
// `S <: T` and `T <: S` implies that `S` is equivalent to `T`.
|
||||
type_property_test!(
|
||||
subtype_of_is_antisymmetric, db,
|
||||
forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t)
|
||||
);
|
||||
|
||||
// `T` is not disjoint from itself, unless `T` is `Never`.
|
||||
type_property_test!(
|
||||
disjoint_from_is_irreflexive, db,
|
||||
|
|
@ -336,7 +349,7 @@ mod stable {
|
|||
all_fully_static_type_pairs_are_subtype_of_their_union, db,
|
||||
forall types s, t.
|
||||
s.is_fully_static(db) && t.is_fully_static(db)
|
||||
=> s.is_subtype_of(db, union(db, s, t)) && t.is_subtype_of(db, union(db, s, t))
|
||||
=> s.is_subtype_of(db, union(db, [s, t])) && t.is_subtype_of(db, union(db, [s, t]))
|
||||
);
|
||||
}
|
||||
|
||||
|
|
@ -348,6 +361,8 @@ mod stable {
|
|||
/// tests to the `stable` section. In the meantime, it can still be useful to run these
|
||||
/// tests (using [`types::property_tests::flaky`]), to see if there are any new obvious bugs.
|
||||
mod flaky {
|
||||
use itertools::Itertools;
|
||||
|
||||
use super::{intersection, union};
|
||||
|
||||
// Currently fails due to https://github.com/astral-sh/ruff/issues/14899
|
||||
|
|
@ -357,13 +372,6 @@ mod flaky {
|
|||
forall types t. t.is_assignable_to(db, t)
|
||||
);
|
||||
|
||||
// `S <: T` and `T <: S` implies that `S` is equivalent to `T`.
|
||||
// This very often passes now, but occasionally flakes due to https://github.com/astral-sh/ruff/issues/15380
|
||||
type_property_test!(
|
||||
subtype_of_is_antisymmetric, db,
|
||||
forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t)
|
||||
);
|
||||
|
||||
// Negating `T` twice is equivalent to `T`.
|
||||
type_property_test!(
|
||||
double_negation_is_identity, db,
|
||||
|
|
@ -387,7 +395,7 @@ mod flaky {
|
|||
all_fully_static_type_pairs_are_supertypes_of_their_intersection, db,
|
||||
forall types s, t.
|
||||
s.is_fully_static(db) && t.is_fully_static(db)
|
||||
=> intersection(db, s, t).is_subtype_of(db, s) && intersection(db, s, t).is_subtype_of(db, t)
|
||||
=> intersection(db, [s, t]).is_subtype_of(db, s) && intersection(db, [s, t]).is_subtype_of(db, t)
|
||||
);
|
||||
|
||||
// And for non-fully-static types, the intersection of a pair of types
|
||||
|
|
@ -395,20 +403,42 @@ mod flaky {
|
|||
// Currently fails due to https://github.com/astral-sh/ruff/issues/14899
|
||||
type_property_test!(
|
||||
all_type_pairs_can_be_assigned_from_their_intersection, db,
|
||||
forall types s, t. intersection(db, s, t).is_assignable_to(db, s) && intersection(db, s, t).is_assignable_to(db, t)
|
||||
forall types s, t. intersection(db, [s, t]).is_assignable_to(db, s) && intersection(db, [s, t]).is_assignable_to(db, t)
|
||||
);
|
||||
|
||||
// For *any* pair of types, whether fully static or not,
|
||||
// each of the pair should be assignable to the union of the two.
|
||||
type_property_test!(
|
||||
all_type_pairs_are_assignable_to_their_union, db,
|
||||
forall types s, t. s.is_assignable_to(db, union(db, s, t)) && t.is_assignable_to(db, union(db, s, t))
|
||||
forall types s, t. s.is_assignable_to(db, union(db, [s, t])) && t.is_assignable_to(db, union(db, [s, t]))
|
||||
);
|
||||
|
||||
// Symmetry: If `S` is gradual equivalent to `T`, `T` is gradual equivalent to `S`.
|
||||
// Equal element sets of intersections implies equivalence
|
||||
// flaky at least in part because of https://github.com/astral-sh/ruff/issues/15513
|
||||
type_property_test!(
|
||||
gradual_equivalent_to_is_symmetric, db,
|
||||
forall types s, t. s.is_gradual_equivalent_to(db, t) => t.is_gradual_equivalent_to(db, s)
|
||||
intersection_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| intersection(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_intersections| vec_of_intersections[0].is_equivalent_to(db, vec_of_intersections[1]))
|
||||
);
|
||||
|
||||
// Equal element sets of unions implies equivalence
|
||||
// flaky at laest in part because of https://github.com/astral-sh/ruff/issues/15513
|
||||
type_property_test!(
|
||||
union_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| union(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_unions| vec_of_unions[0].is_equivalent_to(db, vec_of_unions[1]))
|
||||
);
|
||||
|
||||
// A fully static type does not have any materializations.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,266 @@
|
|||
use std::cmp::Ordering;
|
||||
|
||||
use super::{
|
||||
class_base::ClassBase, ClassLiteralType, DynamicType, InstanceType, KnownInstanceType,
|
||||
TodoType, Type,
|
||||
};
|
||||
|
||||
/// Return an [`Ordering`] that describes the canonical order in which two types should appear
|
||||
/// 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.
|
||||
///
|
||||
/// ## Why not just implement [`Ord`] on [`Type`]?
|
||||
///
|
||||
/// It would be fairly easy to slap `#[derive(PartialOrd, Ord)]` on [`Type`], and the ordering we
|
||||
/// 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 {
|
||||
if left == right {
|
||||
return Ordering::Equal;
|
||||
}
|
||||
|
||||
match (left, right) {
|
||||
(Type::Never, _) => Ordering::Less,
|
||||
(_, Type::Never) => Ordering::Greater,
|
||||
|
||||
(Type::LiteralString, _) => Ordering::Less,
|
||||
(_, Type::LiteralString) => Ordering::Greater,
|
||||
|
||||
(Type::BooleanLiteral(left), Type::BooleanLiteral(right)) => left.cmp(right),
|
||||
(Type::BooleanLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::BooleanLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::IntLiteral(left), Type::IntLiteral(right)) => left.cmp(right),
|
||||
(Type::IntLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::IntLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::StringLiteral(left), Type::StringLiteral(right)) => left.cmp(right),
|
||||
(Type::StringLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::StringLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::BytesLiteral(left), Type::BytesLiteral(right)) => left.cmp(right),
|
||||
(Type::BytesLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::BytesLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::SliceLiteral(left), Type::SliceLiteral(right)) => left.cmp(right),
|
||||
(Type::SliceLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::SliceLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::FunctionLiteral(left), Type::FunctionLiteral(right)) => left.cmp(right),
|
||||
(Type::FunctionLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::FunctionLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::Tuple(left), Type::Tuple(right)) => left.cmp(right),
|
||||
(Type::Tuple(_), _) => Ordering::Less,
|
||||
(_, Type::Tuple(_)) => Ordering::Greater,
|
||||
|
||||
(Type::ModuleLiteral(left), Type::ModuleLiteral(right)) => left.cmp(right),
|
||||
(Type::ModuleLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::ModuleLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(
|
||||
Type::ClassLiteral(ClassLiteralType { class: left }),
|
||||
Type::ClassLiteral(ClassLiteralType { class: right }),
|
||||
) => left.cmp(right),
|
||||
(Type::ClassLiteral(_), _) => Ordering::Less,
|
||||
(_, Type::ClassLiteral(_)) => Ordering::Greater,
|
||||
|
||||
(Type::SubclassOf(left), Type::SubclassOf(right)) => {
|
||||
match (left.subclass_of(), right.subclass_of()) {
|
||||
(ClassBase::Class(left), ClassBase::Class(right)) => left.cmp(&right),
|
||||
(ClassBase::Class(_), _) => Ordering::Less,
|
||||
(_, ClassBase::Class(_)) => Ordering::Greater,
|
||||
(ClassBase::Dynamic(left), ClassBase::Dynamic(right)) => {
|
||||
dynamic_elements_ordering(left, right)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
(Type::SubclassOf(_), _) => Ordering::Less,
|
||||
(_, Type::SubclassOf(_)) => Ordering::Greater,
|
||||
(
|
||||
Type::Instance(InstanceType { class: left }),
|
||||
Type::Instance(InstanceType { class: right }),
|
||||
) => left.cmp(right),
|
||||
|
||||
(Type::Instance(_), _) => Ordering::Less,
|
||||
(_, Type::Instance(_)) => Ordering::Greater,
|
||||
|
||||
(Type::AlwaysTruthy, _) => Ordering::Less,
|
||||
(_, Type::AlwaysTruthy) => Ordering::Greater,
|
||||
|
||||
(Type::AlwaysFalsy, _) => Ordering::Less,
|
||||
(_, Type::AlwaysFalsy) => Ordering::Greater,
|
||||
|
||||
(Type::KnownInstance(left_instance), Type::KnownInstance(right_instance)) => {
|
||||
match (left_instance, right_instance) {
|
||||
(KnownInstanceType::Any, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Any) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Tuple, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Tuple) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::AlwaysFalsy, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::AlwaysFalsy) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::AlwaysTruthy, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::AlwaysTruthy) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Annotated, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Annotated) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Callable, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Callable) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::ChainMap, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::ChainMap) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::ClassVar, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::ClassVar) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Concatenate, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Concatenate) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Counter, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Counter) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::DefaultDict, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::DefaultDict) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Deque, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Deque) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Dict, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Dict) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Final, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Final) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::FrozenSet, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::FrozenSet) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypeGuard, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypeGuard) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::List, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::List) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Literal, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Literal) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::LiteralString, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::LiteralString) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Optional, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Optional) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::OrderedDict, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::OrderedDict) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::NoReturn, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::NoReturn) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Never, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Never) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Set, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Set) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Type, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Type) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypeAlias, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypeAlias) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Unknown, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Unknown) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Not, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Not) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Intersection, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Intersection) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypeOf, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypeOf) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Unpack, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Unpack) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypingSelf, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypingSelf) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Required, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Required) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::NotRequired, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::NotRequired) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypeIs, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypeIs) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::ReadOnly, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::ReadOnly) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::Union, _) => Ordering::Less,
|
||||
(_, KnownInstanceType::Union) => Ordering::Greater,
|
||||
|
||||
(
|
||||
KnownInstanceType::TypeAliasType(left),
|
||||
KnownInstanceType::TypeAliasType(right),
|
||||
) => left.cmp(right),
|
||||
(KnownInstanceType::TypeAliasType(_), _) => Ordering::Less,
|
||||
(_, KnownInstanceType::TypeAliasType(_)) => Ordering::Greater,
|
||||
|
||||
(KnownInstanceType::TypeVar(left), KnownInstanceType::TypeVar(right)) => {
|
||||
left.cmp(right)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
(Type::KnownInstance(_), _) => Ordering::Less,
|
||||
(_, Type::KnownInstance(_)) => Ordering::Greater,
|
||||
|
||||
(Type::Dynamic(left), Type::Dynamic(right)) => dynamic_elements_ordering(*left, *right),
|
||||
(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::Intersection(left), Type::Intersection(right)) => left.cmp(right),
|
||||
}
|
||||
}
|
||||
|
||||
/// Determine a canonical order for two instances of [`DynamicType`].
|
||||
fn dynamic_elements_ordering(left: DynamicType, right: DynamicType) -> Ordering {
|
||||
match (left, right) {
|
||||
(DynamicType::Any, _) => Ordering::Less,
|
||||
(_, DynamicType::Any) => Ordering::Greater,
|
||||
|
||||
(DynamicType::Unknown, _) => Ordering::Less,
|
||||
(_, DynamicType::Unknown) => Ordering::Greater,
|
||||
|
||||
#[cfg(debug_assertions)]
|
||||
(DynamicType::Todo(left), DynamicType::Todo(right)) => match (left, right) {
|
||||
(
|
||||
TodoType::FileAndLine(left_file, left_line),
|
||||
TodoType::FileAndLine(right_file, right_line),
|
||||
) => left_file
|
||||
.cmp(right_file)
|
||||
.then_with(|| left_line.cmp(&right_line)),
|
||||
(TodoType::FileAndLine(..), _) => Ordering::Less,
|
||||
(_, TodoType::FileAndLine(..)) => Ordering::Greater,
|
||||
|
||||
(TodoType::Message(left), TodoType::Message(right)) => left.cmp(right),
|
||||
},
|
||||
|
||||
#[cfg(not(debug_assertions))]
|
||||
(DynamicType::Todo(TodoType), DynamicType::Todo(TodoType)) => Ordering::Equal,
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue