mirror of
https://github.com/astral-sh/ruff.git
synced 2025-10-05 16:10:36 +00:00
[ty] Introduce TypeRelation::Redundancy
(#20602)
## Summary The union `T | U` can be validly simplified to `U` iff: 1. `T` is a subtype of `U` OR 2. `T` is equivalent to `U` OR 3. `U` is a union and contains a type that is equivalent to `T` OR 4. `T` is an intersection and contains a type that is equivalent to `U` (In practice, the only situation in which 2, 3 or 4 would be true when (1) was not true would be if `T` or `U` is a dynamic type.) Currently we achieve these simplifications in the union builder by doing something along the lines of `t.is_subtype_of(db, u) || t.is_equivalent_to_(db, u) || t.into_intersection().is_some_and(|intersection| intersection.positive(db).contains(&u)) || u.into_union().is_some_and(|union| union.elements(db).contains(&t))`. But this is both slow and misses some cases (it doesn't simplify the union `Any | (Unknown & ~None)` to `Any`, for example). We can improve the consistency and performance of our union simplifications by adding a third type relation that sits in between `TypeRelation::Subtyping` and `TypeRelation::Assignability`: `TypeRelation::UnionSimplification`. This change leads to simpler, more user-friendly types due to the more consistent simplification. It also lead to a pretty huge performance improvement! ## Test Plan Existing tests, plus some new ones.
This commit is contained in:
parent
673167a565
commit
c91b457044
9 changed files with 281 additions and 92 deletions
|
@ -138,6 +138,11 @@ static_assert(is_equivalent_to(Any, Any | Intersection[Any, str]))
|
|||
static_assert(is_equivalent_to(Any, Intersection[str, Any] | Any))
|
||||
static_assert(is_equivalent_to(Any, Any | Intersection[Any, Not[None]]))
|
||||
static_assert(is_equivalent_to(Any, Intersection[Not[None], Any] | Any))
|
||||
|
||||
static_assert(is_equivalent_to(Any, Unknown | Intersection[Unknown, str]))
|
||||
static_assert(is_equivalent_to(Any, Intersection[str, Unknown] | Unknown))
|
||||
static_assert(is_equivalent_to(Any, Unknown | Intersection[Unknown, Not[None]]))
|
||||
static_assert(is_equivalent_to(Any, Intersection[Not[None], Unknown] | Unknown))
|
||||
```
|
||||
|
||||
## Tuples
|
||||
|
|
|
@ -306,3 +306,74 @@ def _(c: BC, d: BD):
|
|||
reveal_type(c) # revealed: Literal[b""]
|
||||
reveal_type(d) # revealed: Literal[b""]
|
||||
```
|
||||
|
||||
## Unions of tuples
|
||||
|
||||
A union of a fixed-length tuple and a variable-length tuple must be collapsed to the variable-length
|
||||
element, never to the fixed-length element (`tuple[()] | tuple[Any, ...]` -> `tuple[Any, ...]`, not
|
||||
`tuple[()]`).
|
||||
|
||||
```py
|
||||
from typing import Any
|
||||
|
||||
def f(
|
||||
a: tuple[()] | tuple[int, ...],
|
||||
b: tuple[int, ...] | tuple[()],
|
||||
c: tuple[int] | tuple[str, ...],
|
||||
d: tuple[str, ...] | tuple[int],
|
||||
e: tuple[()] | tuple[Any, ...],
|
||||
f: tuple[Any, ...] | tuple[()],
|
||||
g: tuple[Any, ...] | tuple[Any | str, ...],
|
||||
h: tuple[Any | str, ...] | tuple[Any, ...],
|
||||
):
|
||||
reveal_type(a) # revealed: tuple[int, ...]
|
||||
reveal_type(b) # revealed: tuple[int, ...]
|
||||
reveal_type(c) # revealed: tuple[int] | tuple[str, ...]
|
||||
reveal_type(d) # revealed: tuple[str, ...] | tuple[int]
|
||||
reveal_type(e) # revealed: tuple[Any, ...]
|
||||
reveal_type(f) # revealed: tuple[Any, ...]
|
||||
reveal_type(g) # revealed: tuple[Any | str, ...]
|
||||
reveal_type(h) # revealed: tuple[Any | str, ...]
|
||||
```
|
||||
|
||||
## Unions of other generic containers
|
||||
|
||||
```toml
|
||||
[environment]
|
||||
python-version = "3.12"
|
||||
```
|
||||
|
||||
```py
|
||||
from typing import Any
|
||||
|
||||
class Bivariant[T]: ...
|
||||
|
||||
class Covariant[T]:
|
||||
def get(self) -> T:
|
||||
raise NotImplementedError
|
||||
|
||||
class Contravariant[T]:
|
||||
def receive(self, input: T) -> None: ...
|
||||
|
||||
class Invariant[T]:
|
||||
mutable_attribute: T
|
||||
|
||||
def _(
|
||||
a: Bivariant[Any] | Bivariant[Any | str],
|
||||
b: Bivariant[Any | str] | Bivariant[Any],
|
||||
c: Covariant[Any] | Covariant[Any | str],
|
||||
d: Covariant[Any | str] | Covariant[Any],
|
||||
e: Contravariant[Any | str] | Contravariant[Any],
|
||||
f: Contravariant[Any] | Contravariant[Any | str],
|
||||
g: Invariant[Any] | Invariant[Any | str],
|
||||
h: Invariant[Any | str] | Invariant[Any],
|
||||
):
|
||||
reveal_type(a) # revealed: Bivariant[Any]
|
||||
reveal_type(b) # revealed: Bivariant[Any | str]
|
||||
reveal_type(c) # revealed: Covariant[Any | str]
|
||||
reveal_type(d) # revealed: Covariant[Any | str]
|
||||
reveal_type(e) # revealed: Contravariant[Any]
|
||||
reveal_type(f) # revealed: Contravariant[Any]
|
||||
reveal_type(g) # revealed: Invariant[Any] | Invariant[Any | str]
|
||||
reveal_type(h) # revealed: Invariant[Any | str] | Invariant[Any]
|
||||
```
|
||||
|
|
|
@ -1050,13 +1050,6 @@ impl<'db> Type<'db> {
|
|||
}
|
||||
}
|
||||
|
||||
pub(crate) const fn into_intersection(self) -> Option<IntersectionType<'db>> {
|
||||
match self {
|
||||
Type::Intersection(intersection_type) => Some(intersection_type),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
#[track_caller]
|
||||
pub(crate) fn expect_union(self) -> UnionType<'db> {
|
||||
|
@ -1420,43 +1413,9 @@ impl<'db> Type<'db> {
|
|||
}
|
||||
}
|
||||
|
||||
/// Return true if this type is a [subtype of] type `target`.
|
||||
/// Return true if this type is a subtype of type `target`.
|
||||
///
|
||||
/// For fully static types, this means that the set of objects represented by `self` is a
|
||||
/// subset of the objects represented by `target`.
|
||||
///
|
||||
/// For gradual types, it means that the union of all possible sets of values represented by
|
||||
/// `self` (the "top materialization" of `self`) is a subtype of the intersection of all
|
||||
/// possible sets of values represented by `target` (the "bottom materialization" of
|
||||
/// `target`). In other words, for all possible pairs of materializations `self'` and
|
||||
/// `target'`, `self'` is always a subtype of `target'`.
|
||||
///
|
||||
/// Note that this latter expansion of the subtyping relation to non-fully-static types is not
|
||||
/// described in the typing spec, but the primary use of the subtyping relation is for
|
||||
/// simplifying unions and intersections, and this expansion to gradual types is sound and
|
||||
/// allows us to better simplify many unions and intersections. This definition does mean the
|
||||
/// subtyping relation is not reflexive for non-fully-static types (e.g. `Any` is not a subtype
|
||||
/// of `Any`).
|
||||
///
|
||||
/// [subtype of]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
|
||||
///
|
||||
/// There would be an even more general definition of subtyping for gradual types, allowing a
|
||||
/// type `S` to be a subtype of a type `T` if the top materialization of `S` (`S+`) is a
|
||||
/// subtype of `T+`, and the bottom materialization of `S` (`S-`) is a subtype of `T-`. This
|
||||
/// definition is attractive in that it would restore reflexivity of subtyping for all types,
|
||||
/// and would mean that gradual equivalence of `S` and `T` could be defined simply as `S <: T
|
||||
/// && T <: S`. It would also be sound, in that simplifying unions or intersections according
|
||||
/// to this definition of subtyping would still result in an equivalent type.
|
||||
///
|
||||
/// Unfortunately using this definition would break transitivity of subtyping when both nominal
|
||||
/// and structural types are involved, because Liskov enforcement for nominal types is based on
|
||||
/// assignability, so we can have class `A` with method `def meth(self) -> Any` and a subclass
|
||||
/// `B(A)` with method `def meth(self) -> int`. In this case, `A` would be a subtype of a
|
||||
/// protocol `P` with method `def meth(self) -> Any`, but `B` would not be a subtype of `P`,
|
||||
/// and yet `B` is (by nominal subtyping) a subtype of `A`, so we would have `B <: A` and `A <:
|
||||
/// P`, but not `B <: P`. Losing transitivity of subtyping is not tenable (it makes union and
|
||||
/// intersection simplification dependent on the order in which elements are added), so we do
|
||||
/// not use this more general definition of subtyping.
|
||||
/// See [`TypeRelation::Subtyping`] for more details.
|
||||
pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool {
|
||||
self.when_subtype_of(db, target).is_always_satisfied()
|
||||
}
|
||||
|
@ -1465,9 +1424,9 @@ impl<'db> Type<'db> {
|
|||
self.has_relation_to(db, target, TypeRelation::Subtyping)
|
||||
}
|
||||
|
||||
/// Return true if this type is [assignable to] type `target`.
|
||||
/// Return true if this type is assignable to type `target`.
|
||||
///
|
||||
/// [assignable to]: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation
|
||||
/// See [`TypeRelation::Assignability`] for more details.
|
||||
pub(crate) fn is_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool {
|
||||
self.when_assignable_to(db, target).is_always_satisfied()
|
||||
}
|
||||
|
@ -1476,6 +1435,14 @@ impl<'db> Type<'db> {
|
|||
self.has_relation_to(db, target, TypeRelation::Assignability)
|
||||
}
|
||||
|
||||
/// Return `true` if it would be redundant to add `self` to a union that already contains `other`.
|
||||
///
|
||||
/// See [`TypeRelation::Redundancy`] for more details.
|
||||
pub(crate) fn is_redundant_with(self, db: &'db dyn Db, other: Type<'db>) -> bool {
|
||||
self.has_relation_to(db, other, TypeRelation::Redundancy)
|
||||
.is_always_satisfied()
|
||||
}
|
||||
|
||||
fn has_relation_to(
|
||||
self,
|
||||
db: &'db dyn Db,
|
||||
|
@ -1497,7 +1464,7 @@ impl<'db> Type<'db> {
|
|||
//
|
||||
// Note that we could do a full equivalence check here, but that would be both expensive
|
||||
// and unnecessary. This early return is only an optimisation.
|
||||
if (relation.is_assignability() || self.subtyping_is_always_reflexive()) && self == target {
|
||||
if (!relation.is_subtyping() || self.subtyping_is_always_reflexive()) && self == target {
|
||||
return ConstraintSet::from(true);
|
||||
}
|
||||
|
||||
|
@ -1514,9 +1481,11 @@ impl<'db> Type<'db> {
|
|||
// It is a subtype of all other types.
|
||||
(Type::Never, _) => ConstraintSet::from(true),
|
||||
|
||||
// Dynamic is only a subtype of `object` and only a supertype of `Never`; both were
|
||||
// handled above. It's always assignable, though.
|
||||
(Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => {
|
||||
// In some specific situations, `Any`/`Unknown`/`@Todo` can be simplified out of unions and intersections,
|
||||
// but this is not true for divergent types (and moving this case any lower down appears to cause
|
||||
// "too many cycle iterations" panics).
|
||||
(Type::Dynamic(DynamicType::Divergent(_)), _)
|
||||
| (_, Type::Dynamic(DynamicType::Divergent(_))) => {
|
||||
ConstraintSet::from(relation.is_assignability())
|
||||
}
|
||||
|
||||
|
@ -1541,10 +1510,33 @@ impl<'db> Type<'db> {
|
|||
.has_relation_to_impl(db, right, relation, visitor)
|
||||
}
|
||||
|
||||
(Type::TypedDict(_), _) | (_, Type::TypedDict(_)) => {
|
||||
// TODO: Implement assignability and subtyping for TypedDict
|
||||
ConstraintSet::from(relation.is_assignability())
|
||||
}
|
||||
// Dynamic is only a subtype of `object` and only a supertype of `Never`; both were
|
||||
// handled above. It's always assignable, though.
|
||||
//
|
||||
// Union simplification sits in between subtyping and assignability. `Any <: T` only
|
||||
// holds true if `T` is also a dynamic type or a union that contains a dynamic type.
|
||||
// Similarly, `T <: Any` only holds true if `T` is a dynamic type or an intersection
|
||||
// that contains a dynamic type.
|
||||
(Type::Dynamic(_), _) => ConstraintSet::from(match relation {
|
||||
TypeRelation::Subtyping => false,
|
||||
TypeRelation::Assignability => true,
|
||||
TypeRelation::Redundancy => match target {
|
||||
Type::Dynamic(_) => true,
|
||||
Type::Union(union) => union.elements(db).iter().any(Type::is_dynamic),
|
||||
_ => false,
|
||||
},
|
||||
}),
|
||||
(_, Type::Dynamic(_)) => ConstraintSet::from(match relation {
|
||||
TypeRelation::Subtyping => false,
|
||||
TypeRelation::Assignability => true,
|
||||
TypeRelation::Redundancy => match self {
|
||||
Type::Dynamic(_) => true,
|
||||
Type::Intersection(intersection) => {
|
||||
intersection.positive(db).iter().any(Type::is_dynamic)
|
||||
}
|
||||
_ => false,
|
||||
},
|
||||
}),
|
||||
|
||||
// In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied:
|
||||
// 1. `T` is a bound TypeVar and `T`'s upper bound is a subtype of `S`.
|
||||
|
@ -1692,6 +1684,11 @@ impl<'db> Type<'db> {
|
|||
// TODO: Infer specializations here
|
||||
(Type::TypeVar(_), _) | (_, Type::TypeVar(_)) => ConstraintSet::from(false),
|
||||
|
||||
(Type::TypedDict(_), _) | (_, Type::TypedDict(_)) => {
|
||||
// TODO: Implement assignability and subtyping for TypedDict
|
||||
ConstraintSet::from(relation.is_assignability())
|
||||
}
|
||||
|
||||
// Note that the definition of `Type::AlwaysFalsy` depends on the return value of `__bool__`.
|
||||
// If `__bool__` always returns True or False, it can be treated as a subtype of `AlwaysTruthy` or `AlwaysFalsy`, respectively.
|
||||
(left, Type::AlwaysFalsy) => ConstraintSet::from(left.bool(db).is_always_false()),
|
||||
|
@ -8993,16 +8990,138 @@ impl<'db> ConstructorCallError<'db> {
|
|||
}
|
||||
}
|
||||
|
||||
/// A non-exhaustive enumeration of relations that can exist between types.
|
||||
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
|
||||
pub(crate) enum TypeRelation {
|
||||
/// The "subtyping" relation.
|
||||
///
|
||||
/// A [fully static] type `B` is a subtype of a fully static type `A` if and only if
|
||||
/// the set of possible runtime values represented by `B` is a subset of the set
|
||||
/// of possible runtime values represented by `A`.
|
||||
///
|
||||
/// For a pair of types `C` and `D` that may or may not be fully static,
|
||||
/// `D` can be said to be a subtype of `C` if every possible fully static
|
||||
/// [materialization] of `D` is a subtype of every possible fully static
|
||||
/// materialization of `C`. Another way of saying this is that `D` will be a
|
||||
/// subtype of `C` if and only if the union of all possible sets of values
|
||||
/// represented by `D` (the "top materialization" of `D`) is a subtype of the
|
||||
/// intersection of all possible sets of values represented by `C` (the "bottom
|
||||
/// materialization" of `C`). More concisely: `D <: C` iff `Top[D] <: Bottom[C]`.
|
||||
///
|
||||
/// For example, `list[Any]` can be said to be a subtype of `Sequence[object]`,
|
||||
/// because every possible fully static materialization of `list[Any]` (`list[int]`,
|
||||
/// `list[str]`, `list[bytes | bool]`, `list[SupportsIndex]`, etc.) would be
|
||||
/// considered a subtype of `Sequence[object]`.
|
||||
///
|
||||
/// Note that this latter expansion of the subtyping relation to non-fully-static
|
||||
/// types is not described in the typing spec, but this expansion to gradual types is
|
||||
/// sound and consistent with the principles laid out in the spec. This definition
|
||||
/// does mean the subtyping relation is not reflexive for non-fully-static types
|
||||
/// (e.g. `Any` is not a subtype of `Any`).
|
||||
///
|
||||
/// [fully static]: https://typing.python.org/en/latest/spec/glossary.html#term-fully-static-type
|
||||
/// [materialization]: https://typing.python.org/en/latest/spec/glossary.html#term-materialize
|
||||
Subtyping,
|
||||
|
||||
/// The "assignability" relation.
|
||||
///
|
||||
/// The assignability relation between two types `A` and `B` dictates whether a
|
||||
/// type checker should emit an error when a value of type `B` is assigned to a
|
||||
/// variable declared as having type `A`.
|
||||
///
|
||||
/// For a pair of [fully static] types `A` and `B`, the assignability relation
|
||||
/// between `A` and `B` is the same as the subtyping relation.
|
||||
///
|
||||
/// Between a pair of `C` and `D` where either `C` or `D` is not fully static, the
|
||||
/// assignability relation may be more permissive than the subtyping relation. `D`
|
||||
/// can be said to be assignable to `C` if *some* possible fully static [materialization]
|
||||
/// of `D` is a subtype of *some* possible fully static materialization of `C`.
|
||||
/// Another way of saying this is that `D` will be assignable to `C` if and only if the
|
||||
/// intersection of all possible sets of values represented by `D` (the "bottom
|
||||
/// materialization" of `D`) is a subtype of the union of all possible sets of values
|
||||
/// represented by `C` (the "top materialization" of `C`).
|
||||
/// More concisely: `D <: C` iff `Bottom[D] <: Top[C]`.
|
||||
///
|
||||
/// For example, `Any` is not a subtype of `int`, because there are possible
|
||||
/// materializations of `Any` (e.g., `str`) that are not subtypes of `int`.
|
||||
/// `Any` is *assignable* to `int`, however, as there are *some* possible materializations
|
||||
/// of `Any` (such as `int` itself!) that *are* subtypes of `int`. `Any` cannot even
|
||||
/// be considered a subtype of itself, as two separate uses of `Any` in the same scope
|
||||
/// might materialize to different types between which there would exist no subtyping
|
||||
/// relation; nor is `Any` a subtype of `int | Any`, for the same reason. Nonetheless,
|
||||
/// `Any` is assignable to both `Any` and `int | Any`.
|
||||
///
|
||||
/// While `Any` can materialize to anything, the presence of `Any` in a type does not
|
||||
/// necessarily make it assignable to everything. For example, `list[Any]` is not
|
||||
/// assignable to `int`, because there are no possible fully static types we could
|
||||
/// substitute for `Any` in this type that would make it a subtype of `int`. For the
|
||||
/// same reason, a union such as `str | Any` is not assignable to `int`.
|
||||
///
|
||||
/// [fully static]: https://typing.python.org/en/latest/spec/glossary.html#term-fully-static-type
|
||||
/// [materialization]: https://typing.python.org/en/latest/spec/glossary.html#term-materialize
|
||||
Assignability,
|
||||
|
||||
/// The "redundancy" relation.
|
||||
///
|
||||
/// The redundancy relation dictates whether the union `A | B` can be safely simplified
|
||||
/// to the type `A` without downstream consequences on ty's inference of types elsewhere.
|
||||
///
|
||||
/// For a pair of [fully static] types `A` and `B`, the redundancy relation between `A`
|
||||
/// and `B` is the same as the subtyping relation.
|
||||
///
|
||||
/// Between a pair of `C` and `D` where either `C` or `D` is not fully static, the
|
||||
/// redundancy relation sits in between the subtyping relation and the assignability relation.
|
||||
/// `D` can be said to be redundant in a union with `C` if the top materialization of the type
|
||||
/// `C | D` is equivalent to the top materialization of `C`, *and* the bottom materialization
|
||||
/// of `C | D` is equivalent to the bottom materialization of `C`.
|
||||
/// More concisely: `D <: C` iff `Top[C | D] == Top[C]` AND `Bottom[C | D] == Bottom[C]`.
|
||||
///
|
||||
/// Practically speaking, in most respects the redundancy relation is the same as the subtyping
|
||||
/// relation. It is redundant to add `bool` to a union that includes `int`, because `bool` is a
|
||||
/// subtype of `int`, so inference of attribute access or binary expressions on the union
|
||||
/// `int | bool` would always produce a type that represents the same set of possible sets of
|
||||
/// runtime values as if ty had inferred the attribute access or binary expression on `int`
|
||||
/// alone.
|
||||
///
|
||||
/// Where the redundancy relation differs from the subtyping relation is that there are a
|
||||
/// number of simplifications that can be made when simplifying unions that are not
|
||||
/// strictly permitted by the subtyping relation. For example, it is safe to avoid adding
|
||||
/// `Any` to a union that already includes `Any`, because `Any` already represents an
|
||||
/// unknown set of possible sets of runtime values that can materialize to any type in a
|
||||
/// gradual, permissive way. Inferring attribute access or binary expressions over
|
||||
/// `Any | Any` could never conceivably yield a type that represents a different set of
|
||||
/// possible sets of runtime values to inferring the same expression over `Any` alone;
|
||||
/// although `Any` is not a subtype of `Any`, top materialization of both `Any` and
|
||||
/// `Any | Any` is `object`, and the bottom materialization of both types is `Never`.
|
||||
///
|
||||
/// The same principle also applies to intersections that include `Any` being added to
|
||||
/// unions that include `Any`: for any type `A`, although naively distributing
|
||||
/// type-inference operations over `(Any & A) | Any` could produce types that have
|
||||
/// different displays to `Any`, `(Any & A) | Any` nonetheless has the same top
|
||||
/// materialization as `Any` and the same bottom materialization as `Any`, and thus it is
|
||||
/// redundant to add `Any & A` to a union that already includes `Any`.
|
||||
///
|
||||
/// Union simplification cannot use the assignability relation, meanwhile, as it is
|
||||
/// trivial to produce examples of cases where adding a type `B` to a union that includes
|
||||
/// `A` would impact downstream type inference, even where `B` is assignable to `A`. For
|
||||
/// example, `int` is assignable to `Any`, but attribute access over the union `int | Any`
|
||||
/// will yield very different results to attribute access over `Any` alone. The top
|
||||
/// materialization of `Any` and `int | Any` may be the same type (`object`), but the
|
||||
/// two differ in their bottom materializations (`Never` and `int`, respectively).
|
||||
///
|
||||
/// [fully static]: https://typing.python.org/en/latest/spec/glossary.html#term-fully-static-type
|
||||
/// [materializations]: https://typing.python.org/en/latest/spec/glossary.html#term-materialize
|
||||
Redundancy,
|
||||
}
|
||||
|
||||
impl TypeRelation {
|
||||
pub(crate) const fn is_assignability(self) -> bool {
|
||||
matches!(self, TypeRelation::Assignability)
|
||||
}
|
||||
|
||||
pub(crate) const fn is_subtyping(self) -> bool {
|
||||
matches!(self, TypeRelation::Subtyping)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Copy, Clone, PartialEq, Eq, get_size2::GetSize)]
|
||||
|
|
|
@ -502,18 +502,9 @@ impl<'db> UnionBuilder<'db> {
|
|||
}
|
||||
|
||||
if should_simplify_full && !matches!(element_type, Type::TypeAlias(_)) {
|
||||
if ty.is_equivalent_to(self.db, element_type)
|
||||
|| ty.is_subtype_of(self.db, element_type)
|
||||
|| ty.into_intersection().is_some_and(|intersection| {
|
||||
intersection.positive(self.db).contains(&element_type)
|
||||
})
|
||||
{
|
||||
if ty.is_redundant_with(self.db, element_type) {
|
||||
return;
|
||||
} else if element_type.is_subtype_of(self.db, ty)
|
||||
|| element_type
|
||||
.into_intersection()
|
||||
.is_some_and(|intersection| intersection.positive(self.db).contains(&ty))
|
||||
{
|
||||
} else if element_type.is_redundant_with(self.db, ty) {
|
||||
to_remove.push(index);
|
||||
} else if ty_negated.is_subtype_of(self.db, element_type) {
|
||||
// We add `ty` to the union. We just checked that `~ty` is a subtype of an
|
||||
|
@ -930,13 +921,11 @@ impl<'db> InnerIntersectionBuilder<'db> {
|
|||
let mut to_remove = SmallVec::<[usize; 1]>::new();
|
||||
for (index, existing_positive) in self.positive.iter().enumerate() {
|
||||
// S & T = S if S <: T
|
||||
if existing_positive.is_subtype_of(db, new_positive)
|
||||
|| existing_positive.is_equivalent_to(db, new_positive)
|
||||
{
|
||||
if existing_positive.is_redundant_with(db, new_positive) {
|
||||
return;
|
||||
}
|
||||
// same rule, reverse order
|
||||
if new_positive.is_subtype_of(db, *existing_positive) {
|
||||
if new_positive.is_redundant_with(db, *existing_positive) {
|
||||
to_remove.push(index);
|
||||
}
|
||||
// A & B = Never if A and B are disjoint
|
||||
|
@ -1027,9 +1016,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
|
|||
let mut to_remove = SmallVec::<[usize; 1]>::new();
|
||||
for (index, existing_negative) in self.negative.iter().enumerate() {
|
||||
// ~S & ~T = ~T if S <: T
|
||||
if existing_negative.is_subtype_of(db, new_negative)
|
||||
|| existing_negative.is_equivalent_to(db, new_negative)
|
||||
{
|
||||
if existing_negative.is_redundant_with(db, new_negative) {
|
||||
to_remove.push(index);
|
||||
}
|
||||
// same rule, reverse order
|
||||
|
|
|
@ -551,7 +551,9 @@ impl<'db> ClassType<'db> {
|
|||
self.iter_mro(db).when_any(db, |base| {
|
||||
match base {
|
||||
ClassBase::Dynamic(_) => match relation {
|
||||
TypeRelation::Subtyping => ConstraintSet::from(other.is_object(db)),
|
||||
TypeRelation::Subtyping | TypeRelation::Redundancy => {
|
||||
ConstraintSet::from(other.is_object(db))
|
||||
}
|
||||
TypeRelation::Assignability => ConstraintSet::from(!other.is_final(db)),
|
||||
},
|
||||
|
||||
|
|
|
@ -969,7 +969,9 @@ impl<'db> FunctionType<'db> {
|
|||
_visitor: &HasRelationToVisitor<'db>,
|
||||
) -> ConstraintSet<'db> {
|
||||
match relation {
|
||||
TypeRelation::Subtyping => ConstraintSet::from(self.is_subtype_of(db, other)),
|
||||
TypeRelation::Subtyping | TypeRelation::Redundancy => {
|
||||
ConstraintSet::from(self.is_subtype_of(db, other))
|
||||
}
|
||||
TypeRelation::Assignability => ConstraintSet::from(self.is_assignable_to(db, other)),
|
||||
}
|
||||
}
|
||||
|
|
|
@ -620,22 +620,26 @@ fn has_relation_in_invariant_position<'db>(
|
|||
base_type.has_relation_to_impl(db, *derived_type, relation, visitor)
|
||||
}),
|
||||
// For gradual types, A <: B (subtyping) is defined as Top[A] <: Bottom[B]
|
||||
(None, Some(base_mat), TypeRelation::Subtyping) => is_subtype_in_invariant_position(
|
||||
db,
|
||||
derived_type,
|
||||
MaterializationKind::Top,
|
||||
base_type,
|
||||
base_mat,
|
||||
visitor,
|
||||
),
|
||||
(Some(derived_mat), None, TypeRelation::Subtyping) => is_subtype_in_invariant_position(
|
||||
db,
|
||||
derived_type,
|
||||
derived_mat,
|
||||
base_type,
|
||||
MaterializationKind::Bottom,
|
||||
visitor,
|
||||
),
|
||||
(None, Some(base_mat), TypeRelation::Subtyping | TypeRelation::Redundancy) => {
|
||||
is_subtype_in_invariant_position(
|
||||
db,
|
||||
derived_type,
|
||||
MaterializationKind::Top,
|
||||
base_type,
|
||||
base_mat,
|
||||
visitor,
|
||||
)
|
||||
}
|
||||
(Some(derived_mat), None, TypeRelation::Subtyping | TypeRelation::Redundancy) => {
|
||||
is_subtype_in_invariant_position(
|
||||
db,
|
||||
derived_type,
|
||||
derived_mat,
|
||||
base_type,
|
||||
MaterializationKind::Bottom,
|
||||
visitor,
|
||||
)
|
||||
}
|
||||
// And A <~ B (assignability) is Bottom[A] <: Top[B]
|
||||
(None, Some(base_mat), TypeRelation::Assignability) => is_subtype_in_invariant_position(
|
||||
db,
|
||||
|
|
|
@ -138,7 +138,7 @@ impl<'db> SubclassOfType<'db> {
|
|||
) -> ConstraintSet<'db> {
|
||||
match (self.subclass_of, other.subclass_of) {
|
||||
(SubclassOfInner::Dynamic(_), SubclassOfInner::Dynamic(_)) => {
|
||||
ConstraintSet::from(relation.is_assignability())
|
||||
ConstraintSet::from(!relation.is_subtyping())
|
||||
}
|
||||
(SubclassOfInner::Dynamic(_), SubclassOfInner::Class(other_class)) => {
|
||||
ConstraintSet::from(other_class.is_object(db) || relation.is_assignability())
|
||||
|
|
|
@ -757,8 +757,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
|
|||
// (or any other dynamic type), then the `...` is the _gradual choice_ of all
|
||||
// possible lengths. This means that `tuple[Any, ...]` can match any tuple of any
|
||||
// length.
|
||||
if relation == TypeRelation::Subtyping || !matches!(self.variable, Type::Dynamic(_))
|
||||
{
|
||||
if !relation.is_assignability() || !self.variable.is_dynamic() {
|
||||
return ConstraintSet::from(false);
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue