Compare commits

...

5 Commits

Author SHA1 Message Date
Alex Waygood
1ef2f73820 any better 2025-01-28 18:32:53 +00:00
Alex Waygood
91784bbe93 is this faster 2025-01-28 14:19:18 +00:00
Alex Waygood
80136d81f6 take 7? 2025-01-28 13:26:05 +00:00
Alex Waygood
2851098c36 Add missing test coverage for the changes to is_subtype_of and is_assignable_to 2025-01-28 12:15:42 +00:00
Alex Waygood
84fdb04049 [red-knot] Decompose bool to Literal[True, False] in unions and intersections 2025-01-28 12:15:42 +00:00
8 changed files with 266 additions and 178 deletions

View File

@@ -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]

View File

@@ -11,37 +11,37 @@ x = foo()
if x:
reveal_type(x) # revealed: Literal[-1, True, "foo", b"bar"]
else:
reveal_type(x) # revealed: Literal[0, False, "", b""] | None | tuple[()]
reveal_type(x) # revealed: Literal[0, False, "", b""] | tuple[()] | None
if not x:
reveal_type(x) # revealed: Literal[0, False, "", b""] | None | tuple[()]
reveal_type(x) # revealed: Literal[0, False, "", b""] | tuple[()] | None
else:
reveal_type(x) # revealed: Literal[-1, True, "foo", b"bar"]
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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | bool | tuple[()] | None
if (isinstance(x, int) or isinstance(x, str)) and x:
reveal_type(x) # revealed: Literal[-1, True, "foo"]
else:
reveal_type(x) # revealed: Literal[b"", b"bar", 0, False, ""] | None | tuple[()]
reveal_type(x) # revealed: tuple[()] | None | Literal[b"", b"bar", 0, False, ""]
```
## Function Literals

View File

@@ -346,4 +346,24 @@ 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))
```
### `bool` is assignable to `AlwaysTruthy | AlwaysFalsy`
```py
from knot_extensions import static_assert, is_assignable_to, AlwaysTruthy, AlwaysFalsy
static_assert(is_assignable_to(bool, AlwaysTruthy | AlwaysFalsy))
```
[typing documentation]: https://typing.readthedocs.io/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation

View File

@@ -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

View File

@@ -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

View File

@@ -881,6 +881,15 @@ impl<'db> Type<'db> {
(Type::Never, _) => true,
(_, Type::Never) => false,
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
Type::BooleanLiteral(true).is_subtype_of(db, target)
&& Type::BooleanLiteral(false).is_subtype_of(db, target)
}
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
self.is_subtype_of(db, Type::BooleanLiteral(true))
|| self.is_subtype_of(db, Type::BooleanLiteral(false))
}
(Type::Union(union), _) => union
.elements(db)
.iter()
@@ -961,7 +970,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 +1086,7 @@ impl<'db> Type<'db> {
if self.is_gradual_equivalent_to(db, target) {
return true;
}
match (self, target) {
// Never can be assigned to any type.
(Type::Never, _) => true,
@@ -1093,6 +1103,15 @@ impl<'db> Type<'db> {
true
}
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
Type::BooleanLiteral(true).is_assignable_to(db, target)
&& Type::BooleanLiteral(false).is_assignable_to(db, target)
}
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
self.is_assignable_to(db, Type::BooleanLiteral(false))
|| self.is_assignable_to(db, Type::BooleanLiteral(true))
}
// A union is assignable to a type T iff every element of the union is assignable to T.
(Type::Union(union), ty) => union
.elements(db)

View File

@@ -33,6 +33,7 @@ use smallvec::SmallVec;
pub(crate) struct UnionBuilder<'db> {
elements: Vec<Type<'db>>,
db: &'db dyn Db,
bool_literals_present: BoolLiteralsPresent,
}
impl<'db> UnionBuilder<'db> {
@@ -40,6 +41,7 @@ impl<'db> UnionBuilder<'db> {
Self {
db,
elements: vec![],
bool_literals_present: BoolLiteralsPresent::Zero,
}
}
@@ -54,28 +56,16 @@ impl<'db> UnionBuilder<'db> {
}
}
Type::Never => {}
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
self = self
.add(Type::BooleanLiteral(false))
.add(Type::BooleanLiteral(true));
}
_ => {
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) {
@@ -93,9 +83,14 @@ impl<'db> UnionBuilder<'db> {
return self;
}
}
if ty.is_boolean_literal() {
self.bool_literals_present.increment();
}
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 +105,7 @@ impl<'db> UnionBuilder<'db> {
current_index += 1;
retain
});
self.elements.push(to_add);
self.elements.push(ty);
}
}
}
@@ -119,14 +114,56 @@ impl<'db> UnionBuilder<'db> {
}
pub(crate) fn build(self) -> Type<'db> {
match self.elements.len() {
let UnionBuilder {
mut elements,
db,
bool_literals_present,
} = self;
match elements.len() {
0 => Type::Never,
1 => self.elements[0],
_ => Type::Union(UnionType::new(self.db, self.elements.into_boxed_slice())),
1 => elements[0],
_ => {
if bool_literals_present.is_two() {
let mut element_iter = elements.iter();
if let Some(first_pos) = element_iter.position(Type::is_boolean_literal) {
if let Some(second_pos) = element_iter.position(Type::is_boolean_literal) {
let bool_instance = KnownClass::Bool.to_instance(db);
if elements.len() == 2 {
return bool_instance;
}
elements.swap_remove(first_pos + second_pos + 1);
elements[first_pos] = bool_instance;
}
}
}
Type::Union(UnionType::new(db, elements.into_boxed_slice()))
}
}
}
}
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum BoolLiteralsPresent {
Zero,
One,
Two,
}
impl BoolLiteralsPresent {
fn increment(&mut self) {
*self = match self {
BoolLiteralsPresent::Zero => BoolLiteralsPresent::One,
BoolLiteralsPresent::One => BoolLiteralsPresent::Two,
BoolLiteralsPresent::Two => BoolLiteralsPresent::Two,
};
}
const fn is_two(self) -> bool {
matches!(self, BoolLiteralsPresent::Two)
}
}
#[derive(Clone)]
pub(crate) struct IntersectionBuilder<'db> {
// Really this builds a union-of-intersections, because we always keep our set-theoretic types
@@ -154,7 +191,18 @@ impl<'db> IntersectionBuilder<'db> {
}
pub(crate) fn add_positive(mut self, ty: Type<'db>) -> Self {
if let Type::Union(union) = ty {
const BOOL_LITERALS: &[Type] = &[Type::BooleanLiteral(false), Type::BooleanLiteral(true)];
// Treat `bool` as `Literal[True] | Literal[False]`
let union_elements = match ty {
Type::Union(union) => Some(union.elements(self.db)),
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
Some(BOOL_LITERALS)
}
_ => None,
};
if let Some(elements) = union_elements {
// 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
// of those sub-intersections in it. E.g. if `self` is a simple intersection `T1 & T2`
@@ -163,8 +211,7 @@ impl<'db> IntersectionBuilder<'db> {
// (T2 & T4)`. If `self` is already a union-of-intersections `(T1 & T2) | (T3 & T4)`
// and we add `T5 | T6` to it, that flattens all the way out to `(T1 & T2 & T5) | (T1 &
// T2 & T6) | (T3 & T4 & T5) ...` -- you get the idea.
union
.elements(self.db)
elements
.iter()
.map(|elem| self.clone().add_positive(*elem))
.fold(IntersectionBuilder::empty(self.db), |mut builder, sub| {
@@ -183,43 +230,52 @@ 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.
if let Type::Union(union) = ty {
for elem in union.elements(self.db) {
self = self.add_negative(*elem);
match ty {
Type::Union(union) => {
for elem in union.elements(self.db) {
self = self.add_negative(*elem);
}
self
}
self
} else if let Type::Intersection(intersection) = ty {
// (A | B) & ~(C & ~D)
// -> (A | B) & (~C | D)
// -> ((A | B) & ~C) | ((A | B) & D)
// i.e. if we have an intersection of positive constraints C
// and negative constraints D, then our new intersection
// is (existing & ~C) | (existing & D)
let positive_side = intersection
.positive(self.db)
.iter()
// we negate all the positive constraints while distributing
.map(|elem| self.clone().add_negative(*elem));
let negative_side = intersection
.negative(self.db)
.iter()
// all negative constraints end up becoming positive constraints
.map(|elem| self.clone().add_positive(*elem));
positive_side.chain(negative_side).fold(
IntersectionBuilder::empty(self.db),
|mut builder, sub| {
builder.intersections.extend(sub.intersections);
builder
},
)
} else {
for inner in &mut self.intersections {
inner.add_negative(self.db, ty);
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
self.add_negative(Type::BooleanLiteral(false))
.add_negative(Type::BooleanLiteral(true))
}
Type::Intersection(intersection) => {
// (A | B) & ~(C & ~D)
// -> (A | B) & (~C | D)
// -> ((A | B) & ~C) | ((A | B) & D)
// i.e. if we have an intersection of positive constraints C
// and negative constraints D, then our new intersection
// is (existing & ~C) | (existing & D)
let positive_side = intersection
.positive(self.db)
.iter()
// we negate all the positive constraints while distributing
.map(|elem| self.clone().add_negative(*elem));
let negative_side = intersection
.negative(self.db)
.iter()
// all negative constraints end up becoming positive constraints
.map(|elem| self.clone().add_positive(*elem));
positive_side.chain(negative_side).fold(
IntersectionBuilder::empty(self.db),
|mut builder, sub| {
builder.intersections.extend(sub.intersections);
builder
},
)
}
_ => {
for inner in &mut self.intersections {
inner.add_negative(self.db, ty);
}
self
}
self
}
}
@@ -246,7 +302,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 +349,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 +396,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 +419,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, ""));

View File

@@ -328,8 +328,9 @@ fn union<'db>(db: &'db TestDb, tys: impl IntoIterator<Item = Type<'db>>) -> 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!(