[ty] Move constraint set mdtest functions into ConstraintSet class (#21108)
Some checks are pending
CI / Determine changes (push) Waiting to run
CI / cargo fmt (push) Waiting to run
CI / cargo clippy (push) Blocked by required conditions
CI / cargo test (linux) (push) Blocked by required conditions
CI / cargo test (linux, release) (push) Blocked by required conditions
CI / cargo test (${{ github.repository == 'astral-sh/ruff' && 'depot-windows-2022-16' || 'windows-latest' }}) (push) Blocked by required conditions
CI / cargo test (macos-latest) (push) Blocked by required conditions
CI / cargo test (wasm) (push) Blocked by required conditions
CI / cargo build (msrv) (push) Blocked by required conditions
CI / cargo fuzz build (push) Blocked by required conditions
CI / cargo shear (push) Blocked by required conditions
CI / fuzz parser (push) Blocked by required conditions
CI / test scripts (push) Blocked by required conditions
CI / ecosystem (push) Blocked by required conditions
CI / Fuzz for new ty panics (push) Blocked by required conditions
CI / ty completion evaluation (push) Blocked by required conditions
CI / python package (push) Waiting to run
CI / pre-commit (push) Waiting to run
CI / mkdocs (push) Waiting to run
CI / formatter instabilities and black similarity (push) Blocked by required conditions
CI / test ruff-lsp (push) Blocked by required conditions
CI / check playground (push) Blocked by required conditions
CI / benchmarks instrumented (ruff) (push) Blocked by required conditions
CI / benchmarks instrumented (ty) (push) Blocked by required conditions
CI / benchmarks walltime (medium|multithreaded) (push) Blocked by required conditions
CI / benchmarks walltime (small|large) (push) Blocked by required conditions
[ty Playground] Release / publish (push) Waiting to run

We have several functions in `ty_extensions` for testing our constraint
set implementation. This PR refactors those functions so that they are
all methods of the `ConstraintSet` class, rather than being standalone
top-level functions. 🎩 to @sharkdp for pointing out that
`KnownBoundMethod` gives us what we need to implement that!
This commit is contained in:
Douglas Creager 2025-10-28 14:32:41 -04:00 committed by GitHub
parent 7b959ef44b
commit 4d2ee41e24
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 407 additions and 297 deletions

View file

@ -34,7 +34,7 @@ upper bound.
```py
from typing import Any, final, Never, Sequence
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -45,7 +45,7 @@ class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super))
reveal_type(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
@ -54,7 +54,7 @@ bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
reveal_type(range_constraint(Never, T, Base))
reveal_type(ConstraintSet.range(Never, T, Base))
```
Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
@ -63,7 +63,7 @@ no upper bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
reveal_type(range_constraint(Base, T, object))
reveal_type(ConstraintSet.range(Base, T, object))
```
And a range constraint with _both_ a lower bound of `Never` and an upper bound of `object` does not
@ -72,7 +72,7 @@ constrain the typevar at all.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(range_constraint(Never, T, object))
reveal_type(ConstraintSet.range(Never, T, object))
```
If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
@ -81,9 +81,9 @@ or incomparable, then there is no type that can satisfy the constraint.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Super, T, Sub))
reveal_type(ConstraintSet.range(Super, T, Sub))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Base, T, Unrelated))
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
@ -92,7 +92,7 @@ that specific type.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ = Base)]
reveal_type(range_constraint(Base, T, Base))
reveal_type(ConstraintSet.range(Base, T, Base))
```
Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
@ -101,14 +101,14 @@ their bottom and top materializations, respectively.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
reveal_type(range_constraint(Base, T, Any))
reveal_type(ConstraintSet.range(Base, T, Any))
# revealed: ty_extensions.ConstraintSet[(Sequence[Base] ≤ T@_ ≤ Sequence[object])]
reveal_type(range_constraint(Sequence[Base], T, Sequence[Any]))
reveal_type(ConstraintSet.range(Sequence[Base], T, Sequence[Any]))
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
reveal_type(range_constraint(Any, T, Base))
reveal_type(ConstraintSet.range(Any, T, Base))
# revealed: ty_extensions.ConstraintSet[(Sequence[Never] ≤ T@_ ≤ Sequence[Base])]
reveal_type(range_constraint(Sequence[Any], T, Sequence[Base]))
reveal_type(ConstraintSet.range(Sequence[Any], T, Sequence[Base]))
```
### Negated range
@ -119,7 +119,7 @@ strict subtype of the lower bound, a strict supertype of the upper bound, or inc
```py
from typing import Any, final, Never, Sequence
from ty_extensions import negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -130,7 +130,7 @@ class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(Sub, T, Super))
reveal_type(~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
@ -139,7 +139,7 @@ bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)]
reveal_type(negated_range_constraint(Never, T, Base))
reveal_type(~ConstraintSet.range(Never, T, Base))
```
Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
@ -148,7 +148,7 @@ no upper bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)]
reveal_type(negated_range_constraint(Base, T, object))
reveal_type(~ConstraintSet.range(Base, T, object))
```
And a negated range constraint with _both_ a lower bound of `Never` and an upper bound of `object`
@ -157,7 +157,7 @@ cannot be satisfied at all.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(negated_range_constraint(Never, T, object))
reveal_type(~ConstraintSet.range(Never, T, object))
```
If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
@ -166,9 +166,9 @@ 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))
reveal_type(~ConstraintSet.range(Super, T, Sub))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(negated_range_constraint(Base, T, Unrelated))
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
@ -177,7 +177,7 @@ type other than that specific type.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(negated_range_constraint(Base, T, Base))
reveal_type(~ConstraintSet.range(Base, T, Base))
```
Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
@ -186,14 +186,14 @@ their bottom and top materializations, respectively.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_)]
reveal_type(negated_range_constraint(Base, T, Any))
reveal_type(~ConstraintSet.range(Base, T, Any))
# revealed: ty_extensions.ConstraintSet[¬(Sequence[Base] ≤ T@_ ≤ Sequence[object])]
reveal_type(negated_range_constraint(Sequence[Base], T, Sequence[Any]))
reveal_type(~ConstraintSet.range(Sequence[Base], T, Sequence[Any]))
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)]
reveal_type(negated_range_constraint(Any, T, Base))
reveal_type(~ConstraintSet.range(Any, T, Base))
# revealed: ty_extensions.ConstraintSet[¬(Sequence[Never] ≤ T@_ ≤ Sequence[Base])]
reveal_type(negated_range_constraint(Sequence[Any], T, Sequence[Base]))
reveal_type(~ConstraintSet.range(Sequence[Any], T, Sequence[Base]))
```
## Intersection
@ -204,7 +204,7 @@ cases, we can simplify the result of an intersection.
### Different typevars
```py
from ty_extensions import range_constraint, negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -216,9 +216,9 @@ We cannot simplify the intersection of constraints that refer to different typev
```py
def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base))]
reveal_type(range_constraint(Sub, T, Base) & range_constraint(Sub, U, Base))
reveal_type(ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Sub, U, 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))
reveal_type(~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Sub, U, Base))
```
### Intersection of two ranges
@ -227,7 +227,7 @@ The intersection of two ranges is where the ranges "overlap".
```py
from typing import final
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -239,13 +239,13 @@ class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(SubSub, T, Base) & range_constraint(Sub, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Base) & ConstraintSet.range(Sub, T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(SubSub, T, Super) & range_constraint(Sub, T, Base))
reveal_type(ConstraintSet.range(SubSub, T, Super) & ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ = Base)]
reveal_type(range_constraint(Sub, T, Base) & range_constraint(Base, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super) & range_constraint(Sub, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Super) & ConstraintSet.range(Sub, T, Super))
```
If they don't overlap, the intersection is empty.
@ -253,9 +253,9 @@ If they don't overlap, the intersection is empty.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Base, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Unrelated, T, object))
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Unrelated, T, object))
```
### Intersection of a range and a negated range
@ -266,7 +266,7 @@ the intersection as removing the hole from the range constraint.
```py
from typing import final, Never
from ty_extensions import range_constraint, negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -282,9 +282,9 @@ If the negative range completely contains the positive range, then the intersect
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(SubSub, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(SubSub, T, Super))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(Sub, T, Base))
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
@ -293,11 +293,11 @@ anything; the intersection is the positive range.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) & negated_range_constraint(Never, T, Unrelated))
reveal_type(ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Never, T, Unrelated))
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub)]
reveal_type(range_constraint(SubSub, T, Sub) & negated_range_constraint(Base, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Base, T, Super) & negated_range_constraint(SubSub, T, Sub))
reveal_type(ConstraintSet.range(Base, T, Super) & ~ConstraintSet.range(SubSub, T, Sub))
```
Otherwise we clip the negative constraint to the mininum range that overlaps with the positive
@ -306,9 +306,9 @@ range.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ T@_ ≤ Base))]
reveal_type(range_constraint(SubSub, T, Base) & negated_range_constraint(Sub, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(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))
reveal_type(ConstraintSet.range(SubSub, T, Super) & ~ConstraintSet.range(Sub, T, Base))
```
### Intersection of two negated ranges
@ -318,7 +318,7 @@ smaller constraint. For negated ranges, the smaller constraint is the one with t
```py
from typing import final
from ty_extensions import negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -330,9 +330,9 @@ class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(SubSub, T, Super) & negated_range_constraint(Sub, T, Base))
reveal_type(~ConstraintSet.range(SubSub, T, Super) & ~ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(Sub, T, Super) & negated_range_constraint(Sub, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Super) & ~ConstraintSet.range(Sub, T, Super))
```
Otherwise, the union cannot be simplified.
@ -340,11 +340,11 @@ Otherwise, the union cannot be simplified.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))]
reveal_type(negated_range_constraint(Sub, T, Base) & negated_range_constraint(Base, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Base) & ~ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Sub))]
reveal_type(negated_range_constraint(SubSub, T, Sub) & negated_range_constraint(Base, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) & ~ConstraintSet.range(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))
reveal_type(~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
@ -361,7 +361,7 @@ that type _is_ in `SubSub ≤ T ≤ Super`, it is not correct to simplify the un
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Base))]
reveal_type(negated_range_constraint(SubSub, T, Base) & negated_range_constraint(Sub, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Base) & ~ConstraintSet.range(Sub, T, Super))
```
## Union
@ -372,7 +372,7 @@ can simplify the result of an union.
### Different typevars
```py
from ty_extensions import range_constraint, negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -384,9 +384,9 @@ We cannot simplify the union of constraints that refer to different typevars.
```py
def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) (Sub ≤ U@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) | range_constraint(Sub, U, Base))
reveal_type(ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Sub, U, 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))
reveal_type(~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Sub, U, Base))
```
### Union of two ranges
@ -396,7 +396,7 @@ bounds.
```py
from typing import final
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -408,9 +408,9 @@ class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base))
reveal_type(ConstraintSet.range(SubSub, T, Super) | ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super) | range_constraint(Sub, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Super) | ConstraintSet.range(Sub, T, Super))
```
Otherwise, the union cannot be simplified.
@ -418,11 +418,11 @@ Otherwise, the union cannot be simplified.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) (Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) | range_constraint(Base, T, Super))
reveal_type(ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) (SubSub ≤ T@_ ≤ Sub)]
reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) (Unrelated ≤ T@_)]
reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Unrelated, T, object))
reveal_type(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
@ -438,7 +438,7 @@ not include `Sub`. That means it should not be in the union. Since that type _is
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super) (SubSub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super))
reveal_type(ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super))
```
### Union of a range and a negated range
@ -449,7 +449,7 @@ the union as filling part of the hole with the types from the range constraint.
```py
from typing import final, Never
from ty_extensions import range_constraint, negated_range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -465,9 +465,9 @@ If the positive range completely contains the negative range, then the union is
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(negated_range_constraint(Sub, T, Base) | range_constraint(SubSub, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(SubSub, T, Super))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(negated_range_constraint(Sub, T, Base) | range_constraint(Sub, T, Base))
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;
@ -476,11 +476,11 @@ 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))
reveal_type(~ConstraintSet.range(Sub, T, Base) | ConstraintSet.range(Never, T, Unrelated))
# revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Sub)]
reveal_type(negated_range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[¬(Base ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(Base, T, Super) | range_constraint(SubSub, T, Sub))
reveal_type(~ConstraintSet.range(Base, T, Super) | ConstraintSet.range(SubSub, T, Sub))
```
Otherwise we clip the positive constraint to the mininum range that overlaps with the negative
@ -489,9 +489,9 @@ range.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ¬(SubSub ≤ T@_ ≤ Base)]
reveal_type(negated_range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ¬(SubSub ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base))
reveal_type(~ConstraintSet.range(SubSub, T, Super) | ConstraintSet.range(Sub, T, Base))
```
### Union of two negated ranges
@ -500,7 +500,7 @@ 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
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -512,13 +512,13 @@ 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))
reveal_type(~ConstraintSet.range(SubSub, T, Base) | ~ConstraintSet.range(Sub, T, Super))
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)]
reveal_type(negated_range_constraint(SubSub, T, Super) | negated_range_constraint(Sub, T, Base))
reveal_type(~ConstraintSet.range(SubSub, T, Super) | ~ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(negated_range_constraint(Sub, T, Base) | negated_range_constraint(Base, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Base) | ~ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Super)]
reveal_type(negated_range_constraint(Sub, T, Super) | negated_range_constraint(Sub, T, Super))
reveal_type(~ConstraintSet.range(Sub, T, Super) | ~ConstraintSet.range(Sub, T, Super))
```
If the holes don't overlap, the union is always satisfied.
@ -526,9 +526,9 @@ If the holes don't overlap, the union is always satisfied.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(negated_range_constraint(SubSub, T, Sub) | negated_range_constraint(Base, T, Super))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(negated_range_constraint(SubSub, T, Sub) | negated_range_constraint(Unrelated, T, object))
reveal_type(~ConstraintSet.range(SubSub, T, Sub) | ~ConstraintSet.range(Unrelated, T, object))
```
## Negation
@ -537,7 +537,7 @@ def _[T]() -> None:
```py
from typing import Never
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
class Super: ...
class Base(Super): ...
@ -545,20 +545,20 @@ class Sub(Base): ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base)]
reveal_type(~range_constraint(Sub, T, Base))
reveal_type(~ConstraintSet.range(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base)]
reveal_type(~range_constraint(Never, T, Base))
reveal_type(~ConstraintSet.range(Never, T, Base))
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_)]
reveal_type(~range_constraint(Sub, T, object))
reveal_type(~ConstraintSet.range(Sub, T, object))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(~range_constraint(Never, T, object))
reveal_type(~ConstraintSet.range(Never, T, object))
```
The union of a range constraint and its negation should always be satisfiable.
```py
def _[T]() -> None:
constraint = range_constraint(Sub, T, Base)
constraint = ConstraintSet.range(Sub, T, Base)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(constraint | ~constraint)
```
@ -567,7 +567,7 @@ def _[T]() -> None:
```py
from typing import final, Never
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
class Base: ...
@ -576,20 +576,20 @@ class Unrelated: ...
def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[¬(T@_ ≤ Base) ¬(U@_ ≤ Base)]
reveal_type(~(range_constraint(Never, T, Base) & range_constraint(Never, U, Base)))
reveal_type(~(ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base)))
```
The union of a constraint and its negation should always be satisfiable.
```py
def _[T, U]() -> None:
c1 = range_constraint(Never, T, Base) & range_constraint(Never, U, Base)
c1 = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Base)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(c1 | ~c1)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~c1 | c1)
c2 = range_constraint(Unrelated, T, object) & range_constraint(Unrelated, U, object)
c2 = ConstraintSet.range(Unrelated, T, object) & ConstraintSet.range(Unrelated, U, object)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(c2 | ~c2)
# revealed: ty_extensions.ConstraintSet[always]
@ -614,19 +614,19 @@ since we always hide `Never` lower bounds and `object` upper bounds.
```py
from typing import Never
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
def f[S, T]():
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
reveal_type(range_constraint(Never, S, T))
reveal_type(ConstraintSet.range(Never, S, T))
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
reveal_type(range_constraint(S, T, object))
reveal_type(ConstraintSet.range(S, T, object))
def f[T, S]():
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
reveal_type(range_constraint(Never, S, T))
reveal_type(ConstraintSet.range(Never, S, T))
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
reveal_type(range_constraint(S, T, object))
reveal_type(ConstraintSet.range(S, T, object))
```
Equivalence constraints are similar; internally we arbitrarily choose the "earlier" typevar to be
@ -635,15 +635,15 @@ the constraint, and the other the bound. But we display the result the same way
```py
def f[S, T]():
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)]
reveal_type(range_constraint(T, S, T))
reveal_type(ConstraintSet.range(T, S, T))
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)]
reveal_type(range_constraint(S, T, S))
reveal_type(ConstraintSet.range(S, T, S))
def f[T, S]():
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)]
reveal_type(range_constraint(T, S, T))
reveal_type(ConstraintSet.range(T, S, T))
# revealed: ty_extensions.ConstraintSet[(S@f = T@f)]
reveal_type(range_constraint(S, T, S))
reveal_type(ConstraintSet.range(S, T, S))
```
But in the case of `S ≤ T ≤ U`, we end up with an ambiguity. Depending on the typevar ordering, that
@ -654,7 +654,7 @@ def f[S, T, U]():
# Could be either of:
# ty_extensions.ConstraintSet[(S@f ≤ T@f ≤ U@f)]
# ty_extensions.ConstraintSet[(S@f ≤ T@f) ∧ (T@f ≤ U@f)]
# reveal_type(range_constraint(S, T, U))
# reveal_type(ConstraintSet.range(S, T, U))
...
```
@ -668,13 +668,13 @@ This section contains several examples that show that we simplify the DNF formul
before displaying it.
```py
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
def f[T, U]():
t1 = range_constraint(str, T, str)
t2 = range_constraint(bool, T, bool)
u1 = range_constraint(str, U, str)
u2 = range_constraint(bool, U, bool)
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)
@ -692,8 +692,8 @@ from typing import Never
from ty_extensions import static_assert
def f[T]():
t_int = range_constraint(Never, T, int)
t_bool = range_constraint(Never, T, bool)
t_int = ConstraintSet.range(Never, T, int)
t_bool = ConstraintSet.range(Never, T, bool)
# `T ≤ bool` implies `T ≤ int`: if a type satisfies the former, it must always satisfy the
# latter. We can turn that into a constraint set, using the equivalence `p → q == ¬p q`:
@ -707,7 +707,7 @@ def f[T]():
# "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 = range_constraint(Never, T, object)
always = ConstraintSet.range(Never, T, object)
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(always)
static_assert(always)
@ -721,11 +721,11 @@ intersections whose elements appear in different orders.
```py
from typing import Never
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
def f[T]():
# revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]
reveal_type(range_constraint(Never, T, str | int))
reveal_type(ConstraintSet.range(Never, T, str | int))
# revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]
reveal_type(range_constraint(Never, T, int | str))
reveal_type(ConstraintSet.range(Never, T, int | str))
```

