From 1f46c189214fb0ea79e9fe707fa67ad09a511f68 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Tue, 16 Sep 2025 10:05:01 -0400 Subject: [PATCH] [ty] More constraint set simplifications via simpler constraint representation (#20423) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Previously, we used a very fine-grained representation for individual constraints: each constraint was _either_ a range constraint, a not-equivalent constraint, or an incomparable constraint. These three pieces are enough to represent all of the "real" constraints we need to create — range constraints and their negation. However, it meant that we weren't picking up as many chances to simplify constraint sets as we could. Our simplification logic depends on being able to look at _pairs_ of constraints or clauses to see if they simplify relative to each other. With our fine-grained representation, we could easily encounter situations that we should have been able to simplify, but that would require looking at three or more individual constraints. For instance, negating a range constraint would produce: ``` ¬(Base ≤ T ≤ Super) = ((T ≤ Base) ∧ (T ≠ Base)) ∨ (T ≁ Base) ∨ ((Super ≤ T) ∧ (T ≠ Super)) ∨ (T ≁ Super) ``` That is, `T` must be (strictly) less than `Base`, (strictly) greater than `Super`, or incomparable to either. If we tried to union those back together, we should get `always`, since `x ∨ ¬x` should always be true, no matter what `x` is. But instead we would get: ``` (Base ≤ T ≤ Super) ∨ ((T ≤ Base) ∧ (T ≠ Base)) ∨ (T ≁ Base) ∨ ((Super ≤ T) ∧ (T ≠ Super)) ∨ (T ≁ Super) ``` Nothing would simplify relative to each other, because we'd have to look at all five union elements to see that together they do in fact combine to `always`. The fine-grained representation was nice, because it made it easier to [work out the math](https://dcreager.net/theory/constraints/) for intersections and unions of each kind of constraint. But being able to simplify is more important, since the example above comes up immediately in #20093 when trying to handle constrained typevars. The fix in this PR is to go back to a more coarse-grained representation, where each individual constraint consists of a positive range (which might be `always` / `Never ≤ T ≤ object`), and zero or more negative ranges. The intuition is to think of a constraint as a region of the type space (representable as a range) with zero or more "holes" removed from it. With this representation, negating a range constraint produces: ``` ¬(Base ≤ T ≤ Super) = (always ∧ ¬(Base ≤ T ≤ Super)) ``` (That looks trivial, because it is! We just move the positive range to the negative side.) The math is not that much harder than before, because there are only three combinations to consider (each for intersection and union) — though the fact that there can be multiple holes in a constraint does require some nested loops. But the mdtest suite gives me confidence that this is not introducing any new issues, and it definitely removes a troublesome TODO. (As an aside, this change also means that we are back to having each clause contain no more than one individual constraint for any typevar. This turned out to be important, because part of our simplification logic was also depending on that!) --------- Co-authored-by: Carl Meyer --- .../mdtest/type_properties/constraints.md | 629 ++++------- crates/ty_python_semantic/src/types.rs | 70 +- .../src/types/constraints.rs | 977 +++++++++--------- .../ty_python_semantic/src/types/function.rs | 70 +- .../ty_extensions/ty_extensions.pyi | 5 +- 5 files changed, 752 insertions(+), 999 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md index f00f199cb1..3239c9c2f1 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md @@ -91,7 +91,7 @@ that specific type. ```py def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)] + # revealed: ty_extensions.ConstraintSet[(T@_ = Base)] reveal_type(range_constraint(Base, T, Base)) ``` @@ -111,88 +111,89 @@ def _[T]() -> None: reveal_type(range_constraint(Sequence[Any], T, Sequence[Base])) ``` -### Not equivalent +### Negated range -A _not-equivalent_ constraint requires the typevar to specialize to anything _other_ than a -particular type (the "hole"). +A _negated range_ constraint is the opposite of a range constraint: it requires the typevar to _not_ +be within a particular lower and upper bound. The typevar can only specialize to a type that is a +strict subtype of the lower bound, a strict supertype of the upper bound, or incomparable to either. ```py -from typing import Any, Never, Sequence -from ty_extensions import not_equivalent_constraint +from typing import Any, final, Never, Sequence +from ty_extensions import negated_range_constraint -class Base: ... +class Super: ... +class Base(Super): ... +class Sub(Base): ... +@final +class Unrelated: ... + +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] + reveal_type(negated_range_constraint(Sub, T, Super)) +``` + +Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower +bound. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] + reveal_type(negated_range_constraint(Never, T, Base)) +``` + +Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having +no upper bound. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)] + reveal_type(negated_range_constraint(Base, T, object)) +``` + +And a negated range constraint with _both_ a lower bound of `Never` and an upper bound of `object` +cannot be satisfied at all. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(negated_range_constraint(Never, T, object)) +``` + +If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound) +or incomparable, then the negated range constraint can always be satisfied. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(Super, T, Sub)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(Base, T, Unrelated)) +``` + +The lower and upper bound can be the same type, in which case the typevar can be specialized to any +type other than that specific type. + +```py def _[T]() -> None: # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base)) + reveal_type(negated_range_constraint(Base, T, Base)) ``` -Unlike range constraints, `Never` and `object` are not special when used as the hole of a -not-equivalent constraint — there are many types that are not equivalent to `Never` or `object`. +Constraints can only refer to fully static types, so the lower and upper bounds are transformed into +their bottom and top materializations, respectively. ```py def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Never)] - reveal_type(not_equivalent_constraint(T, Never)) + # revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)] + reveal_type(negated_range_constraint(Base, T, Any)) + # revealed: ty_extensions.ConstraintSet[¬(Sequence[Base] ≤ T@_ ≤ Sequence[object])] + reveal_type(negated_range_constraint(Sequence[Base], T, Sequence[Any])) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ object)] - reveal_type(not_equivalent_constraint(T, object)) -``` - -Constraints can only refer to fully static types. However, not-equivalent constraints are not -created directly; they are only created when negating a range constraint. Since that range -constraint will have fully static lower and upper bounds, the not-equivalent constraints that we -create will already have a fully static hole. Therefore, we raise a diagnostic when calling the -internal `not_equivalent_constraint` constructor with a non-fully-static type. - -```py -def _[T]() -> None: - # error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type" - reveal_type(not_equivalent_constraint(T, Any)) # revealed: ConstraintSet - # error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type" - reveal_type(not_equivalent_constraint(T, Sequence[Any])) # revealed: ConstraintSet -``` - -### Incomparable - -An _incomparable_ constraint requires the typevar to specialize to any type that is neither a -subtype nor a supertype of a particular type (the "pivot"). - -```py -from typing import Any, Never, Sequence -from ty_extensions import incomparable_constraint - -class Base: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base)) -``` - -Every type is comparable with `Never` and with `object`, so an incomparable constraint with either -as a pivot cannot ever be satisfied. - -```py -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(incomparable_constraint(T, Never)) - - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(incomparable_constraint(T, object)) -``` - -Constraints can only refer to fully static types. However, incomparable constraints are not created -directly; they are only created when negating a range constraint. Since that range constraint will -have fully static lower and upper bounds, the incomparable constraints that we create will already -have a fully static hole. Therefore, we raise a diagnostic when calling the internal -`incomparable_constraint` constructor with a non-fully-static type. - -```py -def _[T]() -> None: - # error: [invalid-argument-type] "Incomparable constraint must have a fully static type" - reveal_type(incomparable_constraint(T, Any)) # revealed: ConstraintSet - # error: [invalid-argument-type] "Incomparable constraint must have a fully static type" - reveal_type(incomparable_constraint(T, Sequence[Any])) # revealed: ConstraintSet + # revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] + reveal_type(negated_range_constraint(Any, T, Base)) + # revealed: ty_extensions.ConstraintSet[¬(Sequence[Never] ≤ T@_ ≤ Sequence[Base])] + reveal_type(negated_range_constraint(Sequence[Any], T, Sequence[Base])) ``` ## Intersection @@ -203,7 +204,7 @@ cases, we can simplify the result of an intersection. ### Different typevars ```py -from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint +from ty_extensions import range_constraint, negated_range_constraint class Super: ... class Base(Super): ... @@ -214,20 +215,10 @@ We cannot simplify the intersection of constraints that refer to different typev ```py def _[T, U]() -> None: - # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (U@_ ≁ Base))] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(U, Base)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (U@_ ≠ Base))] - reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(U, Base)) # revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base))] reveal_type(range_constraint(Sub, T, Base) & range_constraint(Sub, U, Base)) -``` - -Intersection is reflexive. - -```py -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base)) + # revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ U@_ ≤ Base))] + reveal_type(negated_range_constraint(Sub, T, Base) & negated_range_constraint(Sub, U, Base)) ``` ### Intersection of two ranges @@ -251,7 +242,7 @@ def _[T]() -> None: reveal_type(range_constraint(SubSub, T, Base) & range_constraint(Sub, T, Super)) # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] reveal_type(range_constraint(SubSub, T, Super) & range_constraint(Sub, T, Base)) - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)] + # revealed: ty_extensions.ConstraintSet[(T@_ = Base)] reveal_type(range_constraint(Sub, T, Base) & range_constraint(Base, T, Super)) # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)] reveal_type(range_constraint(Sub, T, Super) & range_constraint(Sub, T, Super)) @@ -267,180 +258,110 @@ def _[T]() -> None: reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Unrelated, T, object)) ``` -### Intersection of range and not-equivalent +### Intersection of a range and a negated range -If the hole of a not-equivalent constraint is within the lower and upper bounds of a range -constraint, the intersection "removes" the hole from the range. The intersection cannot be -simplified. +The bounds of the range constraint provide a range of types that should be included; the bounds of +the negated range constraint provide a "hole" of types that should not be included. We can think of +the intersection as removing the hole from the range constraint. ```py -from typing import final -from ty_extensions import not_equivalent_constraint, range_constraint +from typing import final, Never +from ty_extensions import range_constraint, negated_range_constraint class Super: ... class Base(Super): ... class Sub(Base): ... +class SubSub(Sub): ... @final class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Super) ∧ (T@_ ≠ Base))] - reveal_type(range_constraint(Sub, T, Super) & not_equivalent_constraint(T, Base)) ``` -If the hole is not within the lower and upper bounds (because it's a subtype of the lower bound, a -supertype of the upper bound, or not comparable with either), then removing the hole doesn't do -anything. +If the negative range completely contains the positive range, then the intersection is empty. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(SubSub, T, Super)) + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(Sub, T, Base)) +``` + +If the negative range is disjoint from the positive range, the negative range doesn't remove +anything; the intersection is the positive range. ```py def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)] - reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)] - reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] - reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] - reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Unrelated)) + reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(Never, T, Unrelated)) + # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub)] + reveal_type(range_constraint(SubSub, T, Sub) & negated_range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)] + reveal_type(range_constraint(Base, T, Super) & negated_range_constraint(SubSub, T, Sub)) ``` -If the lower and upper bounds are the same, it's actually an "equivalent" constraint. If the hole is -also that same type, then the intersection is empty — the not-equivalent constraint removes the only -type that satisfies the range constraint. +Otherwise we clip the negative constraint to the mininum range that overlaps with the positive +range. ```py def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(range_constraint(Base, T, Base) & not_equivalent_constraint(T, Base)) + # revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ T@_ ≤ Base))] + reveal_type(range_constraint(SubSub, T, Base) & negated_range_constraint(Sub, T, Super)) + # revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))] + reveal_type(range_constraint(SubSub, T, Super) & negated_range_constraint(Sub, T, Base)) ``` -### Intersection of range and incomparable +### Intersection of two negated ranges -The intersection of a range constraint and an incomparable constraint cannot be satisfied if the -pivot is a subtype of the lower bound, or a supertype of the upper bound. (If the pivot is a subtype -of the lower bound, then by transitivity, the pivot is also a subtype of everything in the range.) +When one of the bounds is entirely contained within the other, the intersection simplifies to the +smaller constraint. For negated ranges, the smaller constraint is the one with the larger "hole". ```py from typing import final -from ty_extensions import incomparable_constraint, range_constraint +from ty_extensions import negated_range_constraint class Super: ... class Base(Super): ... class Sub(Base): ... +class SubSub(Sub): ... @final class Unrelated: ... def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Base)) - - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[never] - reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Base)) + # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Super)] + reveal_type(negated_range_constraint(SubSub, T, Super) & negated_range_constraint(Sub, T, Base)) + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] + reveal_type(negated_range_constraint(Sub, T, Super) & negated_range_constraint(Sub, T, Super)) ``` -Otherwise, the intersection cannot be simplified. +Otherwise, the union cannot be simplified. ```py -from ty_extensions import is_subtype_of - def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[((Base ≤ T@_ ≤ Super) ∧ (T@_ ≁ Unrelated))] - reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Unrelated)) + # revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ ¬(Base ≤ T@_ ≤ Super))] + reveal_type(negated_range_constraint(Sub, T, Base) & negated_range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Base ≤ T@_ ≤ Super))] + reveal_type(negated_range_constraint(SubSub, T, Sub) & negated_range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Unrelated ≤ T@_))] + reveal_type(negated_range_constraint(SubSub, T, Sub) & negated_range_constraint(Unrelated, T, object)) ``` -### Intersection of two not-equivalents - -Intersection is reflexive, so the intersection of a not-equivalent constraint with itself is itself. +In particular, the following does not simplify, even though it seems like it could simplify to +`¬(SubSub ≤ T@_ ≤ Super)`. The issue is that there are types that are within the bounds of +`SubSub ≤ T@_ ≤ Super`, but which are not comparable to `Base` or `Sub`, and which therefore should +be included in the union. An example would be the type that contains all instances of `Super`, +`Base`, and `SubSub` (but _not_ including instances of `Sub`). (We don't have a way to spell that +type at the moment, but it is a valid type.) That type is not in `SubSub ≤ T ≤ Base`, since it +includes `Super`, which is outside the range. It's also not in `Sub ≤ T ≤ Super`, because it does +not include `Sub`. That means it should be in the union. (Remember that for negated range +constraints, the lower and upper bounds define the "hole" of types that are _not_ allowed.) Since +that type _is_ in `SubSub ≤ T ≤ Super`, it is not correct to simplify the union in this way. ```py -from typing import final -from ty_extensions import not_equivalent_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Super))] - reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Sub))] - reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Unrelated))] - reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Unrelated)) -``` - -### Intersection of not-equivalent and incomparable - -When intersecting a not-equivalent constraint and an incomparable constraint, if the hole and pivot -are comparable, then the incomparable constraint already excludes the hole, so removing the hole -doesn't do anything. - -```py -from typing import final -from ty_extensions import incomparable_constraint, not_equivalent_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(not_equivalent_constraint(T, Super) & incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(not_equivalent_constraint(T, Sub) & incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Unrelated) ∧ (T@_ ≁ Base))] - reveal_type(not_equivalent_constraint(T, Unrelated) & incomparable_constraint(T, Base)) - - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Super)] - reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Sub)] - reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≁ Unrelated))] - reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Unrelated)) -``` - -### Intersection of two incomparables - -We can only simplify the intersection of two incomparable constraints if they have the same pivot. - -```py -from typing import final -from ty_extensions import incomparable_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Super))] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Sub))] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Unrelated))] - reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Unrelated)) + # revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ T@_ ≤ Super))] + reveal_type(negated_range_constraint(SubSub, T, Base) & negated_range_constraint(Sub, T, Super)) ``` ## Union @@ -451,7 +372,7 @@ can simplify the result of an union. ### Different typevars ```py -from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint +from ty_extensions import range_constraint, negated_range_constraint class Super: ... class Base(Super): ... @@ -462,20 +383,10 @@ We cannot simplify the union of constraints that refer to different typevars. ```py def _[T, U]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (U@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(U, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base) ∨ (U@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(U, Base)) # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Sub ≤ U@_ ≤ Base)] reveal_type(range_constraint(Sub, T, Base) | range_constraint(Sub, U, Base)) -``` - -Union is reflexive. - -```py -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base)) + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base) ∨ ¬(Sub ≤ U@_ ≤ Base)] + reveal_type(negated_range_constraint(Sub, T, Base) | negated_range_constraint(Sub, U, Base)) ``` ### Union of two ranges @@ -530,175 +441,100 @@ def _[T]() -> None: reveal_type(range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super)) ``` -### Union of range and not-equivalent +### Union of a range and a negated range -If the hole of a not-equivalent constraint is within the lower and upper bounds of a range -constraint, the range "fills in" the hole. The resulting union can always be satisfied. +The bounds of the range constraint provide a range of types that should be included; the bounds of +the negated range constraint provide a "hole" of types that should not be included. We can think of +the union as filling part of the hole with the types from the range constraint. ```py -from typing import final -from ty_extensions import not_equivalent_constraint, range_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(range_constraint(Sub, T, Super) | not_equivalent_constraint(T, Base)) -``` - -Otherwise the range constraint is subsumed by the not-equivalent constraint. - -```py -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)] - reveal_type(range_constraint(Sub, T, Base) | not_equivalent_constraint(T, Super)) -``` - -### Union of range and incomparable - -When the "pivot" of the incomparable constraint is not comparable with either bound of the range -constraint, the incomparable constraint subsumes the range constraint. - -```py -from typing import final -from ty_extensions import incomparable_constraint, range_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Unrelated)] - reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Unrelated)) -``` - -Otherwise, the union cannot be simplified. - -```py -from ty_extensions import is_subtype_of - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Base)] - reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Sub)] - reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Super)] - reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Super)) -``` - -### Union of two not-equivalents - -Union is reflexive, so the union of a not-equivalent constraint with itself is itself. The union of -two different not-equivalent constraints is always satisfied. - -```py -from typing import final -from ty_extensions import not_equivalent_constraint +from typing import final, Never +from ty_extensions import range_constraint, negated_range_constraint class Super: ... class Base(Super): ... class Sub(Base): ... +class SubSub(Sub): ... + +@final +class Unrelated: ... +``` + +If the positive range completely contains the negative range, then the union is always satisfied. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(Sub, T, Base) | range_constraint(SubSub, T, Super)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(Sub, T, Base) | range_constraint(Sub, T, Base)) +``` + +If the negative range is disjoint from the positive range, the positive range doesn't add anything; +the union is the negative range. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] + reveal_type(negated_range_constraint(Sub, T, Base) | range_constraint(Never, T, Unrelated)) + # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Sub)] + reveal_type(negated_range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_ ≤ Super)] + reveal_type(negated_range_constraint(Base, T, Super) | range_constraint(SubSub, T, Sub)) +``` + +Otherwise we clip the positive constraint to the mininum range that overlaps with the negative +range. + +```py +def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Base) ∨ (Sub ≤ T@_ ≤ Base)] + reveal_type(negated_range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super)) + # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Super) ∨ (Sub ≤ T@_ ≤ Base)] + reveal_type(negated_range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base)) +``` + +### Union of two negated ranges + +The union of two negated ranges has a hole where the ranges "overlap". + +```py +from typing import final +from ty_extensions import negated_range_constraint + +class Super: ... +class Base(Super): ... +class Sub(Base): ... +class SubSub(Sub): ... @final class Unrelated: ... def _[T]() -> None: + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] + reveal_type(negated_range_constraint(SubSub, T, Base) | negated_range_constraint(Sub, T, Super)) + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] + reveal_type(negated_range_constraint(SubSub, T, Super) | negated_range_constraint(Sub, T, Base)) # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Unrelated)) + reveal_type(negated_range_constraint(Sub, T, Base) | negated_range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] + reveal_type(negated_range_constraint(Sub, T, Super) | negated_range_constraint(Sub, T, Super)) ``` -### Union of not-equivalent and incomparable - -When the hole of the non-equivalent constraint and the pivot of the incomparable constraint are not -comparable, then the hole is covered by the incomparable constraint, and the union is therefore -always satisfied. - -```py -from typing import final -from ty_extensions import incomparable_constraint, not_equivalent_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(not_equivalent_constraint(T, Unrelated) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Unrelated)) -``` - -Otherwise, the hole and pivot are comparable, and the non-equivalent constraint subsumes the -incomparable constraint. +If the holes don't overlap, the union is always satisfied. ```py def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Sub)) - - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)] - reveal_type(not_equivalent_constraint(T, Super) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] - reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Sub)] - reveal_type(not_equivalent_constraint(T, Sub) | incomparable_constraint(T, Base)) -``` - -### Union of two incomparables - -We can only simplify the union of two incomparable constraints if they have the same pivot. - -```py -from typing import final -from ty_extensions import incomparable_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -@final -class Unrelated: ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Super)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Super)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Sub)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Unrelated)] - reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Unrelated)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(SubSub, T, Sub) | negated_range_constraint(Base, T, Super)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(negated_range_constraint(SubSub, T, Sub) | negated_range_constraint(Unrelated, T, object)) ``` ## Negation ### Negation of a range constraint -In the negation of a range constraint, the typevar must specialize to a type that is not a subtype -of the lower bound, or is not a supertype of the upper bound. Subtyping is a partial order, so one -type is not a subtype of another if it is a _proper_ supertype, or if they are incomparable. - ```py from typing import Never from ty_extensions import range_constraint @@ -708,62 +544,21 @@ class Base(Super): ... class Sub(Base): ... def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) ∨ (T@_ ≁ Sub) ∨ ((Base ≤ T@_) ∧ (T@_ ≠ Base)) ∨ (T@_ ≁ Base)] + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] reveal_type(~range_constraint(Sub, T, Base)) - # revealed: ty_extensions.ConstraintSet[((Base ≤ T@_) ∧ (T@_ ≠ Base)) ∨ (T@_ ≁ Base)] + # revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] reveal_type(~range_constraint(Never, T, Base)) - # revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) ∨ (T@_ ≁ Sub)] + # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_)] reveal_type(~range_constraint(Sub, T, object)) # revealed: ty_extensions.ConstraintSet[never] reveal_type(~range_constraint(Never, T, object)) ``` -### Negation of a not-equivalent constraint - -In the negation of a not-equivalent constrant, the typevar must specialize to a type that _is_ -equivalent to the hole. The negation does not include types that are incomparable with the hole — -those types are not equivalent to the hole, and are therefore in the original not-equivalent -constraint, not its negation. +The union of a range constraint and its negation should always be satisfiable. ```py -from typing import Never -from ty_extensions import not_equivalent_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)] - reveal_type(~not_equivalent_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Sub)] - reveal_type(~not_equivalent_constraint(T, Sub)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Never)] - reveal_type(~not_equivalent_constraint(T, Never)) - # revealed: ty_extensions.ConstraintSet[(object ≤ T@_)] - reveal_type(~not_equivalent_constraint(T, object)) -``` - -### Negation of an incomparable constraint - -In the negation of an incomparable constraint, the typevar must specialize to a type that _is_ -comparable with (either a subtype _or_ supertype of) the pivot. - -```py -from typing import Never -from ty_extensions import incomparable_constraint - -class Super: ... -class Base(Super): ... -class Sub(Base): ... - -def _[T]() -> None: - # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base) ∨ (Base ≤ T@_)] - reveal_type(~incomparable_constraint(T, Base)) - # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Sub) ∨ (Sub ≤ T@_)] - reveal_type(~incomparable_constraint(T, Sub)) + constraint = range_constraint(Sub, T, Base) # revealed: ty_extensions.ConstraintSet[always] - reveal_type(~incomparable_constraint(T, Never)) - # revealed: ty_extensions.ConstraintSet[always] - reveal_type(~incomparable_constraint(T, object)) + reveal_type(constraint | ~constraint) ``` diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index 7c6028739e..680d6a791a 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -4058,56 +4058,26 @@ impl<'db> Type<'db> { ) .into(), - Some(KnownFunction::RangeConstraint) => Binding::single( - self, - Signature::new( - Parameters::new([ - Parameter::positional_only(Some(Name::new_static("lower_bound"))) - .type_form() - .with_annotated_type(Type::any()), - Parameter::positional_only(Some(Name::new_static("typevar"))) - .type_form() - .with_annotated_type(Type::any()), - Parameter::positional_only(Some(Name::new_static("upper_bound"))) - .type_form() - .with_annotated_type(Type::any()), - ]), - Some(KnownClass::ConstraintSet.to_instance(db)), - ), - ) - .into(), - - Some(KnownFunction::NotEquivalentConstraint) => Binding::single( - self, - Signature::new( - Parameters::new([ - Parameter::positional_only(Some(Name::new_static("typevar"))) - .type_form() - .with_annotated_type(Type::any()), - Parameter::positional_only(Some(Name::new_static("hole"))) - .type_form() - .with_annotated_type(Type::any()), - ]), - Some(KnownClass::ConstraintSet.to_instance(db)), - ), - ) - .into(), - - Some(KnownFunction::IncomparableConstraint) => Binding::single( - self, - Signature::new( - Parameters::new([ - Parameter::positional_only(Some(Name::new_static("typevar"))) - .type_form() - .with_annotated_type(Type::any()), - Parameter::positional_only(Some(Name::new_static("pivot"))) - .type_form() - .with_annotated_type(Type::any()), - ]), - Some(KnownClass::ConstraintSet.to_instance(db)), - ), - ) - .into(), + Some(KnownFunction::RangeConstraint | KnownFunction::NegatedRangeConstraint) => { + Binding::single( + self, + Signature::new( + Parameters::new([ + Parameter::positional_only(Some(Name::new_static("lower_bound"))) + .type_form() + .with_annotated_type(Type::any()), + Parameter::positional_only(Some(Name::new_static("typevar"))) + .type_form() + .with_annotated_type(Type::any()), + Parameter::positional_only(Some(Name::new_static("upper_bound"))) + .type_form() + .with_annotated_type(Type::any()), + ]), + Some(KnownClass::ConstraintSet.to_instance(db)), + ), + ) + .into() + } Some(KnownFunction::IsSingleton | KnownFunction::IsSingleValued) => { Binding::single( diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 635936747b..7087f01301 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -23,25 +23,15 @@ //! set that contains a single clause, where that clause contains no constraints, is always //! satisfiable (`⋃ {⋂ {}} = 1`). //! -//! There are three possible individual constraints: +//! An individual constraint consists of a _positive range_ and zero or more _negative holes_. The +//! positive range and each negative hole consists of a lower and upper bound. A type is within a +//! lower and upper bound if it is a supertype of the lower bound and a subtype of the upper bound. +//! The typevar can specialize to any type that is within the positive range, and is not within any +//! of the negative holes. (You can think of the constraint as the set of types that are within the +//! positive range, with the negative holes "removed" from that set.) //! -//! - A _range_ constraint requires the typevar to be within a particular lower and upper bound: -//! the typevar can only specialize to a type that is a supertype of the lower bound, and a -//! subtype of the upper bound. -//! -//! - A _not-equivalent_ constraint requires the typevar to specialize to anything _other_ than a -//! particular type (the "hole"). -//! -//! - An _incomparable_ constraint requires the typevar to specialize to any type that is neither a -//! subtype nor a supertype of a particular type (the "pivot"). -//! -//! Not-equivalent and incomparable constraints are usually not constructed directly; instead, they -//! typically arise when building up complex combinations of range constraints. -//! -//! Note that all of the types that a constraint compares against — the bounds of a range -//! constraint, the hole of not-equivalent constraint, and the pivot of an incomparable constraint -//! — must be fully static. We take the bottom and top materializations of the types to remove any -//! gradual forms if needed. +//! Note that all lower and upper bounds in a constraint must be fully static. We take the bottom +//! and top materializations of the types to remove any gradual forms if needed. //! //! NOTE: This module is currently in a transitional state. We've added the DNF [`ConstraintSet`] //! representation, and updated all of our property checks to build up a constraint set and then @@ -70,27 +60,6 @@ //! constraint `(int ≤ T ≤ int) ∪ (str ≤ T ≤ str)`. When the lower and upper bounds are the same, //! the constraint says that the typevar must specialize to that _exact_ type, not to a subtype or //! supertype of it. -//! -//! Python does not give us an easy way to construct this, but we can also consider a typevar that -//! can specialize to any type that `T` _cannot_ specialize to — that is, the negation of `T`'s -//! constraint. Another way to write `Never ≤ V ≤ B` is `Never ≤ V ∩ V ≤ B`; if we negate that, we -//! get `¬(Never ≤ V) ∪ ¬(V ≤ B)`, or -//! -//! ```text -//! ((V ≤ Never ∩ V ≠ Never) ∪ V ≁ Never) ∪ ((B ≤ V ∩ V ≠ B) ∪ V ≁ B) -//! ``` -//! -//! The first constraint in the union indicates that `V` can specialize to any type that is a -//! subtype of `Never` or incomparable with `Never`, but not to `Never` itself. -//! -//! The second constraint in the union indicates that `V` can specialize to any type that is a -//! supertype of `B` or incomparable with `B`, but not to `B` itself. (For instance, it _can_ -//! specialize to `A`.) -//! -//! There aren't any types that satisfy the first constraint in the union (the type would have to -//! somehow contain a negative number of values). You can think of a constraint that cannot be -//! satisfied as an empty set (of types), which means we can simplify it out of the union. That -//! gives us a final constraint of `(B ≤ V ∩ V ≠ B) ∪ V ≁ B` for the negation of `T`'s constraint. use std::fmt::Display; @@ -298,23 +267,15 @@ impl<'db> ConstraintSet<'db> { result } - pub(crate) fn not_equivalent( + pub(crate) fn negated_range( db: &'db dyn Db, + lower: Type<'db>, typevar: BoundTypeVarInstance<'db>, - hole: Type<'db>, + upper: Type<'db>, ) -> Self { - let constraint = Constraint::not_equivalent(db, hole).constrain(typevar); - let mut result = Self::never(); - result.union_constraint(db, constraint); - result - } - - pub(crate) fn incomparable( - db: &'db dyn Db, - typevar: BoundTypeVarInstance<'db>, - pivot: Type<'db>, - ) -> Self { - let constraint = Constraint::incomparable(db, pivot).constrain(typevar); + let lower = lower.bottom_materialization(db); + let upper = upper.top_materialization(db); + let constraint = Constraint::negated_range(db, lower, upper).constrain(typevar); let mut result = Self::never(); result.union_constraint(db, constraint); result @@ -457,6 +418,14 @@ pub(crate) struct ConstraintClause<'db> { } impl<'db> ConstraintClause<'db> { + fn new(constraints: SmallVec<[ConstrainedTypeVar<'db>; 1]>) -> Satisfiable { + if constraints.is_empty() { + Satisfiable::Always + } else { + Satisfiable::Constrained(Self { constraints }) + } + } + /// Returns the clause that is always satisfiable. fn always() -> Self { Self { @@ -471,23 +440,6 @@ impl<'db> ConstraintClause<'db> { } } - /// Returns a clause that is the intersection of an iterator of constraints. - fn from_constraints( - db: &'db dyn Db, - constraints: impl IntoIterator>>, - ) -> Satisfiable { - let mut result = Self::always(); - for constraint in constraints { - if result.intersect_constraint(db, constraint) == Satisfiable::Never { - return Satisfiable::Never; - } - } - if result.is_always() { - return Satisfiable::Always; - } - Satisfiable::Constrained(result) - } - /// Returns whether this constraint is always satisfiable. fn is_always(&self) -> bool { self.constraints.is_empty() @@ -530,13 +482,13 @@ impl<'db> ConstraintClause<'db> { for existing in existing_constraints.by_ref() { // Try to simplify the new constraint against an existing constraint. match existing.intersect(db, &constraint) { - Simplifiable::NeverSatisfiable => { + Some(Satisfiable::Never) => { // If two constraints cancel out to 0, that makes the entire clause 0, and all // existing constraints are simplified away. return Satisfiable::Never; } - Simplifiable::AlwaysSatisfiable => { + Some(Satisfiable::Always) => { // If two constraints cancel out to 1, that does NOT cause the entire clause to // become 1. We need to keep whatever constraints have already been added to // the result, and also need to copy over any later constraints that we hadn't @@ -545,19 +497,18 @@ impl<'db> ConstraintClause<'db> { return self.is_satisfiable(); } - Simplifiable::NotSimplified(existing, c) => { + None => { // We couldn't simplify the new constraint relative to this existing // constraint, so add the existing constraint to the result. Continue trying to // simplify the new constraint against the later existing constraints. - self.constraints.push(existing); - constraint = c; + self.constraints.push(existing.clone()); } - Simplifiable::Simplified(c) => { + Some(Satisfiable::Constrained(simplified)) => { // We were able to simplify the new constraint relative to this existing // constraint. Don't add it to the result yet; instead, try to simplify the // result further against later existing constraints. - constraint = c; + constraint = simplified; } } } @@ -678,10 +629,7 @@ impl<'db> ConstraintClause<'db> { // x: A[X1, Y1, Z2] | A[X2, Y2, Z2] // ``` if let Some(simplified) = self.simplifies_via_distribution(db, &other) { - if simplified.is_always() { - return Simplifiable::AlwaysSatisfiable; - } - return Simplifiable::Simplified(simplified); + return simplified; } // Can't be simplified @@ -723,10 +671,28 @@ impl<'db> ConstraintClause<'db> { } /// If the union of two clauses is simpler than either of the individual clauses, returns the - /// union. This happens when (a) they mention the same set of typevars, (b) the union of the - /// constraints for exactly one typevar simplifies to a single constraint, and (c) the - /// constraints for all other typevars are identical. Otherwise returns `None`. - fn simplifies_via_distribution(&self, db: &'db dyn Db, other: &Self) -> Option { + /// union. This happens when they mention the same set of typevars and the constraints for all + /// but one typevar are identical. Moreover, for the other typevar, the union of the + /// constraints for that typevar simplifies to (a) a single constraint, or (b) two constraints + /// where one of them is smaller than before. That is, + /// + /// ```text + /// (A₁ ∩ B ∩ C) ∪ (A₂ ∩ B ∩ C) = A₁₂ ∩ B ∩ C + /// or (A₁' ∪ A₂) ∩ B ∩ C + /// or (A₁ ∪ A₂') ∩ B ∩ C + /// ``` + /// + /// where `B` and `C` are the constraints that are identical for all but one typevar, and `A₁` + /// and `A₂` are the constraints for the other typevar; and where `A₁ ∪ A₂` either simplifies + /// to a single constraint (`A₁₂`), or to a union where either `A₁` or `A₂` becomes smaller + /// (`A₁'` or `A₂'`, respectively). + /// + /// Otherwise returns `None`. + fn simplifies_via_distribution( + &self, + db: &'db dyn Db, + other: &Self, + ) -> Option> { // See the notes in `simplify_clauses` for more details on distribution, including Python // examples that cause it to fire. @@ -750,17 +716,12 @@ impl<'db> ConstraintClause<'db> { if self_constraint == other_constraint { continue; } - let union_constraint = match self_constraint.union(db, other_constraint) { - Simplifiable::NotSimplified(_, _) => { - // The constraints for this typevar are not identical, nor do they - // simplify. - return None; - } - Simplifiable::Simplified(union_constraint) => Some(union_constraint), - Simplifiable::AlwaysSatisfiable => None, - Simplifiable::NeverSatisfiable => { - panic!("unioning two non-never constraints should not be never") - } + let Some(union_constraint) = + self_constraint.simplified_union(db, other_constraint) + else { + // The constraints for this typevar are not identical, nor do they + // simplify. + return None; }; if simplified_index .replace((index, union_constraint)) @@ -779,14 +740,31 @@ impl<'db> ConstraintClause<'db> { return None; }; let mut constraints = self.constraints.clone(); - if let Some(union_constraint) = union_constraint { - constraints[index] = union_constraint; - } else { - // If the simplified union of constraints is Always, then we can remove this typevar - // from the constraint completely. - constraints.remove(index); + match union_constraint { + Simplifiable::NeverSatisfiable => { + panic!("unioning two non-never constraints should not be never") + } + Simplifiable::AlwaysSatisfiable => { + // If the simplified union of constraints is Always, then we can remove this typevar + // from the constraint completely. + constraints.remove(index); + Some(Simplifiable::from_one(Self::new(constraints))) + } + Simplifiable::Simplified(union_constraint) => { + constraints[index] = union_constraint; + Some(Simplifiable::from_one(Self::new(constraints))) + } + Simplifiable::NotSimplified(left, right) => { + let mut left_constraints = constraints.clone(); + let mut right_constraints = constraints; + left_constraints[index] = left; + right_constraints[index] = right; + Some(Simplifiable::from_union( + Self::new(left_constraints), + Self::new(right_constraints), + )) + } } - Some(Self { constraints }) } /// Returns the negation of this clause. The result is a set since negating an intersection @@ -811,7 +789,10 @@ impl<'db> ConstraintClause<'db> { return f.write_str("1"); } - if self.clause.constraints.len() > 1 { + let clause_count: usize = (self.clause.constraints.iter()) + .map(ConstrainedTypeVar::clause_count) + .sum(); + if clause_count > 1 { f.write_str("(")?; } for (i, constraint) in self.clause.constraints.iter().enumerate() { @@ -820,7 +801,7 @@ impl<'db> ConstraintClause<'db> { } constraint.display(self.db).fmt(f)?; } - if self.clause.constraints.len() > 1 { + if clause_count > 1 { f.write_str(")")?; } Ok(()) @@ -838,24 +819,34 @@ pub(crate) struct ConstrainedTypeVar<'db> { } impl<'db> ConstrainedTypeVar<'db> { - /// Returns the intersection of this individual constraint and another. - fn intersect(&self, db: &'db dyn Db, other: &Self) -> Simplifiable { - if self.typevar != other.typevar { - return Simplifiable::NotSimplified(self.clone(), other.clone()); - } - self.constraint - .intersect(db, &other.constraint) - .map(|constraint| constraint.constrain(self.typevar)) + fn clause_count(&self) -> usize { + self.constraint.clause_count() } - /// Returns the union of this individual constraint and another. - fn union(&self, db: &'db dyn Db, other: &Self) -> Simplifiable { + /// Returns the intersection of this individual constraint and another, or `None` if the two + /// constraints do not refer to the same typevar (and therefore cannot be simplified to a + /// single constraint). + fn intersect(&self, db: &'db dyn Db, other: &Self) -> Option> { if self.typevar != other.typevar { - return Simplifiable::NotSimplified(self.clone(), other.clone()); + return None; + } + Some( + self.constraint + .intersect(db, &other.constraint) + .map(|constraint| constraint.constrain(self.typevar)), + ) + } + + /// Returns the union of this individual constraint and another, if it can be simplified to a + /// union of two constraints or fewer. Returns `None` if the union cannot be simplified that + /// much. + fn simplified_union(&self, db: &'db dyn Db, other: &Self) -> Option> { + if self.typevar != other.typevar { + return None; } self.constraint - .union(db, &other.constraint) - .map(|constraint| constraint.constrain(self.typevar)) + .simplified_union(db, &other.constraint) + .map(|constraint| constraint.map(|constraint| constraint.constrain(self.typevar))) } /// Adds the negation of this individual constraint to a constraint set. @@ -868,7 +859,7 @@ impl<'db> ConstrainedTypeVar<'db> { fn subsumes(&self, db: &'db dyn Db, other: &Self) -> bool { debug_assert_eq!(self.typevar, other.typevar); match self.intersect(db, other) { - Simplifiable::Simplified(intersection) => intersection == *self, + Some(Satisfiable::Constrained(intersection)) => intersection == *self, _ => false, } } @@ -879,10 +870,9 @@ impl<'db> ConstrainedTypeVar<'db> { } #[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)] -pub(crate) enum Constraint<'db> { - Range(RangeConstraint<'db>), - NotEquivalent(NotEquivalentConstraint<'db>), - Incomparable(IncomparableConstraint<'db>), +pub(crate) struct Constraint<'db> { + positive: RangeConstraint<'db>, + negative: SmallVec<[NegatedRangeConstraint<'db>; 1]>, } impl<'db> Constraint<'db> { @@ -893,62 +883,228 @@ impl<'db> Constraint<'db> { } } - fn intersect(&self, db: &'db dyn Db, other: &Constraint<'db>) -> Simplifiable> { - match (self, other) { - (Constraint::Range(left), Constraint::Range(right)) => left.intersect_range(db, right), - - (Constraint::Range(range), Constraint::NotEquivalent(not_equivalent)) - | (Constraint::NotEquivalent(not_equivalent), Constraint::Range(range)) => { - range.intersect_not_equivalent(db, not_equivalent) - } - - (Constraint::Range(range), Constraint::Incomparable(incomparable)) - | (Constraint::Incomparable(incomparable), Constraint::Range(range)) => { - range.intersect_incomparable(db, incomparable) - } - - (Constraint::NotEquivalent(left), Constraint::NotEquivalent(right)) => { - left.intersect_not_equivalent(db, right) - } - - (Constraint::NotEquivalent(not_equivalent), Constraint::Incomparable(incomparable)) - | (Constraint::Incomparable(incomparable), Constraint::NotEquivalent(not_equivalent)) => { - not_equivalent.intersect_incomparable(db, incomparable) - } - - (Constraint::Incomparable(left), Constraint::Incomparable(right)) => { - left.intersect_incomparable(db, right) - } - } + fn clause_count(&self) -> usize { + usize::from(!self.positive.is_always()) + self.negative.len() } - fn union(&self, db: &'db dyn Db, other: &Constraint<'db>) -> Simplifiable> { - match (self, other) { - (Constraint::Range(left), Constraint::Range(right)) => left.union_range(db, right), + fn satisfiable(self, db: &'db dyn Db) -> Satisfiable { + if self.positive.is_always() && self.negative.is_empty() { + return Satisfiable::Always; + } + if (self.negative.iter()).any(|negative| negative.hole.contains(db, &self.positive)) { + return Satisfiable::Never; + } + Satisfiable::Constrained(self) + } - (Constraint::Range(range), Constraint::NotEquivalent(not_equivalent)) - | (Constraint::NotEquivalent(not_equivalent), Constraint::Range(range)) => { - range.union_not_equivalent(db, not_equivalent) + fn intersect(&self, db: &'db dyn Db, other: &Constraint<'db>) -> Satisfiable> { + let Some(positive) = self.positive.intersect(db, &other.positive) else { + // If the positive intersection is empty, none of the negative holes matter, since + // there are no types for the holes to remove. + return Satisfiable::Never; + }; + + // The negative portion of the intersection is given by + // + // ¬(s₁ ≤ α ≤ t₁) ∧ ¬(s₂ ≤ α ≤ t₂) = ¬((s₁ ≤ α ≤ t₁) ∨ (s₂ ≤ α ≤ t₂)) + // + // That is, we union together the holes from `self` and `other`. If any of the holes + // entirely contain another, we can simplify those two down to the larger hole. We use the + // same trick as above in `union_clause` and `intersect_constraint` to look for pairs that + // we can simplify. + // + // We also want to clip each negative hole to the minimum range that overlaps with the + // positive range. We'll do that now to all of the holes from `self`, and we'll do that to + // holes from `other` below when we try to simplify them. + let mut previous: SmallVec<[NegatedRangeConstraint<'db>; 1]> = SmallVec::new(); + let mut current: SmallVec<_> = (self.negative.iter()) + .filter_map(|negative| negative.clip_to_positive(db, &positive)) + .collect(); + for other_negative in &other.negative { + let Some(mut other_negative) = other_negative.clip_to_positive(db, &positive) else { + continue; + }; + std::mem::swap(&mut previous, &mut current); + let mut previous_negative = previous.iter(); + for self_negative in previous_negative.by_ref() { + match self_negative.intersect_negative(db, &other_negative) { + None => { + // We couldn't simplify the new hole relative to this existing holes, so + // add the existing hole to the result. Continue trying to simplify the new + // hole against the later existing holes. + current.push(self_negative.clone()); + } + + Some(union) => { + // We were able to simplify the new hole relative to this existing hole. + // Don't add it to the result yet; instead, try to simplify the result + // further against later existing holes. + other_negative = union.clone(); + } + } } - (Constraint::Range(range), Constraint::Incomparable(incomparable)) - | (Constraint::Incomparable(incomparable), Constraint::Range(range)) => { - range.union_incomparable(db, incomparable) + // If we fall through then we need to add the new hole to the hole list (either because + // we couldn't simplify it with anything, or because we did without it canceling out). + current.push(other_negative); + } + + let result = Self { + positive, + negative: current, + }; + result.satisfiable(db) + } + + fn simplified_union( + &self, + db: &'db dyn Db, + other: &Constraint<'db>, + ) -> Option>> { + // (ap ∧ ¬an₁ ∧ ¬an₂ ∧ ...) ∨ (bp ∧ ¬bn₁ ∧ ¬bn₂ ∧ ...) + // = (ap ∨ bp) ∧ (ap ∨ ¬bn₁) ∧ (ap ∨ ¬bn₂) ∧ ... + // ∧ (¬an₁ ∨ bp) ∧ (¬an₁ ∨ ¬bn₁) ∧ (¬an₁ ∨ ¬bn₂) ∧ ... + // ∧ (¬an₂ ∨ bp) ∧ (¬an₂ ∨ ¬bn₁) ∧ (¬an₂ ∨ ¬bn₂) ∧ ... + // + // We use a helper type to build up the result of the union of two constraints, since we + // need to calculate the Cartesian product of the the positive and negative portions of the + // two inputs. We cannot use `ConstraintSet` for this, since it would try to invoke the + // `simplify_union` logic, which this method is part of the definition of! So we have to + // reproduce some of that logic here, in a simplified form since we know we're only ever + // looking at pairs of individual constraints at a time. + + struct Results<'db> { + next: Vec>, + results: Vec>, + } + + impl<'db> Results<'db> { + fn new(constraint: Constraint<'db>) -> Results<'db> { + Results { + next: vec![], + results: vec![constraint], + } } - (Constraint::NotEquivalent(left), Constraint::NotEquivalent(right)) => { - left.union_not_equivalent(db, right) + fn flip(&mut self) { + std::mem::swap(&mut self.next, &mut self.results); + self.next.clear(); } - (Constraint::NotEquivalent(not_equivalent), Constraint::Incomparable(incomparable)) - | (Constraint::Incomparable(incomparable), Constraint::NotEquivalent(not_equivalent)) => { - not_equivalent.union_incomparable(db, incomparable) + /// Adds a constraint by intersecting it with any currently pending results. + fn add_constraint(&mut self, db: &'db dyn Db, constraint: &Constraint<'db>) { + self.next.extend(self.results.iter().filter_map(|result| { + match result.intersect(db, constraint) { + Satisfiable::Never => None, + Satisfiable::Always => Some(Constraint { + positive: RangeConstraint::always(), + negative: smallvec![], + }), + Satisfiable::Constrained(constraint) => Some(constraint), + } + })); } - (Constraint::Incomparable(left), Constraint::Incomparable(right)) => { - left.union_incomparable(db, right) + /// Adds a single negative range constraint to the pending results. + fn add_negated_range( + &mut self, + db: &'db dyn Db, + negative: Option>, + ) { + let negative = match negative { + Some(negative) => Constraint { + positive: RangeConstraint::always(), + negative: smallvec![negative], + }, + // If the intersection of these two holes is empty, then they don't remove + // anything from the final union. + None => return, + }; + self.add_constraint(db, &negative); + self.flip(); + } + + /// Adds a possibly simplified constraint to the pending results. If the parameter has + /// been simplified to a single constraint, it is intersected with each currently + /// pending result. If it could not be simplified (i.e., it is the union of two + /// constraints), then we duplicate any pending results, so that we can _separately_ + /// intersect each non-simplified constraint with the results. + fn add_simplified_constraint( + &mut self, + db: &'db dyn Db, + constraints: Simplifiable>, + ) { + match constraints { + Simplifiable::NeverSatisfiable => { + self.results.clear(); + return; + } + Simplifiable::AlwaysSatisfiable => { + return; + } + Simplifiable::Simplified(constraint) => { + self.add_constraint(db, &constraint); + } + Simplifiable::NotSimplified(first, second) => { + self.add_constraint(db, &first); + self.add_constraint(db, &second); + } + } + self.flip(); + } + + /// If there are two or fewer final results, translates them into a [`Simplifiable`] + /// result. Otherwise returns `None`, indicating that the union cannot be simplified + /// enough for our purposes. + fn into_result(self, db: &'db dyn Db) -> Option>> { + let mut results = self.results.into_iter(); + let Some(first) = results.next() else { + return Some(Simplifiable::NeverSatisfiable); + }; + let Some(second) = results.next() else { + return Some(Simplifiable::from_one(first.satisfiable(db))); + }; + if results.next().is_some() { + return None; + } + Some(Simplifiable::from_union( + first.satisfiable(db), + second.satisfiable(db), + )) } } + + let mut results = match self.positive.union(db, &other.positive) { + Some(positive) => Results::new(Constraint { + positive: positive.clone(), + negative: smallvec![], + }), + None => return None, + }; + for other_negative in &other.negative { + results.add_simplified_constraint( + db, + self.positive.union_negated_range(db, other_negative), + ); + } + for self_negative in &self.negative { + // Reverse the results here so that we always add items from `self` first. This ensures + // that the output we produce is ordered consistently with the input we receive. + results.add_simplified_constraint( + db, + other + .positive + .union_negated_range(db, self_negative) + .reverse(), + ); + } + for self_negative in &self.negative { + for other_negative in &other.negative { + results.add_negated_range(db, self_negative.union_negative(db, other_negative)); + } + } + + results.into_result(db) } fn negate_into( @@ -957,11 +1113,17 @@ impl<'db> Constraint<'db> { typevar: BoundTypeVarInstance<'db>, set: &mut ConstraintSet<'db>, ) { - match self { - Constraint::Range(constraint) => constraint.negate_into(db, typevar, set), - Constraint::NotEquivalent(constraint) => constraint.negate_into(db, typevar, set), - Constraint::Incomparable(constraint) => constraint.negate_into(db, typevar, set), + for negative in &self.negative { + set.union_constraint( + db, + Constraint::range(db, negative.hole.lower, negative.hole.upper).constrain(typevar), + ); } + set.union_constraint( + db, + Constraint::negated_range(db, self.positive.lower, self.positive.upper) + .constrain(typevar), + ); } fn display(&self, db: &'db dyn Db, typevar: impl Display) -> impl Display { @@ -973,17 +1135,22 @@ impl<'db> Constraint<'db> { impl Display for DisplayConstraint<'_, '_, D> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match self.constraint { - Constraint::Range(constraint) => { - constraint.display(self.db, &self.typevar).fmt(f) - } - Constraint::NotEquivalent(constraint) => { - constraint.display(self.db, &self.typevar).fmt(f) - } - Constraint::Incomparable(constraint) => { - constraint.display(self.db, &self.typevar).fmt(f) - } + let mut first = true; + if !self.constraint.positive.is_always() { + (self.constraint.positive) + .display(self.db, &self.typevar) + .fmt(f)?; + first = false; } + for negative in &self.constraint.negative { + if first { + first = false; + } else { + f.write_str(" ∧ ")?; + } + negative.display(self.db, &self.typevar).fmt(f)?; + } + Ok(()) } } @@ -1023,164 +1190,101 @@ impl<'db> Constraint<'db> { // If the requested constraint is `Never ≤ T ≤ object`, then the typevar can be specialized // to _any_ type, and the constraint does nothing. - if lower.is_never() && upper.is_object() { + let positive = RangeConstraint { lower, upper }; + if positive.is_always() { return Satisfiable::Always; } - Satisfiable::Constrained(Constraint::Range(RangeConstraint { lower, upper })) + Satisfiable::Constrained(Constraint { + positive, + negative: smallvec![], + }) } } impl<'db> RangeConstraint<'db> { - fn intersect_range( - &self, - db: &'db dyn Db, - other: &RangeConstraint<'db>, - ) -> Simplifiable> { - // (s₁ ≤ α ≤ t₁) ∧ (s₂ ≤ α ≤ t₂) = (s₁ ∪ s₂) ≤ α (t₁ ∩ t₂) - Simplifiable::from_one(Constraint::range( - db, - UnionType::from_elements(db, [self.lower, other.lower]), - IntersectionType::from_elements(db, [self.upper, other.upper]), - )) + fn always() -> Self { + Self { + lower: Type::Never, + upper: Type::object(), + } } - fn intersect_not_equivalent( - &self, - db: &'db dyn Db, - other: &NotEquivalentConstraint<'db>, - ) -> Simplifiable> { - // If the range constraint says that the typevar must be equivalent to some type, and the - // not-equivalent type says that it must not, we have a contradiction. - if self.lower.is_equivalent_to(db, self.upper) && self.lower.is_equivalent_to(db, other.ty) - { - return Simplifiable::NeverSatisfiable; - } - - // If the "hole" of the not-equivalent type is not contained in the range, the the - // intersection simplifies to the range. - if !self.lower.is_subtype_of(db, other.ty) || !other.ty.is_subtype_of(db, self.upper) { - return Simplifiable::Simplified(Constraint::Range(self.clone())); - } - - // Otherwise the result cannot be simplified. - Simplifiable::NotSimplified( - Constraint::Range(self.clone()), - Constraint::NotEquivalent(other.clone()), - ) + fn contains(&self, db: &'db dyn Db, other: &RangeConstraint<'db>) -> bool { + self.lower.is_subtype_of(db, other.lower) && other.upper.is_subtype_of(db, self.upper) } - fn intersect_incomparable( - &self, - db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - if other.ty.is_subtype_of(db, self.lower) || self.upper.is_subtype_of(db, other.ty) { - return Simplifiable::NeverSatisfiable; - } - - // A range constraint and an incomparable constraint cannot be simplified. - Simplifiable::NotSimplified( - Constraint::Range(self.clone()), - Constraint::Incomparable(other.clone()), - ) + fn is_always(&self) -> bool { + self.lower.is_never() && self.upper.is_object() } - fn union_range( - &self, - db: &'db dyn Db, - other: &RangeConstraint<'db>, - ) -> Simplifiable> { + /// Returns the intersection of two range constraints, or `None` if the intersection is empty. + fn intersect(&self, db: &'db dyn Db, other: &RangeConstraint<'db>) -> Option { + // (s₁ ≤ α ≤ t₁) ∧ (s₂ ≤ α ≤ t₂) = (s₁ ∪ s₂) ≤ α ≤ (t₁ ∩ t₂)) + let lower = UnionType::from_elements(db, [self.lower, other.lower]); + let upper = IntersectionType::from_elements(db, [self.upper, other.upper]); + + // If `lower ≰ upper`, then the intersection is empty, since there is no type that is both + // greater than `lower`, and less than `upper`. + if !lower.is_subtype_of(db, upper) { + return None; + } + + Some(Self { lower, upper }) + } + + /// Returns the union of two range constraints if it can be simplified to a single constraint. + /// Otherwise returns `None`. + fn union(&self, db: &'db dyn Db, other: &RangeConstraint<'db>) -> Option { // When one of the bounds is entirely contained within the other, the union simplifies to // the larger bounds. if self.lower.is_subtype_of(db, other.lower) && other.upper.is_subtype_of(db, self.upper) { - return Simplifiable::Simplified(Constraint::Range(self.clone())); + return Some(self.clone()); } if other.lower.is_subtype_of(db, self.lower) && self.upper.is_subtype_of(db, other.upper) { - return Simplifiable::Simplified(Constraint::Range(other.clone())); + return Some(other.clone()); } // Otherwise the result cannot be simplified. - Simplifiable::NotSimplified( - Constraint::Range(self.clone()), - Constraint::Range(other.clone()), - ) + None } - fn union_not_equivalent( + /// Returns the union of a positive range with a negative hole. + fn union_negated_range( &self, db: &'db dyn Db, - other: &NotEquivalentConstraint<'db>, + negated: &NegatedRangeConstraint<'db>, ) -> Simplifiable> { - // When the range constraint contains the "hole" from the non-equivalent constraint, then - // the range constraint fills in the hole, and the result is always satisfiable. - if self.lower.is_subtype_of(db, other.ty) && other.ty.is_subtype_of(db, self.upper) { + // If the positive range completely contains the negative range, then the union is always + // satisfied. + if self.contains(db, &negated.hole) { return Simplifiable::AlwaysSatisfiable; } - // Otherwise the range constraint is subsumed by the non-equivalent constraint. - Simplifiable::Simplified(Constraint::NotEquivalent(other.clone())) - } - - fn union_incomparable( - &self, - db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - // When the "pivot" of the incomparable constraint is not comparable with either bound of - // the range constraint, the incomparable constraint subsumes the range constraint. - if incomparable(db, self.lower, other.ty) && incomparable(db, self.upper, other.ty) { - return Simplifiable::Simplified(Constraint::Incomparable(other.clone())); + // If the positive range is disjoint from the negative range, the positive range doesn't + // add anything; the union is the negative range. + if incomparable(db, self.lower, negated.hole.upper) + || incomparable(db, negated.hole.lower, self.upper) + { + return Simplifiable::from_one(Constraint::negated_range( + db, + negated.hole.lower, + negated.hole.upper, + )); } - // Otherwise the result cannot be simplified. - Simplifiable::NotSimplified( - Constraint::Range(self.clone()), - Constraint::Incomparable(other.clone()), + // Otherwise we clip the positive constraint to the minimum range that overlaps with the + // negative range. + Simplifiable::from_union( + Constraint::range( + db, + UnionType::from_elements(db, [self.lower, negated.hole.lower]), + IntersectionType::from_elements(db, [self.upper, negated.hole.upper]), + ), + Constraint::negated_range(db, negated.hole.lower, negated.hole.upper), ) } - fn negate_into( - &self, - db: &'db dyn Db, - typevar: BoundTypeVarInstance<'db>, - set: &mut ConstraintSet<'db>, - ) { - // Lower bound: - // ¬(s ≤ α) = ((α ≤ s) ∧ α ≠ s) ∨ (a ≁ s) - set.union_clause( - db, - ConstraintClause::from_constraints( - db, - [ - Constraint::range(db, Type::Never, self.lower).constrain(typevar), - Constraint::not_equivalent(db, self.lower).constrain(typevar), - ], - ), - ); - set.union_constraint( - db, - Constraint::incomparable(db, self.lower).constrain(typevar), - ); - - // Upper bound: - // ¬(α ≤ t) = ((t ≤ α) ∧ α ≠ t) ∨ (a ≁ t) - set.union_clause( - db, - ConstraintClause::from_constraints( - db, - [ - Constraint::range(db, self.upper, Type::object()).constrain(typevar), - Constraint::not_equivalent(db, self.upper).constrain(typevar), - ], - ), - ); - set.union_constraint( - db, - Constraint::incomparable(db, self.upper).constrain(typevar), - ); - } - fn display(&self, db: &'db dyn Db, typevar: impl Display) -> impl Display { struct DisplayRangeConstraint<'a, 'db, D> { constraint: &'a RangeConstraint<'db>, @@ -1190,6 +1294,15 @@ impl<'db> RangeConstraint<'db> { impl Display for DisplayRangeConstraint<'_, '_, D> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if (self.constraint.lower).is_equivalent_to(self.db, self.constraint.upper) { + return write!( + f, + "({} = {})", + &self.typevar, + self.constraint.lower.display(self.db) + ); + } + f.write_str("(")?; if !self.constraint.lower.is_never() { write!(f, "{} ≤ ", self.constraint.lower.display(self.db))?; @@ -1211,206 +1324,103 @@ impl<'db> RangeConstraint<'db> { } #[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)] -pub(crate) struct NotEquivalentConstraint<'db> { - ty: Type<'db>, +pub(crate) struct NegatedRangeConstraint<'db> { + hole: RangeConstraint<'db>, } impl<'db> Constraint<'db> { - /// Returns a new not-equivalent constraint. + /// Returns a new negated range constraint. /// - /// Panics if `ty` is not fully static. - fn not_equivalent(db: &'db dyn Db, ty: Type<'db>) -> Satisfiable> { - debug_assert_eq!(ty, ty.top_materialization(db)); - Satisfiable::Constrained(Constraint::NotEquivalent(NotEquivalentConstraint { ty })) - } -} - -impl<'db> NotEquivalentConstraint<'db> { - fn intersect_not_equivalent( - &self, + /// Panics if `lower` and `upper` are not both fully static. + fn negated_range( db: &'db dyn Db, - other: &NotEquivalentConstraint<'db>, - ) -> Simplifiable> { - if self.ty.is_equivalent_to(db, other.ty) { - return Simplifiable::Simplified(Constraint::NotEquivalent(self.clone())); - } - Simplifiable::NotSimplified( - Constraint::NotEquivalent(self.clone()), - Constraint::NotEquivalent(other.clone()), - ) - } + lower: Type<'db>, + upper: Type<'db>, + ) -> Satisfiable> { + debug_assert_eq!(lower, lower.bottom_materialization(db)); + debug_assert_eq!(upper, upper.top_materialization(db)); - fn intersect_incomparable( - &self, - db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - // If the hole and pivot are comparable, then removing the hole from the incomparable - // constraint doesn't do anything. - if comparable(db, self.ty, other.ty) { - return Simplifiable::Simplified(Constraint::Incomparable(other.clone())); - } - Simplifiable::NotSimplified( - Constraint::NotEquivalent(self.clone()), - Constraint::Incomparable(other.clone()), - ) - } - - fn union_not_equivalent( - &self, - db: &'db dyn Db, - other: &NotEquivalentConstraint<'db>, - ) -> Simplifiable> { - if self.ty.is_equivalent_to(db, other.ty) { - return Simplifiable::Simplified(Constraint::NotEquivalent(self.clone())); - } - Simplifiable::AlwaysSatisfiable - } - - fn union_incomparable( - &self, - db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - // When the "hole" of the non-equivalent constraint and the "pivot" of the incomparable - // constraint are not comparable, then the hole is covered by the incomparable constraint, - // and the union is therefore always satisfied. - if incomparable(db, self.ty, other.ty) { - return Simplifiable::AlwaysSatisfiable; + // If `lower ≰ upper`, then the negated constraint is always satisfied, since there is no + // type that is both greater than `lower`, and less than `upper`. + if !lower.is_subtype_of(db, upper) { + return Satisfiable::Always; } - // Otherwise, the hole and pivot are comparable, and the non-equivalent constraint subsumes - // the incomparable constraint. - Simplifiable::Simplified(Constraint::NotEquivalent(self.clone())) - } - - fn negate_into( - &self, - db: &'db dyn Db, - typevar: BoundTypeVarInstance<'db>, - set: &mut ConstraintSet<'db>, - ) { - // Not equivalent: - // ¬(α ≠ t) = (t ≤ α ≤ t) - set.union_constraint( - db, - Constraint::range(db, self.ty, self.ty).constrain(typevar), - ); - } - - fn display(&self, db: &'db dyn Db, typevar: impl Display) -> impl Display { - struct DisplayNotEquivalentConstraint<'a, 'db, D> { - constraint: &'a NotEquivalentConstraint<'db>, - typevar: D, - db: &'db dyn Db, - } - - impl Display for DisplayNotEquivalentConstraint<'_, '_, D> { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!( - f, - "({} ≠ {})", - self.typevar, - self.constraint.ty.display(self.db) - ) - } - } - - DisplayNotEquivalentConstraint { - constraint: self, - typevar, - db, - } - } -} - -#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)] -pub(crate) struct IncomparableConstraint<'db> { - ty: Type<'db>, -} - -impl<'db> Constraint<'db> { - /// Returns a new incomparable constraint. - /// - /// Panics if `ty` is not fully static. - fn incomparable(db: &'db dyn Db, ty: Type<'db>) -> Satisfiable> { - debug_assert_eq!(ty, ty.top_materialization(db)); - - // Every type is comparable to Never and to object. - if ty.is_never() || ty.is_object() { + // If the requested constraint is `¬(Never ≤ T ≤ object)`, then the constraint cannot be + // satisfied. + let negative = NegatedRangeConstraint { + hole: RangeConstraint { lower, upper }, + }; + if negative.hole.is_always() { return Satisfiable::Never; } - Satisfiable::Constrained(Constraint::Incomparable(IncomparableConstraint { ty })) + Satisfiable::Constrained(Constraint { + positive: RangeConstraint::always(), + negative: smallvec![negative], + }) } } -impl<'db> IncomparableConstraint<'db> { - fn intersect_incomparable( - &self, - db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - if self.ty.is_equivalent_to(db, other.ty) { - return Simplifiable::Simplified(Constraint::Incomparable(other.clone())); - } - Simplifiable::NotSimplified( - Constraint::Incomparable(self.clone()), - Constraint::Incomparable(other.clone()), - ) +impl<'db> NegatedRangeConstraint<'db> { + /// Clips this negative hole to be the smallest hole that removes the same types from the given + /// positive range. + fn clip_to_positive(&self, db: &'db dyn Db, positive: &RangeConstraint<'db>) -> Option { + self.hole + .intersect(db, positive) + .map(|hole| NegatedRangeConstraint { hole }) } - fn union_incomparable( + /// Returns the union of two negative constraints. (This this is _intersection_ of the + /// constraints' holes.) + fn union_negative( &self, db: &'db dyn Db, - other: &IncomparableConstraint<'db>, - ) -> Simplifiable> { - if self.ty.is_equivalent_to(db, other.ty) { - return Simplifiable::Simplified(Constraint::Incomparable(other.clone())); - } - Simplifiable::NotSimplified( - Constraint::Incomparable(self.clone()), - Constraint::Incomparable(other.clone()), - ) + positive: &NegatedRangeConstraint<'db>, + ) -> Option { + self.hole + .intersect(db, &positive.hole) + .map(|hole| NegatedRangeConstraint { hole }) } - fn negate_into( + /// Returns the intersection of two negative constraints. (This this is _union_ of the + /// constraints' holes.) + fn intersect_negative( &self, db: &'db dyn Db, - typevar: BoundTypeVarInstance<'db>, - set: &mut ConstraintSet<'db>, - ) { - // Not comparable: - // ¬(α ≁ t) = (t ≤ α) ∨ (α ≤ t) - set.union_constraint( - db, - Constraint::range(db, Type::Never, self.ty).constrain(typevar), - ); - set.union_constraint( - db, - Constraint::range(db, self.ty, Type::object()).constrain(typevar), - ); + other: &NegatedRangeConstraint<'db>, + ) -> Option { + self.hole + .union(db, &other.hole) + .map(|hole| NegatedRangeConstraint { hole }) } fn display(&self, db: &'db dyn Db, typevar: impl Display) -> impl Display { - struct DisplayIncomparableConstraint<'a, 'db, D> { - constraint: &'a IncomparableConstraint<'db>, + struct DisplayNegatedRangeConstraint<'a, 'db, D> { + constraint: &'a NegatedRangeConstraint<'db>, typevar: D, db: &'db dyn Db, } - impl Display for DisplayIncomparableConstraint<'_, '_, D> { + impl Display for DisplayNegatedRangeConstraint<'_, '_, D> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!( - f, - "({} ≁ {})", - self.typevar, - self.constraint.ty.display(self.db) - ) + if (self.constraint.hole.lower) + .is_equivalent_to(self.db, self.constraint.hole.upper) + { + return write!( + f, + "({} ≠ {})", + &self.typevar, + self.constraint.hole.lower.display(self.db) + ); + } + + f.write_str("¬")?; + self.constraint.hole.display(self.db, &self.typevar).fmt(f) } } - DisplayIncomparableConstraint { + DisplayNegatedRangeConstraint { constraint: self, typevar, db, @@ -1456,6 +1466,22 @@ impl Simplifiable { Satisfiable::Constrained(constraint) => Simplifiable::Simplified(constraint), } } +} + +impl Simplifiable { + fn from_union(first: Satisfiable, second: Satisfiable) -> Self { + match (first, second) { + (Satisfiable::Always, _) | (_, Satisfiable::Always) => Simplifiable::AlwaysSatisfiable, + (Satisfiable::Never, Satisfiable::Never) => Simplifiable::NeverSatisfiable, + (Satisfiable::Never, Satisfiable::Constrained(constraint)) + | (Satisfiable::Constrained(constraint), Satisfiable::Never) => { + Simplifiable::Simplified(constraint) + } + (Satisfiable::Constrained(first), Satisfiable::Constrained(second)) => { + Simplifiable::NotSimplified(first, second) + } + } + } fn map(self, mut f: impl FnMut(T) -> U) -> Simplifiable { match self { @@ -1465,4 +1491,13 @@ impl Simplifiable { Simplifiable::NotSimplified(t1, t2) => Simplifiable::NotSimplified(f(t1), f(t2)), } } + + fn reverse(self) -> Self { + match self { + Simplifiable::NeverSatisfiable + | Simplifiable::AlwaysSatisfiable + | Simplifiable::Simplified(_) => self, + Simplifiable::NotSimplified(t1, t2) => Simplifiable::NotSimplified(t2, t1), + } + } } diff --git a/crates/ty_python_semantic/src/types/function.rs b/crates/ty_python_semantic/src/types/function.rs index 4d9fdfb756..585ecbc2da 100644 --- a/crates/ty_python_semantic/src/types/function.rs +++ b/crates/ty_python_semantic/src/types/function.rs @@ -1259,10 +1259,8 @@ pub enum KnownFunction { RevealProtocolInterface, /// `ty_extensions.range_constraint` RangeConstraint, - /// `ty_extensions.not_equivalent_constraint` - NotEquivalentConstraint, - /// `ty_extensions.incomparable_constraint` - IncomparableConstraint, + /// `ty_extensions.negated_range_constraint` + NegatedRangeConstraint, } impl KnownFunction { @@ -1330,8 +1328,7 @@ impl KnownFunction { | Self::HasMember | Self::RevealProtocolInterface | Self::RangeConstraint - | Self::NotEquivalentConstraint - | Self::IncomparableConstraint + | Self::NegatedRangeConstraint | Self::AllMembers => module.is_ty_extensions(), Self::ImportModule => module.is_importlib(), } @@ -1644,61 +1641,17 @@ impl KnownFunction { ))); } - KnownFunction::NotEquivalentConstraint => { - let [Some(Type::NonInferableTypeVar(typevar)), Some(hole)] = parameter_types else { - return; - }; - - if !hole.is_equivalent_to(db, hole.top_materialization(db)) { - if let Some(builder) = - context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression) - { - let mut diagnostic = builder.into_diagnostic(format_args!( - "Not-equivalent constraint must have a fully static type" - )); - diagnostic.annotate( - Annotation::secondary(context.span(&call_expression.arguments.args[1])) - .message(format_args!( - "Type `{}` is not fully static", - hole.display(db) - )), - ); - } - return; - } - - let constraints = ConstraintSet::not_equivalent(db, *typevar, *hole); - let tracked = TrackedConstraintSet::new(db, constraints); - overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet( - tracked, - ))); - } - - KnownFunction::IncomparableConstraint => { - let [Some(Type::NonInferableTypeVar(typevar)), Some(pivot)] = parameter_types + KnownFunction::NegatedRangeConstraint => { + let [ + Some(lower), + Some(Type::NonInferableTypeVar(typevar)), + Some(upper), + ] = parameter_types else { return; }; - if !pivot.is_equivalent_to(db, pivot.top_materialization(db)) { - if let Some(builder) = - context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression) - { - let mut diagnostic = builder.into_diagnostic(format_args!( - "Incomparable constraint must have a fully static type" - )); - diagnostic.annotate( - Annotation::secondary(context.span(&call_expression.arguments.args[1])) - .message(format_args!( - "Type `{}` is not fully static", - pivot.display(db) - )), - ); - } - return; - } - - let constraints = ConstraintSet::incomparable(db, *typevar, *pivot); + let constraints = ConstraintSet::negated_range(db, *lower, *typevar, *upper); let tracked = TrackedConstraintSet::new(db, constraints); overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet( tracked, @@ -1837,8 +1790,7 @@ pub(crate) mod tests { | KnownFunction::HasMember | KnownFunction::RevealProtocolInterface | KnownFunction::RangeConstraint - | KnownFunction::NotEquivalentConstraint - | KnownFunction::IncomparableConstraint + | KnownFunction::NegatedRangeConstraint | KnownFunction::AllMembers => KnownModule::TyExtensions, KnownFunction::ImportModule => KnownModule::ImportLib, diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi index 6b09ce0b97..ccaf90a06e 100644 --- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi +++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi @@ -50,8 +50,9 @@ class ConstraintSet: def range_constraint( lower_bound: Any, typevar: Any, upper_bound: Any ) -> ConstraintSet: ... -def not_equivalent_constraint(typevar: Any, hole: Any) -> ConstraintSet: ... -def incomparable_constraint(typevar: Any, pivot: Any) -> ConstraintSet: ... +def negated_range_constraint( + lower_bound: Any, typevar: Any, upper_bound: Any +) -> ConstraintSet: ... # Predicates on types #