Python
/
ruff
mirror of https://github.com/astral-sh/ruff
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[ty] Stop testing the (brittle) constraint set display implementation (#21743) 

The `Display` implementation for constraint sets is brittle, and
deserves a rethink. But later! It's perfectly fine for printf debugging;
we just shouldn't be writing mdtests that depend on any particular
rendering details. Most of these tests can be replaced with an
equivalence check that actually validates that the _behavior_ of two
constraint sets are identical.
This commit is contained in:
Douglas Creager 2025-12-02 03:17:29 -05:00 committed by GitHub
parent 2182c750db
commit cf4196466c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 355 additions and 371 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
View File

@ -321,9 +321,8 @@ from typing import Never
from ty_extensions import ConstraintSet, generic_context from ty_extensions import ConstraintSet, generic_context
def mentions[T, U](): def mentions[T, U]():
# (T@mentions ≤ int) ∧ (U@mentions = list[T@mentions])
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T]) constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T])
# revealed: ty_extensions.ConstraintSet[((T@mentions ≤ int) ∧ (U@mentions = list[T@mentions]))]
reveal_type(constraints)
# revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]] # revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
reveal_type(generic_context(mentions).specialize_constrained(constraints)) reveal_type(generic_context(mentions).specialize_constrained(constraints))
``` ```
@ -334,9 +333,8 @@ this case.
```py ```py
def divergent[T, U](): def divergent[T, U]():
# (T@divergent = list[U@divergent]) ∧ (U@divergent = list[T@divergent]))
constraints = ConstraintSet.range(list[U], T, list[U]) & ConstraintSet.range(list[T], U, list[T]) constraints = ConstraintSet.range(list[U], T, list[U]) & ConstraintSet.range(list[T], U, list[T])
# revealed: ty_extensions.ConstraintSet[((T@divergent = list[U@divergent]) ∧ (U@divergent = list[T@divergent]))]
reveal_type(constraints)
# revealed: None # revealed: None
reveal_type(generic_context(divergent).specialize_constrained(constraints)) reveal_type(generic_context(divergent).specialize_constrained(constraints))
``` ```

2
crates/ty_python_semantic/resources/mdtest/ty_extensions.md
View File

@ -398,7 +398,7 @@ the expression `str`:
from ty_extensions import TypeOf, is_subtype_of, static_assert from ty_extensions import TypeOf, is_subtype_of, static_assert
# This is incorrect and therefore fails with ... # This is incorrect and therefore fails with ...
# error: "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy" # error: "Static assertion error: argument of type `ty_extensions.ConstraintSet` is statically known to be falsy"
static_assert(is_subtype_of(str, type[str])) static_assert(is_subtype_of(str, type[str]))
# Correct, returns True: # Correct, returns True:

560
crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
View File