View file

@ -5,7 +5,7 @@
python-version = "3.12"
```
This file tests the _constraint implication_ relationship between types, aka `is_subtype_of_given`,
This file tests the _constraint implication_ relationship between types, aka `implies_subtype_of`,
which tests whether one type is a [subtype][subtyping] of another _assuming that the constraints in
a particular constraint set hold_.
@ -16,14 +16,14 @@ fully static type that is not a typevar. It can _contain_ a typevar, though —
considered concrete.)
```py
from ty_extensions import is_subtype_of, is_subtype_of_given, static_assert
from ty_extensions import ConstraintSet, is_subtype_of, static_assert
def equivalent_to_other_relationships[T]():
static_assert(is_subtype_of(bool, int))
static_assert(is_subtype_of_given(True, bool, int))
static_assert(ConstraintSet.always().implies_subtype_of(bool, int))
static_assert(not is_subtype_of(bool, str))
static_assert(not is_subtype_of_given(True, bool, str))
static_assert(not ConstraintSet.always().implies_subtype_of(bool, str))
```
Moreover, for concrete types, the answer does not depend on which constraint set we are considering.
@ -32,16 +32,16 @@ there isn't a valid specialization for the typevars we are considering.
```py
from typing import Never
from ty_extensions import range_constraint
from ty_extensions import ConstraintSet
def even_given_constraints[T]():
constraints = range_constraint(Never, T, int)
static_assert(is_subtype_of_given(constraints, bool, int))
static_assert(not is_subtype_of_given(constraints, bool, str))
constraints = ConstraintSet.range(Never, T, int)
static_assert(constraints.implies_subtype_of(bool, int))
static_assert(not constraints.implies_subtype_of(bool, str))
def even_given_unsatisfiable_constraints():
static_assert(is_subtype_of_given(False, bool, int))
static_assert(not is_subtype_of_given(False, bool, str))
static_assert(ConstraintSet.never().implies_subtype_of(bool, int))
static_assert(not ConstraintSet.never().implies_subtype_of(bool, str))
```
## Type variables
@ -141,37 +141,37 @@ considering.
```py
from typing import Never
from ty_extensions import is_subtype_of_given, range_constraint, static_assert
from ty_extensions import ConstraintSet, static_assert
def given_constraints[T]():
static_assert(not is_subtype_of_given(True, T, int))
static_assert(not is_subtype_of_given(True, T, bool))
static_assert(not is_subtype_of_given(True, T, str))
static_assert(not ConstraintSet.always().implies_subtype_of(T, int))
static_assert(not ConstraintSet.always().implies_subtype_of(T, bool))
static_assert(not ConstraintSet.always().implies_subtype_of(T, str))
# These are vacuously true; false implies anything
static_assert(is_subtype_of_given(False, T, int))
static_assert(is_subtype_of_given(False, T, bool))
static_assert(is_subtype_of_given(False, T, str))
static_assert(ConstraintSet.never().implies_subtype_of(T, int))
static_assert(ConstraintSet.never().implies_subtype_of(T, bool))
static_assert(ConstraintSet.never().implies_subtype_of(T, str))
given_int = range_constraint(Never, T, int)
static_assert(is_subtype_of_given(given_int, T, int))
static_assert(not is_subtype_of_given(given_int, T, bool))
static_assert(not is_subtype_of_given(given_int, T, str))
given_int = ConstraintSet.range(Never, T, int)
static_assert(given_int.implies_subtype_of(T, int))
static_assert(not given_int.implies_subtype_of(T, bool))
static_assert(not given_int.implies_subtype_of(T, str))
given_bool = range_constraint(Never, T, bool)
static_assert(is_subtype_of_given(given_bool, T, int))
static_assert(is_subtype_of_given(given_bool, T, bool))
static_assert(not is_subtype_of_given(given_bool, T, str))
given_bool = ConstraintSet.range(Never, T, bool)
static_assert(given_bool.implies_subtype_of(T, int))
static_assert(given_bool.implies_subtype_of(T, bool))
static_assert(not given_bool.implies_subtype_of(T, str))
given_both = given_bool & given_int
static_assert(is_subtype_of_given(given_both, T, int))
static_assert(is_subtype_of_given(given_both, T, bool))
static_assert(not is_subtype_of_given(given_both, T, str))
static_assert(given_both.implies_subtype_of(T, int))
static_assert(given_both.implies_subtype_of(T, bool))
static_assert(not given_both.implies_subtype_of(T, str))
given_str = range_constraint(Never, T, str)
static_assert(not is_subtype_of_given(given_str, T, int))
static_assert(not is_subtype_of_given(given_str, T, bool))
static_assert(is_subtype_of_given(given_str, T, str))
given_str = ConstraintSet.range(Never, T, str)
static_assert(not given_str.implies_subtype_of(T, int))
static_assert(not given_str.implies_subtype_of(T, bool))
static_assert(given_str.implies_subtype_of(T, str))
```
This might require propagating constraints from other typevars.
@ -179,20 +179,20 @@ This might require propagating constraints from other typevars.
```py
def mutually_constrained[T, U]():
# If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well.
given_int = range_constraint(U, T, U) & range_constraint(Never, U, int)
given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no static-assert-error
# error: [static-assert-error]
static_assert(is_subtype_of_given(given_int, T, int))
static_assert(not is_subtype_of_given(given_int, T, bool))
static_assert(not is_subtype_of_given(given_int, T, str))
static_assert(given_int.implies_subtype_of(T, int))
static_assert(not given_int.implies_subtype_of(T, bool))
static_assert(not given_int.implies_subtype_of(T, str))
# If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well.
given_int = range_constraint(Never, T, U) & range_constraint(Never, U, int)
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no static-assert-error
# error: [static-assert-error]
static_assert(is_subtype_of_given(given_int, T, int))
static_assert(not is_subtype_of_given(given_int, T, bool))
static_assert(not is_subtype_of_given(given_int, T, str))
static_assert(given_int.implies_subtype_of(T, int))
static_assert(not given_int.implies_subtype_of(T, bool))
static_assert(not given_int.implies_subtype_of(T, str))
```
[subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence