diff --git a/crates/red_knot_python_semantic/resources/mdtest/comparison/tuples.md b/crates/red_knot_python_semantic/resources/mdtest/comparison/tuples.md index 8fe7f29541a9a..250ded168f8a7 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/comparison/tuples.md +++ b/crates/red_knot_python_semantic/resources/mdtest/comparison/tuples.md @@ -58,7 +58,22 @@ reveal_type(c >= d) # revealed: Literal[True] #### Results with Ambiguity ```py -def _(x: bool, y: int): +class P: + def __lt__(self, other: "P") -> bool: + return True + + def __le__(self, other: "P") -> bool: + return True + + def __gt__(self, other: "P") -> bool: + return True + + def __ge__(self, other: "P") -> bool: + return True + +class Q(P): ... + +def _(x: P, y: Q): a = (x,) b = (y,) diff --git a/crates/red_knot_python_semantic/resources/mdtest/exception/control_flow.md b/crates/red_knot_python_semantic/resources/mdtest/exception/control_flow.md index 284b0f24d5620..a6e703dff5b6e 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/exception/control_flow.md +++ b/crates/red_knot_python_semantic/resources/mdtest/exception/control_flow.md @@ -455,9 +455,9 @@ else: reveal_type(x) # revealed: slice finally: # TODO: should be `Literal[1] | str | bytes | bool | memoryview | float | range | slice` - reveal_type(x) # revealed: bool | float | slice + reveal_type(x) # revealed: bool | slice | float -reveal_type(x) # revealed: bool | float | slice +reveal_type(x) # revealed: bool | slice | float ``` ## Nested `try`/`except` blocks @@ -534,7 +534,7 @@ try: reveal_type(x) # revealed: slice finally: # TODO: should be `Literal[1] | str | bytes | bool | memoryview | float | range | slice` - reveal_type(x) # revealed: bool | float | slice + reveal_type(x) # revealed: bool | slice | float x = 2 reveal_type(x) # revealed: Literal[2] reveal_type(x) # revealed: Literal[2] diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/truthiness.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/truthiness.md index b3975c1a813b7..b1129498ce176 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/narrow/truthiness.md +++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/truthiness.md @@ -21,22 +21,22 @@ else: if x and not x: reveal_type(x) # revealed: Never else: - reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()] + reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None if not (x and not x): - reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()] + reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None else: reveal_type(x) # revealed: Never if x or not x: - reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()] + reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None else: reveal_type(x) # revealed: Never if not (x or not x): reveal_type(x) # revealed: Never else: - reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()] + reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None if (isinstance(x, int) or isinstance(x, str)) and x: reveal_type(x) # revealed: Literal[-1, True, "foo"] diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md index 06ee56aaf0d5f..e51cc4dcaae8e 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md @@ -346,4 +346,16 @@ static_assert(is_assignable_to(Never, type[str])) static_assert(is_assignable_to(Never, type[Any])) ``` +### `bool` is assignable to unions that include `bool` + +Since we decompose `bool` to `Literal[True, False]` in unions, it would be surprisingly easy to get +this wrong if we forgot to normalize `bool` to `Literal[True, False]` when it appeared on the +left-hand side in `Type::is_assignable_to()`. + +```py +from knot_extensions import is_assignable_to, static_assert + +static_assert(is_assignable_to(bool, str | bool)) +``` + [typing documentation]: https://typing.readthedocs.io/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md index 047a45fc2fd0b..b607b05f1b663 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md @@ -118,4 +118,48 @@ class R: ... static_assert(is_equivalent_to(Intersection[tuple[P | Q], R], Intersection[tuple[Q | P], R])) ``` +## Unions containing tuples containing `bool` + +```py +from knot_extensions import is_equivalent_to, static_assert +from typing_extensions import Literal + +class P: ... + +static_assert(is_equivalent_to(tuple[Literal[True, False]] | P, tuple[bool] | P)) +static_assert(is_equivalent_to(P | tuple[bool], P | tuple[Literal[True, False]])) +``` + +## Unions and intersections involving `AlwaysTruthy`, `bool` and `AlwaysFalsy` + +```py +from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to, Not +from typing_extensions import Literal + +static_assert(is_equivalent_to(AlwaysTruthy | bool, Literal[False] | AlwaysTruthy)) +static_assert(is_equivalent_to(AlwaysFalsy | bool, Literal[True] | AlwaysFalsy)) +static_assert(is_equivalent_to(Not[AlwaysTruthy] | bool, Not[AlwaysTruthy] | Literal[True])) +static_assert(is_equivalent_to(Not[AlwaysFalsy] | bool, Literal[False] | Not[AlwaysFalsy])) +``` + +## Unions and intersections involving `AlwaysTruthy`, `LiteralString` and `AlwaysFalsy` + +```py +from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to, Not, Intersection +from typing_extensions import Literal, LiteralString + +# TODO: these should all pass! + +# error: [static-assert-error] +static_assert(is_equivalent_to(AlwaysTruthy | LiteralString, Literal[""] | AlwaysTruthy)) +# error: [static-assert-error] +static_assert(is_equivalent_to(AlwaysFalsy | LiteralString, Intersection[LiteralString, Not[Literal[""]]] | AlwaysFalsy)) +# error: [static-assert-error] +static_assert(is_equivalent_to(Not[AlwaysFalsy] | LiteralString, Literal[""] | Not[AlwaysFalsy])) +# error: [static-assert-error] +static_assert( + is_equivalent_to(Not[AlwaysTruthy] | LiteralString, Not[AlwaysTruthy] | Intersection[LiteralString, Not[Literal[""]]]) +) +``` + [the equivalence relation]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md index 4e081338d38bc..c120023f819a3 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md @@ -449,5 +449,31 @@ static_assert(not is_subtype_of(Intersection[Unknown, int], int)) static_assert(not is_subtype_of(tuple[int, int], tuple[int, Unknown])) ``` +## `bool` is a subtype of `AlwaysTruthy | AlwaysFalsy` + +`bool` is equivalent to `Literal[True] | Literal[False]`. `Literal[True]` is a subtype of +`AlwaysTruthy` and `Literal[False]` is a subtype of `AlwaysFalsy`; it therefore stands to reason +that `bool` is a subtype of `AlwaysTruthy | AlwaysFalsy`. + +```py +from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert, Not, is_disjoint_from +from typing_extensions import Literal + +static_assert(is_subtype_of(bool, AlwaysTruthy | AlwaysFalsy)) + +# the inverse also applies -- TODO: this should pass! +# See the TODO comments in the `Type::Intersection` branch of `Type::is_disjoint_from()`. +static_assert(is_disjoint_from(bool, Not[AlwaysTruthy | AlwaysFalsy])) # error: [static-assert-error] + +# `Type::is_subtype_of` delegates many questions of `bool` subtyping to `int`, +# but set-theoretic types like intersections and unions are still handled differently to `int` +static_assert(is_subtype_of(Literal[True], Not[Literal[2]])) +static_assert(is_subtype_of(bool, Not[Literal[2]])) +static_assert(is_subtype_of(Literal[True], bool | None)) +static_assert(is_subtype_of(bool, bool | None)) + +static_assert(not is_subtype_of(int, Not[Literal[2]])) +``` + [special case for float and complex]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex [typing documentation]: https://typing.readthedocs.io/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index a056c176c7cd0..893ad9f9f738c 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -811,6 +811,31 @@ impl<'db> Type<'db> { } } + /// Normalize the type `bool` -> `Literal[True, False]`. + /// + /// Using this method in various type-relational methods + /// ensures that the following invariants hold true: + /// + /// - bool ≡ Literal[True, False] + /// - bool | T ≡ Literal[True, False] | T + /// - bool <: Literal[True, False] + /// - bool | T <: Literal[True, False] | T + /// - Literal[True, False] <: bool + /// - Literal[True, False] | T <: bool | T + #[must_use] + pub fn with_normalized_bools(self, db: &'db dyn Db) -> Self { + const LITERAL_BOOLS: [Type; 2] = [Type::BooleanLiteral(false), Type::BooleanLiteral(true)]; + + match self { + Type::Instance(InstanceType { class }) if class.is_known(db, KnownClass::Bool) => { + Type::Union(UnionType::new(db, Box::from(LITERAL_BOOLS))) + } + // TODO: decompose `LiteralString` into `Literal[""] | TruthyLiteralString`? + // We'd need to rename this method... --Alex + _ => self, + } + } + /// Return a normalized version of `self` in which all unions and intersections are sorted /// according to a canonical order, no matter how "deeply" a union/intersection may be nested. #[must_use] @@ -859,6 +884,12 @@ impl<'db> Type<'db> { return true; } + let normalized_self = self.with_normalized_bools(db); + let normalized_target = target.with_normalized_bools(db); + if normalized_self != self || normalized_target != target { + return normalized_self.is_subtype_of(db, normalized_target); + } + // Non-fully-static types do not participate in subtyping. // // Type `A` can only be a subtype of type `B` if the set of possible runtime objects @@ -961,7 +992,7 @@ impl<'db> Type<'db> { KnownClass::Str.to_instance(db).is_subtype_of(db, target) } (Type::BooleanLiteral(_), _) => { - KnownClass::Bool.to_instance(db).is_subtype_of(db, target) + KnownClass::Int.to_instance(db).is_subtype_of(db, target) } (Type::IntLiteral(_), _) => KnownClass::Int.to_instance(db).is_subtype_of(db, target), (Type::BytesLiteral(_), _) => { @@ -1077,6 +1108,11 @@ impl<'db> Type<'db> { if self.is_gradual_equivalent_to(db, target) { return true; } + let normalized_self = self.with_normalized_bools(db); + let normalized_target = target.with_normalized_bools(db); + if normalized_self != self || normalized_target != target { + return normalized_self.is_assignable_to(db, normalized_target); + } match (self, target) { // Never can be assigned to any type. (Type::Never, _) => true, @@ -1177,6 +1213,13 @@ impl<'db> Type<'db> { pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool { // TODO equivalent but not identical types: TypedDicts, Protocols, type aliases, etc. + let normalized_self = self.with_normalized_bools(db); + let normalized_other = other.with_normalized_bools(db); + + if normalized_self != self || normalized_other != other { + return normalized_self.is_equivalent_to(db, normalized_other); + } + match (self, other) { (Type::Union(left), Type::Union(right)) => left.is_equivalent_to(db, right), (Type::Intersection(left), Type::Intersection(right)) => { @@ -1218,6 +1261,13 @@ impl<'db> Type<'db> { /// /// [Summary of type relations]: https://typing.readthedocs.io/en/latest/spec/concepts.html#summary-of-type-relations pub(crate) fn is_gradual_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool { + let normalized_self = self.with_normalized_bools(db); + let normalized_other = other.with_normalized_bools(db); + + if normalized_self != self || normalized_other != other { + return normalized_self.is_gradual_equivalent_to(db, normalized_other); + } + if self == other { return true; } @@ -1250,6 +1300,12 @@ impl<'db> Type<'db> { /// Note: This function aims to have no false positives, but might return /// wrong `false` answers in some cases. pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool { + let normalized_self = self.with_normalized_bools(db); + let normalized_other = other.with_normalized_bools(db); + if normalized_self != self || normalized_other != other { + return normalized_self.is_disjoint_from(db, normalized_other); + } + match (self, other) { (Type::Never, _) | (_, Type::Never) => true, @@ -4642,18 +4698,19 @@ pub struct TupleType<'db> { } impl<'db> TupleType<'db> { - pub fn from_elements>>( - db: &'db dyn Db, - types: impl IntoIterator, - ) -> Type<'db> { + pub fn from_elements(db: &'db dyn Db, types: I) -> Type<'db> + where + I: IntoIterator, + T: Into>, + { let mut elements = vec![]; for ty in types { - let ty = ty.into(); + let ty: Type<'db> = ty.into(); if ty.is_never() { return Type::Never; } - elements.push(ty); + elements.push(ty.with_normalized_bools(db)); } Type::Tuple(Self::new(db, elements.into_boxed_slice())) diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs index c19a4f06cefa4..51cefb7db3323 100644 --- a/crates/red_knot_python_semantic/src/types/builder.rs +++ b/crates/red_knot_python_semantic/src/types/builder.rs @@ -26,7 +26,7 @@ //! eliminate the supertype from the intersection). //! * An intersection containing two non-overlapping types should simplify to [`Type::Never`]. -use crate::types::{InstanceType, IntersectionType, KnownClass, Type, UnionType}; +use crate::types::{IntersectionType, KnownClass, Type, UnionType}; use crate::{Db, FxOrderSet}; use smallvec::SmallVec; @@ -45,6 +45,7 @@ impl<'db> UnionBuilder<'db> { /// Adds a type to this union. pub(crate) fn add(mut self, ty: Type<'db>) -> Self { + let ty = ty.with_normalized_bools(self.db); match ty { Type::Union(union) => { let new_elements = union.elements(self.db); @@ -55,27 +56,10 @@ impl<'db> UnionBuilder<'db> { } Type::Never => {} _ => { - let bool_pair = if let Type::BooleanLiteral(b) = ty { - Some(Type::BooleanLiteral(!b)) - } else { - None - }; - - let mut to_add = ty; let mut to_remove = SmallVec::<[usize; 2]>::new(); let ty_negated = ty.negate(self.db); for (index, element) in self.elements.iter().enumerate() { - if Some(*element) == bool_pair { - to_add = KnownClass::Bool.to_instance(self.db); - to_remove.push(index); - // The type we are adding is a BooleanLiteral, which doesn't have any - // subtypes. And we just found that the union already contained our - // mirror-image BooleanLiteral, so it can't also contain bool or any - // supertype of bool. Therefore, we are done. - break; - } - if ty.is_same_gradual_form(*element) || ty.is_subtype_of(self.db, *element) { return self; } else if element.is_subtype_of(self.db, ty) { @@ -94,8 +78,8 @@ impl<'db> UnionBuilder<'db> { } } match to_remove[..] { - [] => self.elements.push(to_add), - [index] => self.elements[index] = to_add, + [] => self.elements.push(ty), + [index] => self.elements[index] = ty, _ => { let mut current_index = 0; let mut to_remove = to_remove.into_iter(); @@ -110,7 +94,7 @@ impl<'db> UnionBuilder<'db> { current_index += 1; retain }); - self.elements.push(to_add); + self.elements.push(ty); } } } @@ -154,6 +138,7 @@ impl<'db> IntersectionBuilder<'db> { } pub(crate) fn add_positive(mut self, ty: Type<'db>) -> Self { + let ty = ty.with_normalized_bools(self.db); if let Type::Union(union) = ty { // Distribute ourself over this union: for each union element, clone ourself and // intersect with that union element, then create a new union-of-intersections with all @@ -183,6 +168,9 @@ impl<'db> IntersectionBuilder<'db> { pub(crate) fn add_negative(mut self, ty: Type<'db>) -> Self { // See comments above in `add_positive`; this is just the negated version. + + let ty = ty.with_normalized_bools(self.db); + if let Type::Union(union) = ty { for elem in union.elements(self.db) { self = self.add_negative(*elem); @@ -246,7 +234,7 @@ struct InnerIntersectionBuilder<'db> { impl<'db> InnerIntersectionBuilder<'db> { /// Adds a positive type to this intersection. - fn add_positive(&mut self, db: &'db dyn Db, mut new_positive: Type<'db>) { + fn add_positive(&mut self, db: &'db dyn Db, new_positive: Type<'db>) { match new_positive { // `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]` Type::AlwaysTruthy if self.positive.contains(&Type::LiteralString) => { @@ -293,62 +281,6 @@ impl<'db> InnerIntersectionBuilder<'db> { return; } - let addition_is_bool_instance = known_instance == Some(KnownClass::Bool); - - for (index, existing_positive) in self.positive.iter().enumerate() { - match existing_positive { - // `AlwaysTruthy & bool` -> `Literal[True]` - Type::AlwaysTruthy if addition_is_bool_instance => { - new_positive = Type::BooleanLiteral(true); - } - // `AlwaysFalsy & bool` -> `Literal[False]` - Type::AlwaysFalsy if addition_is_bool_instance => { - new_positive = Type::BooleanLiteral(false); - } - Type::Instance(InstanceType { class }) - if class.is_known(db, KnownClass::Bool) => - { - match new_positive { - // `bool & AlwaysTruthy` -> `Literal[True]` - Type::AlwaysTruthy => { - new_positive = Type::BooleanLiteral(true); - } - // `bool & AlwaysFalsy` -> `Literal[False]` - Type::AlwaysFalsy => { - new_positive = Type::BooleanLiteral(false); - } - _ => continue, - } - } - _ => continue, - } - self.positive.swap_remove_index(index); - break; - } - - if addition_is_bool_instance { - for (index, existing_negative) in self.negative.iter().enumerate() { - match existing_negative { - // `bool & ~Literal[False]` -> `Literal[True]` - // `bool & ~Literal[True]` -> `Literal[False]` - Type::BooleanLiteral(bool_value) => { - new_positive = Type::BooleanLiteral(!bool_value); - } - // `bool & ~AlwaysTruthy` -> `Literal[False]` - Type::AlwaysTruthy => { - new_positive = Type::BooleanLiteral(false); - } - // `bool & ~AlwaysFalsy` -> `Literal[True]` - Type::AlwaysFalsy => { - new_positive = Type::BooleanLiteral(true); - } - _ => continue, - } - self.negative.swap_remove_index(index); - break; - } - } - let mut to_remove = SmallVec::<[usize; 1]>::new(); for (index, existing_positive) in self.positive.iter().enumerate() { // S & T = S if S <: T @@ -396,14 +328,6 @@ impl<'db> InnerIntersectionBuilder<'db> { /// Adds a negative type to this intersection. fn add_negative(&mut self, db: &'db dyn Db, new_negative: Type<'db>) { - let contains_bool = || { - self.positive - .iter() - .filter_map(|ty| ty.into_instance()) - .filter_map(|instance| instance.class.known(db)) - .any(KnownClass::is_bool) - }; - match new_negative { Type::Intersection(inter) => { for pos in inter.positive(db) { @@ -427,20 +351,10 @@ impl<'db> InnerIntersectionBuilder<'db> { // simplify the representation. self.add_positive(db, ty); } - // `bool & ~AlwaysTruthy` -> `bool & Literal[False]` - // `bool & ~Literal[True]` -> `bool & Literal[False]` - Type::AlwaysTruthy | Type::BooleanLiteral(true) if contains_bool() => { - self.add_positive(db, Type::BooleanLiteral(false)); - } // `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]` Type::AlwaysTruthy if self.positive.contains(&Type::LiteralString) => { self.add_positive(db, Type::string_literal(db, "")); } - // `bool & ~AlwaysFalsy` -> `bool & Literal[True]` - // `bool & ~Literal[False]` -> `bool & Literal[True]` - Type::AlwaysFalsy | Type::BooleanLiteral(false) if contains_bool() => { - self.add_positive(db, Type::BooleanLiteral(true)); - } // `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]` Type::AlwaysFalsy if self.positive.contains(&Type::LiteralString) => { self.add_negative(db, Type::string_literal(db, "")); diff --git a/crates/red_knot_python_semantic/src/types/display.rs b/crates/red_knot_python_semantic/src/types/display.rs index 50c3ae1fff8cb..8769c8e021242 100644 --- a/crates/red_knot_python_semantic/src/types/display.rs +++ b/crates/red_knot_python_semantic/src/types/display.rs @@ -1,5 +1,6 @@ //! Display implementations for types. +use std::borrow::Cow; use std::fmt::{self, Display, Formatter, Write}; use ruff_db::display::FormatterJoinExtension; @@ -151,12 +152,31 @@ struct DisplayUnionType<'db> { impl Display for DisplayUnionType<'_> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let elements = self.ty.elements(self.db); + let mut elements = Cow::Borrowed(self.ty.elements(self.db)); + + if let Some(literal_false_pos) = elements + .iter() + .position(|ty| matches!(ty, Type::BooleanLiteral(false))) + { + if let Some(literal_true_pos) = elements + .iter() + .position(|ty| matches!(ty, Type::BooleanLiteral(true))) + { + let (min, max) = if literal_false_pos < literal_true_pos { + (literal_false_pos, literal_true_pos) + } else { + (literal_true_pos, literal_false_pos) + }; + let mutable_elements = elements.to_mut(); + mutable_elements.swap_remove(max); + mutable_elements[min] = KnownClass::Bool.to_instance(self.db); + } + } // Group condensed-display types by kind. let mut grouped_condensed_kinds = FxHashMap::default(); - for element in elements { + for element in &*elements { if let Ok(kind) = CondensedDisplayTypeKind::try_from(*element) { grouped_condensed_kinds .entry(kind) @@ -167,7 +187,7 @@ impl Display for DisplayUnionType<'_> { let mut join = f.join(" | "); - for element in elements { + for element in &*elements { if let Ok(kind) = CondensedDisplayTypeKind::try_from(*element) { let Some(condensed_kind) = grouped_condensed_kinds.remove(&kind) else { continue; 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 5f6e8edf06ce3..f4471826cc4d4 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -328,8 +328,9 @@ fn union<'db>(db: &'db TestDb, tys: impl IntoIterator>) -> Type } mod stable { - use super::union; + use super::{intersection, union}; use crate::types::{KnownClass, Type}; + use itertools::Itertools; // Reflexivity: `T` is equivalent to itself. type_property_test!( @@ -474,6 +475,32 @@ mod stable { 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])) ); + + // Equal element sets of intersections implies equivalence + type_property_test!( + 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 + 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])) + ); } /// This module contains property tests that currently lead to many false positives. @@ -484,8 +511,6 @@ 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}; // Negating `T` twice is equivalent to `T`. @@ -522,34 +547,6 @@ mod flaky { forall types s, t. intersection(db, [s, t]).is_assignable_to(db, s) && intersection(db, [s, t]).is_assignable_to(db, t) ); - // 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!( - 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])) - ); - // `S | T` is always a supertype of `S`. // Thus, `S` is never disjoint from `S | T`. type_property_test!(