@ -34,7 +34,7 @@ upper bound.
```py ```py
from typing import Any, final, Never, Sequence from typing import Any, final, Never, Sequence
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -44,8 +44,8 @@ class Sub(Base): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)] # (Sub ≤ T@_ ≤ Super)
reveal_type(ConstraintSet.range(Sub, T, Super)) ConstraintSet.range(Sub, T, Super)
``` ```
Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower
@ -53,8 +53,8 @@ bound.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)] # (T@_ ≤ Base)
reveal_type(ConstraintSet.range(Never, T, Base)) ConstraintSet.range(Never, T, Base)
``` ```
Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
@ -62,8 +62,8 @@ no upper bound.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)] # (Base ≤ T@_)
reveal_type(ConstraintSet.range(Base, T, object)) ConstraintSet.range(Base, T, object)
``` ```
And a range constraint with a lower bound of `Never` and an upper bound of `object` allows the And a range constraint with a lower bound of `Never` and an upper bound of `object` allows the
@ -74,8 +74,8 @@ of `object`.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ = *)] # (T@_ = *)
reveal_type(ConstraintSet.range(Never, T, object)) ConstraintSet.range(Never, T, object)
``` ```
If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound) If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
@ -83,10 +83,8 @@ or incomparable, then there is no type that can satisfy the constraint.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never] static_assert(not ConstraintSet.range(Super, T, Sub))
reveal_type(ConstraintSet.range(Super, T, Sub)) static_assert(not ConstraintSet.range(Base, T, Unrelated))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(ConstraintSet.range(Base, T, Unrelated))
``` ```
The lower and upper bound can be the same type, in which case the typevar can only be specialized to The lower and upper bound can be the same type, in which case the typevar can only be specialized to
@ -94,8 +92,8 @@ that specific type.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ = Base)] # (T@_ = Base)
reveal_type(ConstraintSet.range(Base, T, Base)) ConstraintSet.range(Base, T, Base)
``` ```
Constraints can only refer to fully static types, so the lower and upper bounds are transformed into Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
@ -103,15 +101,21 @@ their bottom and top materializations, respectively.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)] constraints = ConstraintSet.range(Base, T, Any)
reveal_type(ConstraintSet.range(Base, T, Any)) expected = ConstraintSet.range(Base, T, object)
# revealed: ty_extensions.ConstraintSet[(Sequence[Base] ≤ T@_ ≤ Sequence[object])] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Sequence[Base], T, Sequence[Any]))
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)] constraints = ConstraintSet.range(Sequence[Base], T, Sequence[Any])
reveal_type(ConstraintSet.range(Any, T, Base)) expected = ConstraintSet.range(Sequence[Base], T, Sequence[object])
# revealed: ty_extensions.ConstraintSet[(Sequence[Never] ≤ T@_ ≤ Sequence[Base])] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Sequence[Any], T, Sequence[Base]))
constraints = ConstraintSet.range(Any, T, Base)
expected = ConstraintSet.range(Never, T, Base)
static_assert(constraints == expected)
constraints = ConstraintSet.range(Sequence[Any], T, Sequence[Base])
expected = ConstraintSet.range(Sequence[Never], T, Sequence[Base])
static_assert(constraints == expected)
``` ```
### Negated range ### Negated range
@ -122,7 +126,7 @@ strict subtype of the lower bound, a strict supertype of the upper bound, or inc
```py ```py
from typing import Any, final, Never, Sequence from typing import Any, final, Never, Sequence
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -132,8 +136,8 @@ class Sub(Base): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] # ¬(Sub ≤ T@_ ≤ Super)
reveal_type(~ConstraintSet.range(Sub, T, Super)) ~ConstraintSet.range(Sub, T, Super)
``` ```
Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower
@ -141,8 +145,8 @@ bound.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] # ¬(T@_ ≤ Base)
reveal_type(~ConstraintSet.range(Never, T, Base)) ~ConstraintSet.range(Never, T, Base)
``` ```
Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
@ -150,8 +154,8 @@ no upper bound.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)] # ¬(Base ≤ T@_)
reveal_type(~ConstraintSet.range(Base, T, object)) ~ConstraintSet.range(Base, T, object)
``` ```
And a negated range constraint with _both_ a lower bound of `Never` and an upper bound of `object` And a negated range constraint with _both_ a lower bound of `Never` and an upper bound of `object`
@ -159,8 +163,8 @@ cannot be satisfied at all.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ *)] # (T@_ ≠ *)
reveal_type(~ConstraintSet.range(Never, T, object)) ~ConstraintSet.range(Never, T, object)
``` ```
If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound) If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
@ -168,10 +172,8 @@ or incomparable, then the negated range constraint can always be satisfied.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always] static_assert(~ConstraintSet.range(Super, T, Sub))
reveal_type(~ConstraintSet.range(Super, T, Sub)) static_assert(~ConstraintSet.range(Base, T, Unrelated))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~ConstraintSet.range(Base, T, Unrelated))
``` ```
The lower and upper bound can be the same type, in which case the typevar can be specialized to any The lower and upper bound can be the same type, in which case the typevar can be specialized to any
@ -179,8 +181,8 @@ type other than that specific type.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] # (T@_ ≠ Base)
reveal_type(~ConstraintSet.range(Base, T, Base)) ~ConstraintSet.range(Base, T, Base)
``` ```
Constraints can only refer to fully static types, so the lower and upper bounds are transformed into Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
@ -188,15 +190,21 @@ their bottom and top materializations, respectively.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)] constraints = ~ConstraintSet.range(Base, T, Any)
reveal_type(~ConstraintSet.range(Base, T, Any)) expected = ~ConstraintSet.range(Base, T, object)
# revealed: ty_extensions.ConstraintSet[¬(Sequence[Base] ≤ T@_ ≤ Sequence[object])] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(Sequence[Base], T, Sequence[Any]))
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] constraints = ~ConstraintSet.range(Sequence[Base], T, Sequence[Any])
reveal_type(~ConstraintSet.range(Any, T, Base)) expected = ~ConstraintSet.range(Sequence[Base], T, Sequence[object])
# revealed: ty_extensions.ConstraintSet[¬(Sequence[Never] ≤ T@_ ≤ Sequence[Base])] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(Sequence[Any], T, Sequence[Base]))
constraints = ~ConstraintSet.range(Any, T, Base)
expected = ~ConstraintSet.range(Never, T, Base)
static_assert(constraints == expected)
constraints = ~ConstraintSet.range(Sequence[Any], T, Sequence[Base])
expected = ~ConstraintSet.range(Sequence[Never], T, Sequence[Base])
static_assert(constraints == expected)
``` ```
## Intersection ## Intersection
@ -218,10 +226,10 @@ We cannot simplify the intersection of constraints that refer to different typev
```py ```py
def _[T, U]() -> None: def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base))] # (Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base)
reveal_type(ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Sub, U, Base)) ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Sub, U, Base)
# revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ U@_ ≤ Base))] # ¬(Sub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ U@_ ≤ Base)
reveal_type(~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Sub, U, Base)) ~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Sub, U, Base)
``` ```
### Intersection of two ranges ### Intersection of two ranges
@ -230,7 +238,7 @@ The intersection of two ranges is where the ranges "overlap".
```py ```py
from typing import final from typing import final
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -241,24 +249,29 @@ class SubSub(Sub): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] constraints = ConstraintSet.range(SubSub, T, Base) & ConstraintSet.range(Sub, T, Super)
reveal_type(ConstraintSet.range(SubSub, T, Base) & ConstraintSet.range(Sub, T, Super)) expected = ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(SubSub, T, Super) & ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ = Base)] constraints = ConstraintSet.range(SubSub, T, Super) & ConstraintSet.range(Sub, T, Base)
reveal_type(ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Base, T, Super)) expected = ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Sub, T, Super) & ConstraintSet.range(Sub, T, Super))
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Base, T, Super)
expected = ConstraintSet.range(Base, T, Base)
static_assert(constraints == expected)
constraints = ConstraintSet.range(Sub, T, Super) & ConstraintSet.range(Sub, T, Super)
expected = ConstraintSet.range(Sub, T, Super)
static_assert(constraints == expected)
``` ```
If they don't overlap, the intersection is empty. If they don't overlap, the intersection is empty.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never] static_assert(not ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Base, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Base, T, Super)) static_assert(not ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Unrelated, T, object))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Unrelated, T, object))
``` ```
Expanding on this, when intersecting two upper bounds constraints (`(T ≤ Base) ∧ (T ≤ Other)`), we Expanding on this, when intersecting two upper bounds constraints (`(T ≤ Base) ∧ (T ≤ Other)`), we
@ -267,23 +280,17 @@ satisfy their intersection `T ≤ Base & Other`, and vice versa.
```py ```py
from typing import Never from typing import Never
from ty_extensions import Intersection, static_assert from ty_extensions import Intersection
# This is not final, so it's possible for a subclass to inherit from both Base and Other. # This is not final, so it's possible for a subclass to inherit from both Base and Other.
class Other: ... class Other: ...
def upper_bounds[T](): def upper_bounds[T]():
# (T@upper_bounds ≤ Base & Other)
intersection_type = ConstraintSet.range(Never, T, Intersection[Base, Other]) intersection_type = ConstraintSet.range(Never, T, Intersection[Base, Other])
# revealed: ty_extensions.ConstraintSet[(T@upper_bounds ≤ Base & Other)] # (T@upper_bounds ≤ Base) ∧ (T@upper_bounds ≤ Other)
reveal_type(intersection_type)
intersection_constraint = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, T, Other) intersection_constraint = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, T, Other)
# revealed: ty_extensions.ConstraintSet[(T@upper_bounds ≤ Base & Other)] static_assert(intersection_type == intersection_constraint)
reveal_type(intersection_constraint)
# The two constraint sets are equivalent; each satisfies the other.
static_assert(intersection_type.satisfies(intersection_constraint))
static_assert(intersection_constraint.satisfies(intersection_type))
``` ```
For an intersection of two lower bounds constraints (`(Base ≤ T) ∧ (Other ≤ T)`), we union the lower For an intersection of two lower bounds constraints (`(Base ≤ T) ∧ (Other ≤ T)`), we union the lower
@ -292,17 +299,11 @@ bounds. Any type that satisfies both `Base ≤ T` and `Other ≤ T` must necessa
```py ```py
def lower_bounds[T](): def lower_bounds[T]():
# (Base | Other ≤ T@lower_bounds)
union_type = ConstraintSet.range(Base | Other, T, object) union_type = ConstraintSet.range(Base | Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@lower_bounds)] # (Base ≤ T@upper_bounds) ∧ (Other ≤ T@upper_bounds)
reveal_type(union_type)
intersection_constraint = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Other, T, object) intersection_constraint = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@lower_bounds)] static_assert(union_type == intersection_constraint)
reveal_type(intersection_constraint)
# The two constraint sets are equivalent; each satisfies the other.
static_assert(union_type.satisfies(intersection_constraint))
static_assert(intersection_constraint.satisfies(union_type))
``` ```
### Intersection of a range and a negated range ### Intersection of a range and a negated range
@ -313,7 +314,7 @@ the intersection as removing the hole from the range constraint.
```py ```py
from typing import final, Never from typing import final, Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -328,10 +329,8 @@ If the negative range completely contains the positive range, then the intersect
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never] static_assert(not ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(SubSub, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(SubSub, T, Super)) static_assert(not ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Sub, T, Base))
``` ```
If the negative range is disjoint from the positive range, the negative range doesn't remove If the negative range is disjoint from the positive range, the negative range doesn't remove
@ -339,12 +338,17 @@ anything; the intersection is the positive range.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)] constraints = ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Never, T, Unrelated)
reveal_type(ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Never, T, Unrelated)) expected = ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)] constraints = ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Base, T, Super)
reveal_type(ConstraintSet.range(Base, T, Super) & ~ConstraintSet.range(SubSub, T, Sub)) expected = ConstraintSet.range(SubSub, T, Sub)
static_assert(constraints == expected)
constraints = ConstraintSet.range(Base, T, Super) & ~ConstraintSet.range(SubSub, T, Sub)
expected = ConstraintSet.range(Base, T, Super)
static_assert(constraints == expected)
``` ```
Otherwise we clip the negative constraint to the mininum range that overlaps with the positive Otherwise we clip the negative constraint to the mininum range that overlaps with the positive
@ -352,10 +356,9 @@ range.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ T@_ ≤ Base))] constraints = ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Super)
reveal_type(ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Super)) expected = ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(SubSub, T, Super) & ~ConstraintSet.range(Sub, T, Base))
``` ```
### Intersection of two negated ranges ### Intersection of two negated ranges
@ -365,7 +368,7 @@ smaller constraint. For negated ranges, the smaller constraint is the one with t
```py ```py
from typing import final from typing import final
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -376,22 +379,25 @@ class SubSub(Sub): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Super)] constraints = ~ConstraintSet.range(SubSub, T, Super) & ~ConstraintSet.range(Sub, T, Base)
reveal_type(~ConstraintSet.range(SubSub, T, Super) & ~ConstraintSet.range(Sub, T, Base)) expected = ~ConstraintSet.range(SubSub, T, Super)
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(Sub, T, Super) & ~ConstraintSet.range(Sub, T, Super))
constraints = ~ConstraintSet.range(Sub, T, Super) & ~ConstraintSet.range(Sub, T, Super)
expected = ~ConstraintSet.range(Sub, T, Super)
static_assert(constraints == expected)
``` ```
Otherwise, the intersection cannot be simplified. Otherwise, the intersection cannot be simplified.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))] # ¬(Base ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))
reveal_type(~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Base, T, Super)) ~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Base, T, Super)
# revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Sub))] # ¬(Base ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Sub))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Base, T, Super)) ~ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Base, T, Super)
# revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Unrelated ≤ T@_))] # ¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Unrelated ≤ T@_)
reveal_type(~ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Unrelated, T, object)) ~ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Unrelated, T, object)
``` ```
In particular, the following does not simplify, even though it seems like it could simplify to In particular, the following does not simplify, even though it seems like it could simplify to
@ -408,8 +414,8 @@ way.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Base))] # (¬(Sub ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Base))
reveal_type(~ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Super)) ~ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Super)
``` ```
## Union ## Union
@ -431,10 +437,10 @@ We cannot simplify the union of constraints that refer to different typevars.
```py ```py
def _[T, U]() -> None: def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Sub ≤ U@_ ≤ Base)] # (Sub ≤ T@_ ≤ Base) ∨ (Sub ≤ U@_ ≤ Base)
reveal_type(ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Sub, U, Base)) ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Sub, U, Base)
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base) ∨ ¬(Sub ≤ U@_ ≤ Base)] # ¬(Sub ≤ T@_ ≤ Base) ∨ ¬(Sub ≤ U@_ ≤ Base)
reveal_type(~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Sub, U, Base)) ~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Sub, U, Base)
``` ```
### Union of two ranges ### Union of two ranges
@ -444,7 +450,7 @@ bounds.
```py ```py
from typing import final from typing import final
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -455,22 +461,25 @@ class SubSub(Sub): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Super)] constraints = ConstraintSet.range(SubSub, T, Super) | ConstraintSet.range(Sub, T, Base)
reveal_type(ConstraintSet.range(SubSub, T, Super) | ConstraintSet.range(Sub, T, Base)) expected = ConstraintSet.range(SubSub, T, Super)
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Sub, T, Super) | ConstraintSet.range(Sub, T, Super))
constraints = ConstraintSet.range(Sub, T, Super) | ConstraintSet.range(Sub, T, Super)
expected = ConstraintSet.range(Sub, T, Super)
static_assert(constraints == expected)
``` ```
Otherwise, the union cannot be simplified. Otherwise, the union cannot be simplified.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (Sub ≤ T@_ ≤ Base)] # (Base ≤ T@_ ≤ Super) ∨ (Sub ≤ T@_ ≤ Base)
reveal_type(ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Base, T, Super)) ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Base, T, Super)
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (SubSub ≤ T@_ ≤ Sub)] # (Base ≤ T@_ ≤ Super) ∨ (SubSub ≤ T@_ ≤ Sub)
reveal_type(ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super)) ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super)
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) ∨ (Unrelated ≤ T@_)] # (SubSub ≤ T@_ ≤ Sub) ∨ (Unrelated ≤ T@_)
reveal_type(ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Unrelated, T, object)) ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Unrelated, T, object)
``` ```
In particular, the following does not simplify, even though it seems like it could simplify to In particular, the following does not simplify, even though it seems like it could simplify to
@ -485,8 +494,8 @@ not include `Sub`. That means it should not be in the union. Since that type _is
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super) ∨ (SubSub ≤ T@_ ≤ Base)] # (Sub ≤ T@_ ≤ Super) ∨ (SubSub ≤ T@_ ≤ Base)
reveal_type(ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super)) ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super)
``` ```
The union of two upper bound constraints (`(T ≤ Base) ∨ (T ≤ Other)`) is different than the single The union of two upper bound constraints (`(T ≤ Base) ∨ (T ≤ Other)`) is different than the single
@ -496,24 +505,18 @@ that satisfies the union constraint satisfies the union type.
```py ```py
from typing import Never from typing import Never
from ty_extensions import static_assert
# This is not final, so it's possible for a subclass to inherit from both Base and Other. # This is not final, so it's possible for a subclass to inherit from both Base and Other.
class Other: ... class Other: ...
def union[T](): def union[T]():
# (T@union ≤ Base | Other)
union_type = ConstraintSet.range(Never, T, Base | Other) union_type = ConstraintSet.range(Never, T, Base | Other)
# revealed: ty_extensions.ConstraintSet[(T@union ≤ Base | Other)] # (T@union ≤ Base) ∨ (T@union ≤ Other)
reveal_type(union_type)
union_constraint = ConstraintSet.range(Never, T, Base) | ConstraintSet.range(Never, T, Other) union_constraint = ConstraintSet.range(Never, T, Base) | ConstraintSet.range(Never, T, Other)
# revealed: ty_extensions.ConstraintSet[(T@union ≤ Base) ∨ (T@union ≤ Other)]
reveal_type(union_constraint)
# (T = Base | Other) satisfies (T ≤ Base | Other) but not (T ≤ Base ∨ T ≤ Other) # (T = Base | Other) satisfies (T ≤ Base | Other) but not (T ≤ Base ∨ T ≤ Other)
specialization = ConstraintSet.range(Base | Other, T, Base | Other) specialization = ConstraintSet.range(Base | Other, T, Base | Other)
# revealed: ty_extensions.ConstraintSet[(T@union = Base | Other)]
reveal_type(specialization)
static_assert(specialization.satisfies(union_type)) static_assert(specialization.satisfies(union_type))
static_assert(not specialization.satisfies(union_constraint)) static_assert(not specialization.satisfies(union_constraint))
@ -528,18 +531,13 @@ satisfies the union constraint (`(Base ≤ T) ∨ (Other ≤ T)`) but not the un
```py ```py
def union[T](): def union[T]():
# (Base | Other ≤ T@union)
union_type = ConstraintSet.range(Base | Other, T, object) union_type = ConstraintSet.range(Base | Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@union)] # (Base ≤ T@union) ∨ (Other ≤ T@union)
reveal_type(union_type)
union_constraint = ConstraintSet.range(Base, T, object) | ConstraintSet.range(Other, T, object) union_constraint = ConstraintSet.range(Base, T, object) | ConstraintSet.range(Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@union) ∨ (Other ≤ T@union)]
reveal_type(union_constraint)
# (T = Base) satisfies (Base ≤ T ∨ Other ≤ T) but not (Base | Other ≤ T) # (T = Base) satisfies (Base ≤ T ∨ Other ≤ T) but not (Base | Other ≤ T)
specialization = ConstraintSet.range(Base, T, Base) specialization = ConstraintSet.range(Base, T, Base)
# revealed: ty_extensions.ConstraintSet[(T@union = Base)]
reveal_type(specialization)
static_assert(not specialization.satisfies(union_type)) static_assert(not specialization.satisfies(union_type))
static_assert(specialization.satisfies(union_constraint)) static_assert(specialization.satisfies(union_constraint))
@ -556,7 +554,7 @@ the union as filling part of the hole with the types from the range constraint.
```py ```py
from typing import final, Never from typing import final, Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -571,10 +569,8 @@ If the positive range completely contains the negative range, then the union is
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always] static_assert(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(SubSub, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(SubSub, T, Super)) static_assert(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Sub, T, Base))
``` ```
If the negative range is disjoint from the positive range, the positive range doesn't add anything; If the negative range is disjoint from the positive range, the positive range doesn't add anything;
@ -582,12 +578,17 @@ the union is the negative range.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] constraints = ~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Never, T, Unrelated)
reveal_type(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Never, T, Unrelated)) expected = ~ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Sub)] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_ ≤ Super)] constraints = ~ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super)
reveal_type(~ConstraintSet.range(Base, T, Super) | ConstraintSet.range(SubSub, T, Sub)) expected = ~ConstraintSet.range(SubSub, T, Sub)
static_assert(constraints == expected)
constraints = ~ConstraintSet.range(Base, T, Super) | ConstraintSet.range(SubSub, T, Sub)
expected = ~ConstraintSet.range(Base, T, Super)
static_assert(constraints == expected)
``` ```
Otherwise we clip the positive constraint to the mininum range that overlaps with the negative Otherwise we clip the positive constraint to the mininum range that overlaps with the negative
@ -595,10 +596,9 @@ range.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ ¬(SubSub ≤ T@_ ≤ Base)] constraints = ~ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super)
reveal_type(~ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super)) expected = ~ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ ¬(SubSub ≤ T@_ ≤ Super)] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(SubSub, T, Super) | ConstraintSet.range(Sub, T, Base))
``` ```
### Union of two negated ranges ### Union of two negated ranges
@ -607,7 +607,7 @@ The union of two negated ranges has a hole where the ranges "overlap".
```py ```py
from typing import final from typing import final
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
@ -618,24 +618,29 @@ class SubSub(Sub): ...
class Unrelated: ... class Unrelated: ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] constraints = ~ConstraintSet.range(SubSub, T, Base) | ~ConstraintSet.range(Sub, T, Super)
reveal_type(~ConstraintSet.range(SubSub, T, Base) | ~ConstraintSet.range(Sub, T, Super)) expected = ~ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(SubSub, T, Super) | ~ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)] constraints = ~ConstraintSet.range(SubSub, T, Super) | ~ConstraintSet.range(Sub, T, Base)
reveal_type(~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Base, T, Super)) expected = ~ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)] static_assert(constraints == expected)
reveal_type(~ConstraintSet.range(Sub, T, Super) | ~ConstraintSet.range(Sub, T, Super))
constraints = ~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Base, T, Super)
expected = ~ConstraintSet.range(Base, T, Base)
static_assert(constraints == expected)
constraints = ~ConstraintSet.range(Sub, T, Super) | ~ConstraintSet.range(Sub, T, Super)
expected = ~ConstraintSet.range(Sub, T, Super)
static_assert(constraints == expected)
``` ```
If the holes don't overlap, the union is always satisfied. If the holes don't overlap, the union is always satisfied.
```py ```py
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always] static_assert(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Base, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Base, T, Super)) static_assert(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Unrelated, T, object))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Unrelated, T, object))
``` ```
## Negation ## Negation
@ -644,21 +649,21 @@ def _[T]() -> None:
```py ```py
from typing import Never from typing import Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Super: ... class Super: ...
class Base(Super): ... class Base(Super): ...
class Sub(Base): ... class Sub(Base): ...
def _[T]() -> None: def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)] # ¬(Sub ≤ T@_ ≤ Base)
reveal_type(~ConstraintSet.range(Sub, T, Base)) ~ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)] # ¬(T@_ ≤ Base)
reveal_type(~ConstraintSet.range(Never, T, Base)) ~ConstraintSet.range(Never, T, Base)
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_)] # ¬(Sub ≤ T@_)
reveal_type(~ConstraintSet.range(Sub, T, object)) ~ConstraintSet.range(Sub, T, object)
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ *)] # (T@_ ≠ *)
reveal_type(~ConstraintSet.range(Never, T, object)) ~ConstraintSet.range(Never, T, object)
``` ```
The union of a range constraint and its negation should always be satisfiable. The union of a range constraint and its negation should always be satisfiable.
@ -666,15 +671,14 @@ The union of a range constraint and its negation should always be satisfiable.
```py ```py
def _[T]() -> None: def _[T]() -> None:
constraint = ConstraintSet.range(Sub, T, Base) constraint = ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[always] static_assert(constraint | ~constraint)
reveal_type(constraint | ~constraint)
``` ```
### Negation of constraints involving two variables ### Negation of constraints involving two variables
```py ```py
from typing import final, Never from typing import final, Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
class Base: ... class Base: ...
@ -682,8 +686,8 @@ class Base: ...
class Unrelated: ... class Unrelated: ...
def _[T, U]() -> None: def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base) ∨ ¬(U@_ ≤ Base)] # ¬(T@_ ≤ Base) ∨ ¬(U@_ ≤ Base)
reveal_type(~(ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base))) ~(ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base))
``` ```
The union of a constraint and its negation should always be satisfiable. The union of a constraint and its negation should always be satisfiable.
@ -691,150 +695,91 @@ The union of a constraint and its negation should always be satisfiable.
```py ```py
def _[T, U]() -> None: def _[T, U]() -> None:
c1 = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base) c1 = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base)
# revealed: ty_extensions.ConstraintSet[always] static_assert(c1 | ~c1)
reveal_type(c1 | ~c1) static_assert(~c1 | c1)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~c1 | c1)
c2 = ConstraintSet.range(Unrelated, T, object) & ConstraintSet.range(Unrelated, U, object) c2 = ConstraintSet.range(Unrelated, T, object) & ConstraintSet.range(Unrelated, U, object)
# revealed: ty_extensions.ConstraintSet[always] static_assert(c2 | ~c2)
reveal_type(c2 | ~c2) static_assert(~c2 | c2)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~c2 | c2)
union = c1 | c2 union = c1 | c2
# revealed: ty_extensions.ConstraintSet[always] static_assert(union | ~union)
reveal_type(union | ~union) static_assert(~union | union)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~union | union)
``` ```
## Typevar ordering ## Typevar ordering
Constraints can relate two typevars — i.e., `S ≤ T`. We could encode that in one of two ways: Constraints can relate two typevars — i.e., `S ≤ T`. We could encode that in one of two ways:
`Never ≤ S ≤ T` or `S ≤ T ≤ object`. In other words, we can decide whether `S` or `T` is the typevar `Never ≤ S ≤ T` or `S ≤ T ≤ object`. In other words, we can decide whether `S` or `T` is the typevar
being constrained. The other is then the lower or upper bound of the constraint. being constrained. The other is then the lower or upper bound of the constraint. To handle this, we
enforce an arbitrary ordering on typevars, and always place the constraint on the "earlier" typevar.
To handle this, we enforce an arbitrary ordering on typevars, and always place the constraint on the
"earlier" typevar. For the example above, that does not change how the constraint is displayed,
since we always hide `Never` lower bounds and `object` upper bounds.
```py ```py
from typing import Never from typing import Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
def f[S, T](): def f[S, T]():
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] # (S@f ≤ T@f)
reveal_type(ConstraintSet.range(Never, S, T)) c1 = ConstraintSet.range(Never, S, T)
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] c2 = ConstraintSet.range(S, T, object)
reveal_type(ConstraintSet.range(S, T, object)) static_assert(c1 == c2)
def f[T, S](): def f[T, S]():
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] # (S@f ≤ T@f)
reveal_type(ConstraintSet.range(Never, S, T)) c1 = ConstraintSet.range(Never, S, T)
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] c2 = ConstraintSet.range(S, T, object)
reveal_type(ConstraintSet.range(S, T, object)) static_assert(c1 == c2)
``` ```
Equivalence constraints are similar; internally we arbitrarily choose the "earlier" typevar to be Equivalence constraints are similar; internally we arbitrarily choose the "earlier" typevar to be
the constraint, and the other the bound. But we display the result the same way no matter what. the constraint, and the other the bound.
```py ```py
def f[S, T](): def f[S, T]():
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)] # (S@f = T@f)
reveal_type(ConstraintSet.range(T, S, T)) c1 = ConstraintSet.range(T, S, T)
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)] c2 = ConstraintSet.range(S, T, S)
reveal_type(ConstraintSet.range(S, T, S)) static_assert(c1 == c2)
def f[T, S](): def f[T, S]():
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)] # (S@f = T@f)
reveal_type(ConstraintSet.range(T, S, T)) c1 = ConstraintSet.range(T, S, T)
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)] c2 = ConstraintSet.range(S, T, S)
reveal_type(ConstraintSet.range(S, T, S)) static_assert(c1 == c2)
``` ```
But in the case of `S ≤ T ≤ U`, we end up with an ambiguity. Depending on the typevar ordering, that But in the case of `S ≤ T ≤ U`, we end up with an ambiguity. Depending on the typevar ordering, that
might display as `S ≤ T ≤ U`, or as `(S ≤ T) ∧ (T ≤ U)`. might represented internally as `S ≤ T ≤ U`, or as `(S ≤ T) ∧ (T ≤ U)`. However, this should not
affect any uses of the constraint set.
```py ```py
def f[S, T, U](): def f[S, T, U]():
# Could be either of: # Could be either of:
# ty_extensions.ConstraintSet[(S@f ≤ T@f ≤ U@f)] # (S@f ≤ T@f ≤ U@f)
# ty_extensions.ConstraintSet[(S@f ≤ T@f) ∧ (T@f ≤ U@f)] # (S@f ≤ T@f) ∧ (T@f ≤ U@f)
# reveal_type(ConstraintSet.range(S, T, U)) ConstraintSet.range(S, T, U)
... ...
``` ```
## Other simplifications ## Other simplifications
### Displaying constraint sets ### Ordering of intersection and union elements
When displaying a constraint set, we transform the internal BDD representation into a DNF formula The ordering of elements in a union or intersection do not affect what types satisfy a constraint
(i.e., the logical OR of several clauses, each of which is the logical AND of several constraints). set.
This section contains several examples that show that we simplify the DNF formula as much as we can
before displaying it.
```py
from ty_extensions import ConstraintSet
def f[T, U]():
t1 = ConstraintSet.range(str, T, str)
t2 = ConstraintSet.range(bool, T, bool)
u1 = ConstraintSet.range(str, U, str)
u2 = ConstraintSet.range(bool, U, bool)
# revealed: ty_extensions.ConstraintSet[(T@f = bool) ∨ (T@f = str)]
reveal_type(t1 | t2)
# revealed: ty_extensions.ConstraintSet[(U@f = bool) ∨ (U@f = str)]
reveal_type(u1 | u2)
# revealed: ty_extensions.ConstraintSet[((T@f = bool) ∧ (U@f = bool)) ∨ ((T@f = bool) ∧ (U@f = str)) ∨ ((T@f = str) ∧ (U@f = bool)) ∨ ((T@f = str) ∧ (U@f = str))]
reveal_type((t1 | t2) & (u1 | u2))
```
We might simplify a BDD so much that we can no longer see the constraints that we used to construct
it!
```py ```py
from typing import Never from typing import Never
from ty_extensions import static_assert from ty_extensions import ConstraintSet, Intersection, static_assert
def f[T](): def f[T]():
t_int = ConstraintSet.range(Never, T, int) c1 = ConstraintSet.range(Never, T, str | int)
t_bool = ConstraintSet.range(Never, T, bool) c2 = ConstraintSet.range(Never, T, int | str)
static_assert(c1 == c2)
# `T ≤ bool` implies `T ≤ int`: if a type satisfies the former, it must always satisfy the c1 = ConstraintSet.range(Never, T, Intersection[str, int])
# latter. We can turn that into a constraint set, using the equivalence `p → q == ¬p ∨ q`: c2 = ConstraintSet.range(Never, T, Intersection[int, str])
implication = ~t_bool | t_int static_assert(c1 == c2)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(implication)
static_assert(implication)
# However, because of that implication, some inputs aren't valid: it's not possible for
# `T ≤ bool` to be true and `T ≤ int` to be false. This is reflected in the constraint set's
# "domain", which maps valid inputs to `true` and invalid inputs to `false`. This means that two
# constraint sets that are both always satisfied will not be identical if they have different
# domains!
always = ConstraintSet.always()
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(always)
static_assert(always)
static_assert(implication != always)
```
### Normalized bounds
The lower and upper bounds of a constraint are normalized, so that we equate unions and
intersections whose elements appear in different orders.
```py
from typing import Never
from ty_extensions import ConstraintSet
def f[T]():
# revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]
reveal_type(ConstraintSet.range(Never, T, str | int))
# revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]
reveal_type(ConstraintSet.range(Never, T, int | str))
``` ```
### Constraints on the same typevar ### Constraints on the same typevar
@ -846,15 +791,20 @@ static types.)
```py ```py
from typing import Never from typing import Never
from ty_extensions import ConstraintSet from ty_extensions import ConstraintSet, static_assert
def same_typevar[T](): def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] constraints = ConstraintSet.range(Never, T, T)
reveal_type(ConstraintSet.range(Never, T, T)) expected = ConstraintSet.range(Never, T, object)
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(T, T, object))
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] constraints = ConstraintSet.range(T, T, object)
reveal_type(ConstraintSet.range(T, T, T)) expected = ConstraintSet.range(Never, T, object)
static_assert(constraints == expected)
constraints = ConstraintSet.range(T, T, T)
expected = ConstraintSet.range(Never, T, object)
static_assert(constraints == expected)
``` ```
This is also true when the typevar appears in a union in the upper bound, or in an intersection in This is also true when the typevar appears in a union in the upper bound, or in an intersection in
@ -865,12 +815,17 @@ as shown above.)
from ty_extensions import Intersection from ty_extensions import Intersection
def same_typevar[T](): def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] constraints = ConstraintSet.range(Never, T, T | None)
reveal_type(ConstraintSet.range(Never, T, T | None)) expected = ConstraintSet.range(Never, T, object)
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Intersection[T, None], T, object))
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)] constraints = ConstraintSet.range(Intersection[T, None], T, object)
reveal_type(ConstraintSet.range(Intersection[T, None], T, T | None)) expected = ConstraintSet.range(Never, T, object)
static_assert(constraints == expected)
constraints = ConstraintSet.range(Intersection[T, None], T, T | None)
expected = ConstraintSet.range(Never, T, object)
static_assert(constraints == expected)
``` ```
Similarly, if the lower bound is an intersection containing the _negation_ of the typevar, then the Similarly, if the lower bound is an intersection containing the _negation_ of the typevar, then the
@ -880,8 +835,11 @@ constraint set can never be satisfied, since every type is disjoint with its neg
from ty_extensions import Not from ty_extensions import Not
def same_typevar[T](): def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[(T@same_typevar ≠ *)] constraints = ConstraintSet.range(Intersection[Not[T], None], T, object)
reveal_type(ConstraintSet.range(Intersection[Not[T], None], T, object)) expected = ~ConstraintSet.range(Never, T, object)
# revealed: ty_extensions.ConstraintSet[(T@same_typevar ≠ *)] static_assert(constraints == expected)
reveal_type(ConstraintSet.range(Not[T], T, object))
constraints = ConstraintSet.range(Not[T], T, object)
expected = ~ConstraintSet.range(Never, T, object)
static_assert(constraints == expected)
``` ```

130
crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
View File

@ -50,27 +50,37 @@ question when considering a typevar, by translating the desired relationship int
```py ```py
from typing import Any from typing import Any
from ty_extensions import is_assignable_to, is_subtype_of from ty_extensions import ConstraintSet, is_assignable_to, is_subtype_of, static_assert
def assignability[T](): def assignability[T]():
# TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ bool] constraints = is_assignable_to(T, bool)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Never, T, bool)
reveal_type(is_assignable_to(T, bool)) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ int] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, int)) constraints = is_assignable_to(T, int)
# revealed: ty_extensions.ConstraintSet[always] # TODO: expected = ConstraintSet.range(Never, T, int)
reveal_type(is_assignable_to(T, object)) expected = ConstraintSet.never()
static_assert(constraints == expected)
constraints = is_assignable_to(T, object)
expected = ConstraintSet.always()
static_assert(constraints == expected)
def subtyping[T](): def subtyping[T]():
# TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ bool] constraints = is_subtype_of(T, bool)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Never, T, bool)
reveal_type(is_subtype_of(T, bool)) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ int] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, int)) constraints = is_subtype_of(T, int)
# revealed: ty_extensions.ConstraintSet[always] # TODO: expected = ConstraintSet.range(Never, T, int)
reveal_type(is_subtype_of(T, object)) expected = ConstraintSet.never()
static_assert(constraints == expected)
constraints = is_subtype_of(T, object)
expected = ConstraintSet.always()
static_assert(constraints == expected)
``` ```
When checking assignability with a dynamic type, we use the bottom and top materializations of the When checking assignability with a dynamic type, we use the bottom and top materializations of the
@ -88,50 +98,64 @@ class Contravariant[T]:
pass pass
def assignability[T](): def assignability[T]():
# aka [T@assignability ≤ object], which is always satisfiable constraints = is_assignable_to(T, Any)
# revealed: ty_extensions.ConstraintSet[always] expected = ConstraintSet.range(Never, T, object)
reveal_type(is_assignable_to(T, Any)) static_assert(constraints == expected)
# aka [Never ≤ T@assignability], which is always satisfiable constraints = is_assignable_to(Any, T)
# revealed: ty_extensions.ConstraintSet[always] expected = ConstraintSet.range(Never, T, object)
reveal_type(is_assignable_to(Any, T)) static_assert(constraints == expected)
# TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Covariant[object]] constraints = is_assignable_to(T, Covariant[Any])
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Never, T, Covariant[object])
reveal_type(is_assignable_to(T, Covariant[Any])) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[Covariant[Never] ≤ T@assignability] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Covariant[Any], T))
# TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Contravariant[Never]] constraints = is_assignable_to(Covariant[Any], T)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Covariant[Never], T, object)
reveal_type(is_assignable_to(T, Contravariant[Any])) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[Contravariant[object] ≤ T@assignability] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Contravariant[Any], T)) constraints = is_assignable_to(T, Contravariant[Any])
# TODO: expected = ConstraintSet.range(Never, T, Contravariant[Never])
expected = ConstraintSet.never()
static_assert(constraints == expected)
constraints = is_assignable_to(Contravariant[Any], T)
# TODO: expected = ConstraintSet.range(Contravariant[object], T, object)
expected = ConstraintSet.never()
static_assert(constraints == expected)
def subtyping[T](): def subtyping[T]():
# aka [T@assignability ≤ object], which is always satisfiable constraints = is_subtype_of(T, Any)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Never, T, Never)
reveal_type(is_subtype_of(T, Any)) expected = ConstraintSet.never()
static_assert(constraints == expected)
# aka [Never ≤ T@assignability], which is always satisfiable constraints = is_subtype_of(Any, T)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(object, T, object)
reveal_type(is_subtype_of(Any, T)) expected = ConstraintSet.never()
static_assert(constraints == expected)
# TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Covariant[Never]] constraints = is_subtype_of(T, Covariant[Any])
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Never, T, Covariant[Never])
reveal_type(is_subtype_of(T, Covariant[Any])) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[Covariant[object] ≤ T@subtyping] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Covariant[Any], T))
# TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Contravariant[object]] constraints = is_subtype_of(Covariant[Any], T)
# revealed: ty_extensions.ConstraintSet[never] # TODO: expected = ConstraintSet.range(Covariant[object], T, object)
reveal_type(is_subtype_of(T, Contravariant[Any])) expected = ConstraintSet.never()
# TODO: revealed: ty_extensions.ConstraintSet[Contravariant[Never] ≤ T@subtyping] static_assert(constraints == expected)
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Contravariant[Any], T)) constraints = is_subtype_of(T, Contravariant[Any])
# TODO: expected = ConstraintSet.range(Never, T, Contravariant[object])
expected = ConstraintSet.never()
static_assert(constraints == expected)
constraints = is_subtype_of(Contravariant[Any], T)
# TODO: expected = ConstraintSet.range(Contravariant[Never], T, object)
expected = ConstraintSet.never()
static_assert(constraints == expected)
``` ```
At some point, though, we need to resolve a constraint set; at that point, we can no longer punt on At some point, though, we need to resolve a constraint set; at that point, we can no longer punt on

1
crates/ty_python_semantic/src/types/constraints.rs
View File

@ -418,6 +418,7 @@ impl<'db> ConstraintSet<'db> {
Self::constrain_typevar(db, typevar, lower, upper, TypeRelation::Assignability) Self::constrain_typevar(db, typevar, lower, upper, TypeRelation::Assignability)
} }
#[expect(dead_code)] // Keep this around for debugging purposes
pub(crate) fn display(self, db: &'db dyn Db) -> impl Display { pub(crate) fn display(self, db: &'db dyn Db) -> impl Display {
self.node.simplify_for_display(db).display(db) self.node.simplify_for_display(db).display(db)
} }

6
crates/ty_python_semantic/src/types/display.rs
View File

@ -2213,10 +2213,8 @@ impl<'db> FmtDetailed<'db> for DisplayKnownInstanceRepr<'db> {
} }
Ok(()) Ok(())
} }
KnownInstanceType::ConstraintSet(tracked_set) => { KnownInstanceType::ConstraintSet(_) => {
let constraints = tracked_set.constraints(self.db); f.with_type(ty).write_str("ty_extensions.ConstraintSet")
f.with_type(ty).write_str("ty_extensions.ConstraintSet")?;
write!(f, "[{}]", constraints.display(self.db))
} }
KnownInstanceType::GenericContext(generic_context) => { KnownInstanceType::GenericContext(generic_context) => {
f.with_type(ty).write_str("ty_extensions.GenericContext")?; f.with_type(ty).write_str("ty_extensions.GenericContext")?;

21
crates/ty_python_semantic/src/types/infer/builder.rs
View File

@ -10573,14 +10573,19 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
( (
Type::KnownInstance(KnownInstanceType::ConstraintSet(left)), Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
Type::KnownInstance(KnownInstanceType::ConstraintSet(right)), Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
) => match op { ) => {
ast::CmpOp::Eq => Some(Ok(Type::BooleanLiteral( let result = match op {
left.constraints(self.db()) == right.constraints(self.db()) ast::CmpOp::Eq => Some(
))), left.constraints(self.db()).iff(self.db(), right.constraints(self.db()))
ast::CmpOp::NotEq => Some(Ok(Type::BooleanLiteral( ),
left.constraints(self.db()) != right.constraints(self.db()) ast::CmpOp::NotEq => Some(
))), left.constraints(self.db()).iff(self.db(), right.constraints(self.db())).negate(self.db())
_ => None, ),
_ => None,
};
result.map(|constraints| Ok(Type::KnownInstance(KnownInstanceType::ConstraintSet(
TrackedConstraintSet::new(self.db(), constraints)
))))
} }
( (