[ty] Add mdtests that exercise constraint sets (#20319)

This PR adds a new `ty_extensions.ConstraintSet` class, which is used to
expose constraint sets to our mdtest framework. This lets us write a
large collection of unit tests that exercise the invariants and rewrite
rules of our constraint set implementation.

As part of this, `is_assignable_to` and friends are updated to return a
`ConstraintSet` instead of a `bool`, and we implement
`ConstraintSet.__bool__` to return when a constraint set is always
satisfied. That lets us still use
`static_assert(is_assignable_to(...))`, since the assertion will coerce
the constraint set to a bool, and also lets us
`reveal_type(is_assignable_to(...))` to see more detail about
whether/when the two types are assignable. That lets us get rid of
`reveal_when_assignable_to` and friends, since they are now redundant
with the expanded capabilities of `is_assignable_to`.
This commit is contained in:
Douglas Creager 2025-09-10 13:22:19 -04:00 committed by GitHub
parent ffead90410
commit 2ac4147435
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
12 changed files with 1231 additions and 223 deletions

View file

@ -129,7 +129,7 @@ specialization. Thus, the typevar is a subtype of itself and of `object`, but no
(including other typevars).
```py
from ty_extensions import reveal_when_assignable_to, reveal_when_subtype_of
from ty_extensions import is_assignable_to, is_subtype_of
class Super: ...
class Base(Super): ...
@ -137,23 +137,23 @@ class Sub(Base): ...
class Unrelated: ...
def unbounded_unconstrained[T, U](t: T, u: U) -> None:
reveal_when_assignable_to(T, T) # revealed: always
reveal_when_assignable_to(T, object) # revealed: always
reveal_when_assignable_to(T, Super) # revealed: never
reveal_when_assignable_to(U, U) # revealed: always
reveal_when_assignable_to(U, object) # revealed: always
reveal_when_assignable_to(U, Super) # revealed: never
reveal_when_assignable_to(T, U) # revealed: never
reveal_when_assignable_to(U, T) # revealed: never
reveal_type(is_assignable_to(T, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, object)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, U)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(U, object)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(U, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, T) # revealed: always
reveal_when_subtype_of(T, object) # revealed: always
reveal_when_subtype_of(T, Super) # revealed: never
reveal_when_subtype_of(U, U) # revealed: always
reveal_when_subtype_of(U, object) # revealed: always
reveal_when_subtype_of(U, Super) # revealed: never
reveal_when_subtype_of(T, U) # revealed: never
reveal_when_subtype_of(U, T) # revealed: never
reveal_type(is_subtype_of(T, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, object)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, U)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(U, object)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(U, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, T)) # revealed: ty_extensions.ConstraintSet[never]
```
A bounded typevar is assignable to its bound, and a bounded, fully static typevar is a subtype of
@ -167,40 +167,40 @@ from typing import Any
from typing_extensions import final
def bounded[T: Super](t: T) -> None:
reveal_when_assignable_to(T, Super) # revealed: always
reveal_when_assignable_to(T, Sub) # revealed: never
reveal_when_assignable_to(Super, T) # revealed: never
reveal_when_assignable_to(Sub, T) # revealed: never
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Sub, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, Super) # revealed: always
reveal_when_subtype_of(T, Sub) # revealed: never
reveal_when_subtype_of(Super, T) # revealed: never
reveal_when_subtype_of(Sub, T) # revealed: never
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Sub, T)) # revealed: ty_extensions.ConstraintSet[never]
def bounded_by_gradual[T: Any](t: T) -> None:
reveal_when_assignable_to(T, Any) # revealed: always
reveal_when_assignable_to(Any, T) # revealed: always
reveal_when_assignable_to(T, Super) # revealed: always
reveal_when_assignable_to(Super, T) # revealed: never
reveal_when_assignable_to(T, Sub) # revealed: always
reveal_when_assignable_to(Sub, T) # revealed: never
reveal_type(is_assignable_to(T, Any)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Any, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Sub)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Sub, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, Any) # revealed: never
reveal_when_subtype_of(Any, T) # revealed: never
reveal_when_subtype_of(T, Super) # revealed: never
reveal_when_subtype_of(Super, T) # revealed: never
reveal_when_subtype_of(T, Sub) # revealed: never
reveal_when_subtype_of(Sub, T) # revealed: never
reveal_type(is_subtype_of(T, Any)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Sub, T)) # revealed: ty_extensions.ConstraintSet[never]
@final
class FinalClass: ...
def bounded_final[T: FinalClass](t: T) -> None:
reveal_when_assignable_to(T, FinalClass) # revealed: always
reveal_when_assignable_to(FinalClass, T) # revealed: never
reveal_type(is_assignable_to(T, FinalClass)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(FinalClass, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, FinalClass) # revealed: always
reveal_when_subtype_of(FinalClass, T) # revealed: never
reveal_type(is_subtype_of(T, FinalClass)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(FinalClass, T)) # revealed: ty_extensions.ConstraintSet[never]
```
Two distinct fully static typevars are not subtypes of each other, even if they have the same
@ -210,18 +210,18 @@ typevars to `Never` in addition to that final class.
```py
def two_bounded[T: Super, U: Super](t: T, u: U) -> None:
reveal_when_assignable_to(T, U) # revealed: never
reveal_when_assignable_to(U, T) # revealed: never
reveal_type(is_assignable_to(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, U) # revealed: never
reveal_when_subtype_of(U, T) # revealed: never
reveal_type(is_subtype_of(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, T)) # revealed: ty_extensions.ConstraintSet[never]
def two_final_bounded[T: FinalClass, U: FinalClass](t: T, u: U) -> None:
reveal_when_assignable_to(T, U) # revealed: never
reveal_when_assignable_to(U, T) # revealed: never
reveal_type(is_assignable_to(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, U) # revealed: never
reveal_when_subtype_of(U, T) # revealed: never
reveal_type(is_subtype_of(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, T)) # revealed: ty_extensions.ConstraintSet[never]
```
A constrained fully static typevar is assignable to the union of its constraints, but not to any of
@ -232,64 +232,64 @@ intersection of all of its constraints is a subtype of the typevar.
from ty_extensions import Intersection
def constrained[T: (Base, Unrelated)](t: T) -> None:
reveal_when_assignable_to(T, Super) # revealed: never
reveal_when_assignable_to(T, Base) # revealed: never
reveal_when_assignable_to(T, Sub) # revealed: never
reveal_when_assignable_to(T, Unrelated) # revealed: never
reveal_when_assignable_to(T, Super | Unrelated) # revealed: always
reveal_when_assignable_to(T, Base | Unrelated) # revealed: always
reveal_when_assignable_to(T, Sub | Unrelated) # revealed: never
reveal_when_assignable_to(Super, T) # revealed: never
reveal_when_assignable_to(Unrelated, T) # revealed: never
reveal_when_assignable_to(Super | Unrelated, T) # revealed: never
reveal_when_assignable_to(Intersection[Base, Unrelated], T) # revealed: always
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Base)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Base | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Sub | Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_subtype_of(T, Super) # revealed: never
reveal_when_subtype_of(T, Base) # revealed: never
reveal_when_subtype_of(T, Sub) # revealed: never
reveal_when_subtype_of(T, Unrelated) # revealed: never
reveal_when_subtype_of(T, Super | Unrelated) # revealed: always
reveal_when_subtype_of(T, Base | Unrelated) # revealed: always
reveal_when_subtype_of(T, Sub | Unrelated) # revealed: never
reveal_when_subtype_of(Super, T) # revealed: never
reveal_when_subtype_of(Unrelated, T) # revealed: never
reveal_when_subtype_of(Super | Unrelated, T) # revealed: never
reveal_when_subtype_of(Intersection[Base, Unrelated], T) # revealed: always
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Base)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Base | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Sub | Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
reveal_when_assignable_to(T, Super) # revealed: always
reveal_when_assignable_to(T, Base) # revealed: always
reveal_when_assignable_to(T, Sub) # revealed: never
reveal_when_assignable_to(T, Unrelated) # revealed: never
reveal_when_assignable_to(T, Any) # revealed: always
reveal_when_assignable_to(T, Super | Any) # revealed: always
reveal_when_assignable_to(T, Super | Unrelated) # revealed: always
reveal_when_assignable_to(Super, T) # revealed: never
reveal_when_assignable_to(Base, T) # revealed: always
reveal_when_assignable_to(Unrelated, T) # revealed: never
reveal_when_assignable_to(Any, T) # revealed: always
reveal_when_assignable_to(Super | Any, T) # revealed: never
reveal_when_assignable_to(Base | Any, T) # revealed: always
reveal_when_assignable_to(Super | Unrelated, T) # revealed: never
reveal_when_assignable_to(Intersection[Base, Unrelated], T) # revealed: always
reveal_when_assignable_to(Intersection[Base, Any], T) # revealed: always
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Base)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Any)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Super | Any)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Base, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Any, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Super | Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Base | Any, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Intersection[Base, Any], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_subtype_of(T, Super) # revealed: never
reveal_when_subtype_of(T, Base) # revealed: never
reveal_when_subtype_of(T, Sub) # revealed: never
reveal_when_subtype_of(T, Unrelated) # revealed: never
reveal_when_subtype_of(T, Any) # revealed: never
reveal_when_subtype_of(T, Super | Any) # revealed: never
reveal_when_subtype_of(T, Super | Unrelated) # revealed: never
reveal_when_subtype_of(Super, T) # revealed: never
reveal_when_subtype_of(Base, T) # revealed: never
reveal_when_subtype_of(Unrelated, T) # revealed: never
reveal_when_subtype_of(Any, T) # revealed: never
reveal_when_subtype_of(Super | Any, T) # revealed: never
reveal_when_subtype_of(Base | Any, T) # revealed: never
reveal_when_subtype_of(Super | Unrelated, T) # revealed: never
reveal_when_subtype_of(Intersection[Base, Unrelated], T) # revealed: never
reveal_when_subtype_of(Intersection[Base, Any], T) # revealed: never
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Base)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Any)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Super | Any)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Base, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super | Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Base | Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Intersection[Base, Any], T)) # revealed: ty_extensions.ConstraintSet[never]
```
Two distinct fully static typevars are not subtypes of each other, even if they have the same
@ -299,43 +299,43 @@ the same type.
```py
def two_constrained[T: (int, str), U: (int, str)](t: T, u: U) -> None:
reveal_when_assignable_to(T, U) # revealed: never
reveal_when_assignable_to(U, T) # revealed: never
reveal_type(is_assignable_to(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, U) # revealed: never
reveal_when_subtype_of(U, T) # revealed: never
reveal_type(is_subtype_of(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, T)) # revealed: ty_extensions.ConstraintSet[never]
@final
class AnotherFinalClass: ...
def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, AnotherFinalClass)](t: T, u: U) -> None:
reveal_when_assignable_to(T, U) # revealed: never
reveal_when_assignable_to(U, T) # revealed: never
reveal_type(is_assignable_to(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(U, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_when_subtype_of(T, U) # revealed: never
reveal_when_subtype_of(U, T) # revealed: never
reveal_type(is_subtype_of(T, U)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U, T)) # revealed: ty_extensions.ConstraintSet[never]
```
A bound or constrained typevar is a subtype of itself in a union:
```py
def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
reveal_when_assignable_to(T, T | None) # revealed: always
reveal_when_assignable_to(U, U | None) # revealed: always
reveal_type(is_assignable_to(T, T | None)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(U, U | None)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_subtype_of(T, T | None) # revealed: always
reveal_when_subtype_of(U, U | None) # revealed: always
reveal_type(is_subtype_of(T, T | None)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(U, U | None)) # revealed: ty_extensions.ConstraintSet[always]
```
A bound or constrained typevar in a union with a dynamic type is assignable to the typevar:
```py
def union_with_dynamic[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
reveal_when_assignable_to(T | Any, T) # revealed: always
reveal_when_assignable_to(U | Any, U) # revealed: always
reveal_type(is_assignable_to(T | Any, T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(U | Any, U)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_subtype_of(T | Any, T) # revealed: never
reveal_when_subtype_of(U | Any, U) # revealed: never
reveal_type(is_subtype_of(T | Any, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(U | Any, U)) # revealed: ty_extensions.ConstraintSet[never]
```
And an intersection of a typevar with another type is always a subtype of the TypeVar:
@ -346,11 +346,11 @@ from ty_extensions import Intersection, Not, is_disjoint_from, static_assert
class A: ...
def inter[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
reveal_when_assignable_to(Intersection[T, Unrelated], T) # revealed: always
reveal_when_subtype_of(Intersection[T, Unrelated], T) # revealed: always
reveal_type(is_assignable_to(Intersection[T, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(Intersection[T, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_assignable_to(Intersection[U, A], U) # revealed: always
reveal_when_subtype_of(Intersection[U, A], U) # revealed: always
reveal_type(is_assignable_to(Intersection[U, A], U)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(Intersection[U, A], U)) # revealed: ty_extensions.ConstraintSet[always]
static_assert(is_disjoint_from(Not[T], T))
static_assert(is_disjoint_from(T, Not[T]))
@ -647,14 +647,14 @@ The intersection of a typevar with any other type is assignable to (and if fully
of) itself.
```py
from ty_extensions import reveal_when_assignable_to, reveal_when_subtype_of, Not
from ty_extensions import is_assignable_to, is_subtype_of, Not
def intersection_is_assignable[T](t: T) -> None:
reveal_when_assignable_to(Intersection[T, None], T) # revealed: always
reveal_when_assignable_to(Intersection[T, Not[None]], T) # revealed: always
reveal_type(is_assignable_to(Intersection[T, None], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(Intersection[T, Not[None]], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_when_subtype_of(Intersection[T, None], T) # revealed: always
reveal_when_subtype_of(Intersection[T, Not[None]], T) # revealed: always
reveal_type(is_subtype_of(Intersection[T, None], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(Intersection[T, Not[None]], T)) # revealed: ty_extensions.ConstraintSet[always]
```
## Narrowing

View file

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

View file

@ -0,0 +1,769 @@
# Constraints
```toml
[environment]
python-version = "3.13"
```
For "concrete" types (which contain no type variables), type properties like assignability have
simple answers: one type is either assignable to another type, or it isn't. (The _rules_ for
comparing two particular concrete types can be rather complex, but the _answer_ is a simple "yes" or
"no".)
These properties are more complex when type variables are involved, because there are (usually) many
different concrete types that a typevar can be specialized to, and the type property might hold for
some specializations, but not for others. That means that for types that include typevars, "Is this
type assignable to another?" no longer makes sense as a question. The better question is: "Under
what constraints is this type assignable to another?".
An individual constraint restricts the specialization of a single typevar. You can then build up
more complex constraint sets using union, intersection, and negation operations. We use a
disjunctive normal form (DNF) representation, just like we do for types: a _constraint set_ is the
union of zero or more _clauses_, each of which is the intersection of zero or more _individual
constraints_. Note that the constraint set that contains no clauses is never satisfiable
(` {} = 0`); and the constraint set that contains a single clause, where that clause contains no
constraints, is always satisfiable (` {⋂ {}} = 1`).
## Kinds of constraints
### Range
A _range_ constraint requires the typevar to be within a particular lower and upper bound: the
typevar can only specialize to a type that is a supertype of the lower bound, and a subtype of the
upper bound.
```py
from typing import Any, final, Never, Sequence
from ty_extensions import range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super))
```
Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower
bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
reveal_type(range_constraint(Never, T, Base))
```
Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
no upper bound.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
reveal_type(range_constraint(Base, T, object))
```
And a range constraint with _both_ a lower bound of `Never` and an upper bound of `object` does not
constrain the typevar at all.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(range_constraint(Never, T, object))
```
If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
or incomparable, then 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))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Base, T, Unrelated))
```
The lower and upper bound can be the same type, in which case the typevar can only be specialized to
that specific type.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Base, T, Base))
```
Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
their bottom and top materializations, respectively.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
reveal_type(range_constraint(Base, T, Any))
# revealed: ty_extensions.ConstraintSet[(Sequence[Base] ≤ T@_ ≤ Sequence[object])]
reveal_type(range_constraint(Sequence[Base], T, Sequence[Any]))
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
reveal_type(range_constraint(Any, T, Base))
# revealed: ty_extensions.ConstraintSet[(Sequence[Never] ≤ T@_ ≤ Sequence[Base])]
reveal_type(range_constraint(Sequence[Any], T, Sequence[Base]))
```
### Not equivalent
A _not-equivalent_ constraint requires the typevar to specialize to anything _other_ than a
particular type (the "hole").
```py
from typing import Any, Never, Sequence
from ty_extensions import not_equivalent_constraint
class Base: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base))
```
Unlike range constraints, `Never` and `object` are not special when used as the hole of a
not-equivalent constraint — there are many types that are not equivalent to `Never` or `object`.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Never)]
reveal_type(not_equivalent_constraint(T, Never))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ object)]
reveal_type(not_equivalent_constraint(T, object))
```
Constraints can only refer to fully static types. However, not-equivalent constraints are not
created directly; they are only created when negating a range constraint. Since that range
constraint will have fully static lower and upper bounds, the not-equivalent constraints that we
create will already have a fully static hole. Therefore, we raise a diagnostic when calling the
internal `not_equivalent_constraint` constructor with a non-fully-static type.
```py
def _[T]() -> None:
# error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type"
reveal_type(not_equivalent_constraint(T, Any)) # revealed: ConstraintSet
# error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type"
reveal_type(not_equivalent_constraint(T, Sequence[Any])) # revealed: ConstraintSet
```
### Incomparable
An _incomparable_ constraint requires the typevar to specialize to any type that is neither a
subtype nor a supertype of a particular type (the "pivot").
```py
from typing import Any, Never, Sequence
from ty_extensions import incomparable_constraint
class Base: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base))
```
Every type is comparable with `Never` and with `object`, so an incomparable constraint with either
as a pivot cannot ever be satisfied.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(incomparable_constraint(T, Never))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(incomparable_constraint(T, object))
```
Constraints can only refer to fully static types. However, incomparable constraints are not created
directly; they are only created when negating a range constraint. Since that range constraint will
have fully static lower and upper bounds, the incomparable constraints that we create will already
have a fully static hole. Therefore, we raise a diagnostic when calling the internal
`incomparable_constraint` constructor with a non-fully-static type.
```py
def _[T]() -> None:
# error: [invalid-argument-type] "Incomparable constraint must have a fully static type"
reveal_type(incomparable_constraint(T, Any)) # revealed: ConstraintSet
# error: [invalid-argument-type] "Incomparable constraint must have a fully static type"
reveal_type(incomparable_constraint(T, Sequence[Any])) # revealed: ConstraintSet
```
## Intersection
The intersection of two constraint sets requires that the constraints in both sets hold. In many
cases, we can simplify the result of an intersection.
### Different typevars
```py
from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
```
We cannot simplify the intersection of constraints that refer to different typevars.
```py
def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (U@_ ≁ Base))]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(U, Base))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (U@_ ≠ Base))]
reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(U, Base))
# revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base))]
reveal_type(range_constraint(Sub, T, Base) & range_constraint(Sub, U, Base))
```
Intersection is reflexive.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base))
```
### Intersection of two ranges
The intersection of two ranges is where the ranges "overlap".
```py
from typing import final
from ty_extensions import range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
class SubSub(Sub): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(SubSub, T, Base) & range_constraint(Sub, T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(SubSub, T, Super) & range_constraint(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) & range_constraint(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super) & range_constraint(Sub, T, Super))
```
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))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Unrelated, T, object))
```
### Intersection of range and not-equivalent
If the hole of a not-equivalent constraint is within the lower and upper bounds of a range
constraint, the intersection "removes" the hole from the range. The intersection cannot be
simplified.
```py
from typing import final
from ty_extensions import not_equivalent_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Super) ∧ (T@_ ≠ Base))]
reveal_type(range_constraint(Sub, T, Super) & not_equivalent_constraint(T, Base))
```
If the hole is not within the lower and upper bounds (because it's a subtype of the lower bound, a
supertype of the upper bound, or not comparable with either), then removing the hole doesn't do
anything.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Unrelated))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Unrelated))
```
If the lower and upper bounds are the same, it's actually an "equivalent" constraint. If the hole is
also that same type, then the intersection is empty — the not-equivalent constraint removes the only
type that satisfies the range constraint.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Base, T, Base) & not_equivalent_constraint(T, Base))
```
### Intersection of range and incomparable
The intersection of a range constraint and an incomparable constraint cannot be satisfied if the
pivot is a subtype of the lower bound, or a supertype of the upper bound. (If the pivot is a subtype
of the lower bound, then by transitivity, the pivot is also a subtype of everything in the range.)
```py
from typing import final
from ty_extensions import incomparable_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Base))
```
Otherwise, the intersection cannot be simplified.
```py
from ty_extensions import is_subtype_of
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[((Base ≤ T@_ ≤ Super) ∧ (T@_ ≁ Unrelated))]
reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Unrelated))
```
### Intersection of two not-equivalents
Intersection is reflexive, so the intersection of a not-equivalent constraint with itself is itself.
```py
from typing import final
from ty_extensions import not_equivalent_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Super))]
reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Sub))]
reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Unrelated))]
reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Unrelated))
```
### Intersection of not-equivalent and incomparable
When intersecting a not-equivalent constraint and an incomparable constraint, if the hole and pivot
are comparable, then the incomparable constraint already excludes the hole, so removing the hole
doesn't do anything.
```py
from typing import final
from ty_extensions import incomparable_constraint, not_equivalent_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(not_equivalent_constraint(T, Super) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(not_equivalent_constraint(T, Sub) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Unrelated) ∧ (T@_ ≁ Base))]
reveal_type(not_equivalent_constraint(T, Unrelated) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Super)]
reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Sub)]
reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≁ Unrelated))]
reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Unrelated))
```
### Intersection of two incomparables
We can only simplify the intersection of two incomparable constraints if they have the same pivot.
```py
from typing import final
from ty_extensions import incomparable_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Super))]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Sub))]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Unrelated))]
reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Unrelated))
```
## Union
The union of two constraint sets requires that the constraints in either set hold. In many cases, we
can simplify the result of an union.
### Different typevars
```py
from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
```
We cannot simplify the union of constraints that refer to different typevars.
```py
def _[T, U]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) (U@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(U, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base) (U@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(U, Base))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) (Sub ≤ U@_ ≤ Base)]
reveal_type(range_constraint(Sub, T, Base) | range_constraint(Sub, U, Base))
```
Union is reflexive.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base))
```
### Union of two ranges
When one of the bounds is entirely contained within the other, the union simplifies to the larger
bounds.
```py
from typing import final
from ty_extensions import range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
class SubSub(Sub): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Super) | range_constraint(Sub, T, Super))
```
Otherwise, the union cannot be simplified.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) (Base ≤ T@_ ≤ Super)]
reveal_type(range_constraint(Sub, T, Base) | range_constraint(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) (Base ≤ T@_ ≤ Super)]
reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super))
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) (Unrelated ≤ T@_)]
reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Unrelated, T, object))
```
In particular, the following does not simplify, even though it seems like it could simplify to
`SubSub ≤ T@_ ≤ Super`. The issue is that there are types that are within the bounds of
`SubSub ≤ T@_ ≤ Super`, but which are not comparable to `Base` or `Sub`, and which therefore should
not be included in the union. An example would be the type that contains all instances of `Super`,
`Base`, and `SubSub` (but _not_ including instances of `Sub`). (We don't have a way to spell that
type at the moment, but it is a valid type.) That type is not in `SubSub ≤ T ≤ Base`, since it
includes `Super`, which is outside the range. It's also not in `Sub ≤ T ≤ Super`, because it does
not include `Sub`. That means it should not be in the union. Since that type _is_ in
`SubSub ≤ T ≤ Super`, it is not correct to simplify the union in this way.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Base) (Sub ≤ T@_ ≤ Super)]
reveal_type(range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super))
```
### Union of range and not-equivalent
If the hole of a not-equivalent constraint is within the lower and upper bounds of a range
constraint, the range "fills in" the hole. The resulting union can always be satisfied.
```py
from typing import final
from ty_extensions import not_equivalent_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(range_constraint(Sub, T, Super) | not_equivalent_constraint(T, Base))
```
Otherwise the range constraint is subsumed by the not-equivalent constraint.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)]
reveal_type(range_constraint(Sub, T, Base) | not_equivalent_constraint(T, Super))
```
### Union of range and incomparable
When the "pivot" of the incomparable constraint is not comparable with either bound of the range
constraint, the incomparable constraint subsumes the range constraint.
```py
from typing import final
from ty_extensions import incomparable_constraint, range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Unrelated)]
reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Unrelated))
```
Otherwise, the union cannot be simplified.
```py
from ty_extensions import is_subtype_of
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) (T@_ ≁ Base)]
reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) (T@_ ≁ Sub)]
reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) (T@_ ≁ Super)]
reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Super))
```
### Union of two not-equivalents
Union is reflexive, so the union of a not-equivalent constraint with itself is itself. The union of
two different not-equivalent constraints is always satisfied.
```py
from typing import final
from ty_extensions import not_equivalent_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Unrelated))
```
### Union of not-equivalent and incomparable
When the hole of the non-equivalent constraint and the pivot of the incomparable constraint are not
comparable, then the hole is covered by the incomparable constraint, and the union is therefore
always satisfied.
```py
from typing import final
from ty_extensions import incomparable_constraint, not_equivalent_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(not_equivalent_constraint(T, Unrelated) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Unrelated))
```
Otherwise, the hole and pivot are comparable, and the non-equivalent constraint subsumes the
incomparable constraint.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)]
reveal_type(not_equivalent_constraint(T, Super) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ Sub)]
reveal_type(not_equivalent_constraint(T, Sub) | incomparable_constraint(T, Base))
```
### Union of two incomparables
We can only simplify the union of two incomparable constraints if they have the same pivot.
```py
from typing import final
from ty_extensions import incomparable_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
@final
class Unrelated: ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) (T@_ ≁ Super)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Super))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) (T@_ ≁ Sub)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) (T@_ ≁ Unrelated)]
reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Unrelated))
```
## Negation
### Negation of a range constraint
In the negation of a range constraint, the typevar must specialize to a type that is not a subtype
of the lower bound, or is not a supertype of the upper bound. Subtyping is a partial order, so one
type is not a subtype of another if it is a _proper_ supertype, or if they are incomparable.
```py
from typing import Never
from ty_extensions import range_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) (T@_ ≁ Sub) ((Base ≤ T@_) ∧ (T@_ ≠ Base)) (T@_ ≁ Base)]
reveal_type(~range_constraint(Sub, T, Base))
# revealed: ty_extensions.ConstraintSet[((Base ≤ T@_) ∧ (T@_ ≠ Base)) (T@_ ≁ Base)]
reveal_type(~range_constraint(Never, T, Base))
# revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) (T@_ ≁ Sub)]
reveal_type(~range_constraint(Sub, T, object))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(~range_constraint(Never, T, object))
```
### Negation of a not-equivalent constraint
In the negation of a not-equivalent constrant, the typevar must specialize to a type that _is_
equivalent to the hole. The negation does not include types that are incomparable with the hole —
those types are not equivalent to the hole, and are therefore in the original not-equivalent
constraint, not its negation.
```py
from typing import Never
from ty_extensions import not_equivalent_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
reveal_type(~not_equivalent_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Sub)]
reveal_type(~not_equivalent_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Never)]
reveal_type(~not_equivalent_constraint(T, Never))
# revealed: ty_extensions.ConstraintSet[(object ≤ T@_)]
reveal_type(~not_equivalent_constraint(T, object))
```
### Negation of an incomparable constraint
In the negation of an incomparable constraint, the typevar must specialize to a type that _is_
comparable with (either a subtype _or_ supertype of) the pivot.
```py
from typing import Never
from ty_extensions import incomparable_constraint
class Super: ...
class Base(Super): ...
class Sub(Base): ...
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base) (Base ≤ T@_)]
reveal_type(~incomparable_constraint(T, Base))
# revealed: ty_extensions.ConstraintSet[(T@_ ≤ Sub) (Sub ≤ T@_)]
reveal_type(~incomparable_constraint(T, Sub))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~incomparable_constraint(T, Never))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(~incomparable_constraint(T, object))
```

View file

@ -1708,7 +1708,7 @@ static_assert(is_subtype_of(TypeOf[B], Callable[[], B]))
class C: ...
# TODO: This assertion should be true once we understand `Self`
# error: [static-assert-error] "Static assertion error: argument evaluates to `False`"
# error: [static-assert-error] "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy"
static_assert(is_subtype_of(TypeOf[C], Callable[[], C]))
class D[T]:
@ -1865,7 +1865,7 @@ static_assert(not is_subtype_of(TypeOf[a.f], Callable[[float], int]))
static_assert(not is_subtype_of(TypeOf[A.g], Callable[[], int]))
# TODO: This assertion should be true
# error: [static-assert-error] "Static assertion error: argument evaluates to `False`"
# error: [static-assert-error] "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy"
static_assert(is_subtype_of(TypeOf[A.f], Callable[[A, int], int]))
```

View file

@ -3838,6 +3838,11 @@ impl<'db> Type<'db> {
Truthiness::Ambiguous
}
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked_set)) => {
let constraints = tracked_set.constraints(db);
Truthiness::from(constraints.is_always_satisfied(db))
}
Type::FunctionLiteral(_)
| Type::BoundMethod(_)
| Type::WrapperDescriptor(_)
@ -4186,8 +4191,8 @@ impl<'db> Type<'db> {
Type::FunctionLiteral(function_type) => match function_type.known(db) {
Some(
KnownFunction::IsEquivalentTo
| KnownFunction::IsSubtypeOf
| KnownFunction::IsAssignableTo
| KnownFunction::IsSubtypeOf
| KnownFunction::IsDisjointFrom,
) => Binding::single(
self,
@ -4200,25 +4205,58 @@ impl<'db> Type<'db> {
.type_form()
.with_annotated_type(Type::any()),
]),
Some(KnownClass::Bool.to_instance(db)),
Some(KnownClass::ConstraintSet.to_instance(db)),
),
)
.into(),
Some(
KnownFunction::RevealWhenAssignableTo | KnownFunction::RevealWhenSubtypeOf,
) => Binding::single(
Some(KnownFunction::RangeConstraint) => Binding::single(
self,
Signature::new(
Parameters::new([
Parameter::positional_only(Some(Name::new_static("a")))
Parameter::positional_only(Some(Name::new_static("lower_bound")))
.type_form()
.with_annotated_type(Type::any()),
Parameter::positional_only(Some(Name::new_static("b")))
Parameter::positional_only(Some(Name::new_static("typevar")))
.type_form()
.with_annotated_type(Type::any()),
Parameter::positional_only(Some(Name::new_static("upper_bound")))
.type_form()
.with_annotated_type(Type::any()),
]),
Some(KnownClass::NoneType.to_instance(db)),
Some(KnownClass::ConstraintSet.to_instance(db)),
),
)
.into(),
Some(KnownFunction::NotEquivalentConstraint) => Binding::single(
self,
Signature::new(
Parameters::new([
Parameter::positional_only(Some(Name::new_static("typevar")))
.type_form()
.with_annotated_type(Type::any()),
Parameter::positional_only(Some(Name::new_static("hole")))
.type_form()
.with_annotated_type(Type::any()),
]),
Some(KnownClass::ConstraintSet.to_instance(db)),
),
)
.into(),
Some(KnownFunction::IncomparableConstraint) => Binding::single(
self,
Signature::new(
Parameters::new([
Parameter::positional_only(Some(Name::new_static("typevar")))
.type_form()
.with_annotated_type(Type::any()),
Parameter::positional_only(Some(Name::new_static("pivot")))
.type_form()
.with_annotated_type(Type::any()),
]),
Some(KnownClass::ConstraintSet.to_instance(db)),
),
)
.into(),
@ -5702,6 +5740,10 @@ impl<'db> Type<'db> {
invalid_expressions: smallvec::smallvec![InvalidTypeExpression::Field],
fallback_type: Type::unknown(),
}),
KnownInstanceType::ConstraintSet(__call__) => Err(InvalidTypeExpressionError {
invalid_expressions: smallvec::smallvec![InvalidTypeExpression::ConstraintSet],
fallback_type: Type::unknown(),
}),
KnownInstanceType::SubscriptedProtocol(_) => Err(InvalidTypeExpressionError {
invalid_expressions: smallvec::smallvec_inline![
InvalidTypeExpression::Protocol
@ -6851,6 +6893,20 @@ impl<'db> TypeMapping<'_, 'db> {
}
}
/// A Salsa-tracked constraint set. This is only needed to have something appropriately small to
/// put in a [`KnownInstance::ConstraintSet`]. We don't actually manipulate these as part of using
/// constraint sets to check things like assignability; they're only used as a debugging aid in
/// mdtests. That means there's no need for this to be interned; being tracked is sufficient.
#[salsa::tracked(debug, heap_size=ruff_memory_usage::heap_size)]
#[derive(PartialOrd, Ord)]
pub struct TrackedConstraintSet<'db> {
#[returns(ref)]
constraints: ConstraintSet<'db>,
}
// The Salsa heap is tracked separately.
impl get_size2::GetSize for TrackedConstraintSet<'_> {}
/// Singleton types that are heavily special-cased by ty. Despite its name,
/// quite a different type to [`NominalInstanceType`].
///
@ -6893,6 +6949,10 @@ pub enum KnownInstanceType<'db> {
/// A single instance of `dataclasses.Field`
Field(FieldInstance<'db>),
/// A constraint set, which is exposed in mdtests as an instance of
/// `ty_extensions.ConstraintSet`.
ConstraintSet(TrackedConstraintSet<'db>),
}
fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
@ -6911,7 +6971,7 @@ fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
KnownInstanceType::TypeAliasType(type_alias) => {
visitor.visit_type_alias_type(db, type_alias);
}
KnownInstanceType::Deprecated(_) => {
KnownInstanceType::Deprecated(_) | KnownInstanceType::ConstraintSet(_) => {
// Nothing to visit
}
KnownInstanceType::Field(field) => {
@ -6938,6 +6998,10 @@ impl<'db> KnownInstanceType<'db> {
Self::Deprecated(deprecated)
}
Self::Field(field) => Self::Field(field.normalized_impl(db, visitor)),
Self::ConstraintSet(set) => {
// Nothing to normalize
Self::ConstraintSet(set)
}
}
}
@ -6951,6 +7015,7 @@ impl<'db> KnownInstanceType<'db> {
Self::TypeAliasType(_) => KnownClass::TypeAliasType,
Self::Deprecated(_) => KnownClass::Deprecated,
Self::Field(_) => KnownClass::Field,
Self::ConstraintSet(_) => KnownClass::ConstraintSet,
}
}
@ -7010,6 +7075,20 @@ impl<'db> KnownInstanceType<'db> {
field.default_type(self.db).display(self.db).fmt(f)?;
f.write_str("]")
}
KnownInstanceType::ConstraintSet(tracked_set) => {
let constraints = tracked_set.constraints(self.db);
if constraints.is_always_satisfied(self.db) {
f.write_str("ty_extensions.ConstraintSet[always]")
} else if constraints.is_never_satisfied(self.db) {
f.write_str("ty_extensions.ConstraintSet[never]")
} else {
write!(
f,
"ty_extensions.ConstraintSet[{}]",
constraints.display(self.db)
)
}
}
}
}
}
@ -7249,6 +7328,8 @@ enum InvalidTypeExpression<'db> {
Deprecated,
/// Same for `dataclasses.Field`
Field,
/// Same for `ty_extensions.ConstraintSet`
ConstraintSet,
/// Same for `typing.TypedDict`
TypedDict,
/// Type qualifiers are always invalid in *type expressions*,
@ -7298,6 +7379,9 @@ impl<'db> InvalidTypeExpression<'db> {
InvalidTypeExpression::Field => {
f.write_str("`dataclasses.Field` is not allowed in type expressions")
}
InvalidTypeExpression::ConstraintSet => {
f.write_str("`ty_extensions.ConstraintSet` is not allowed in type expressions")
}
InvalidTypeExpression::TypedDict => {
f.write_str(
"The special form `typing.TypedDict` is not allowed in type expressions. \

View file

@ -32,8 +32,8 @@ use crate::types::signatures::{Parameter, ParameterForm, Parameters};
use crate::types::tuple::{Tuple, TupleLength, TupleType};
use crate::types::{
BoundMethodType, ClassLiteral, DataclassParams, FieldInstance, KnownBoundMethodType,
KnownClass, KnownInstanceType, PropertyInstanceType, SpecialFormType, TypeAliasType,
TypeMapping, UnionType, WrapperDescriptorKind, enums, ide_support, todo_type,
KnownClass, KnownInstanceType, PropertyInstanceType, SpecialFormType, TrackedConstraintSet,
TypeAliasType, TypeMapping, UnionType, WrapperDescriptorKind, enums, ide_support, todo_type,
};
use ruff_db::diagnostic::{Annotation, Diagnostic, SubDiagnostic, SubDiagnosticSeverity};
use ruff_python_ast::{self as ast, PythonVersion};
@ -586,32 +586,43 @@ impl<'db> Bindings<'db> {
Type::FunctionLiteral(function_type) => match function_type.known(db) {
Some(KnownFunction::IsEquivalentTo) => {
if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
overload.set_return_type(Type::BooleanLiteral(
ty_a.is_equivalent_to(db, *ty_b),
let constraints =
ty_a.when_equivalent_to::<ConstraintSet>(db, *ty_b);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(
KnownInstanceType::ConstraintSet(tracked),
));
}
}
Some(KnownFunction::IsSubtypeOf) => {
if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
overload.set_return_type(Type::BooleanLiteral(
ty_a.is_subtype_of(db, *ty_b),
let constraints = ty_a.when_subtype_of::<ConstraintSet>(db, *ty_b);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(
KnownInstanceType::ConstraintSet(tracked),
));
}
}
Some(KnownFunction::IsAssignableTo) => {
if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
overload.set_return_type(Type::BooleanLiteral(
ty_a.is_assignable_to(db, *ty_b),
let constraints =
ty_a.when_assignable_to::<ConstraintSet>(db, *ty_b);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(
KnownInstanceType::ConstraintSet(tracked),
));
}
}
Some(KnownFunction::IsDisjointFrom) => {
if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
overload.set_return_type(Type::BooleanLiteral(
ty_a.is_disjoint_from(db, *ty_b),
let constraints =
ty_a.when_disjoint_from::<ConstraintSet>(db, *ty_b);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(
KnownInstanceType::ConstraintSet(tracked),
));
}
}

View file

@ -3652,6 +3652,8 @@ pub enum KnownClass {
TypedDictFallback,
// string.templatelib
Template,
// ty_extensions
ConstraintSet,
}
impl KnownClass {
@ -3751,6 +3753,7 @@ impl KnownClass {
| Self::InitVar
| Self::NamedTupleFallback
| Self::NamedTupleLike
| Self::ConstraintSet
| Self::TypedDictFallback => Some(Truthiness::Ambiguous),
Self::Tuple => None,
@ -3830,6 +3833,7 @@ impl KnownClass {
| KnownClass::InitVar
| KnownClass::NamedTupleFallback
| KnownClass::NamedTupleLike
| KnownClass::ConstraintSet
| KnownClass::TypedDictFallback
| KnownClass::BuiltinFunctionType
| KnownClass::Template => false,
@ -3908,6 +3912,7 @@ impl KnownClass {
| KnownClass::InitVar
| KnownClass::NamedTupleFallback
| KnownClass::NamedTupleLike
| KnownClass::ConstraintSet
| KnownClass::TypedDictFallback
| KnownClass::BuiltinFunctionType
| KnownClass::Template => false,
@ -3986,6 +3991,7 @@ impl KnownClass {
| KnownClass::TypedDictFallback
| KnownClass::NamedTupleLike
| KnownClass::NamedTupleFallback
| KnownClass::ConstraintSet
| KnownClass::BuiltinFunctionType
| KnownClass::Template => false,
}
@ -4075,6 +4081,7 @@ impl KnownClass {
| Self::KwOnly
| Self::InitVar
| Self::NamedTupleFallback
| Self::ConstraintSet
| Self::TypedDictFallback
| Self::BuiltinFunctionType
| Self::Template => false,
@ -4173,6 +4180,7 @@ impl KnownClass {
Self::InitVar => "InitVar",
Self::NamedTupleFallback => "NamedTupleFallback",
Self::NamedTupleLike => "NamedTupleLike",
Self::ConstraintSet => "ConstraintSet",
Self::TypedDictFallback => "TypedDictFallback",
Self::Template => "Template",
}
@ -4439,7 +4447,7 @@ impl KnownClass {
| Self::OrderedDict => KnownModule::Collections,
Self::Field | Self::KwOnly | Self::InitVar => KnownModule::Dataclasses,
Self::NamedTupleFallback | Self::TypedDictFallback => KnownModule::TypeCheckerInternals,
Self::NamedTupleLike => KnownModule::TyExtensions,
Self::NamedTupleLike | Self::ConstraintSet => KnownModule::TyExtensions,
Self::Template => KnownModule::Templatelib,
}
}
@ -4518,6 +4526,7 @@ impl KnownClass {
| Self::Iterator
| Self::NamedTupleFallback
| Self::NamedTupleLike
| Self::ConstraintSet
| Self::TypedDictFallback
| Self::BuiltinFunctionType
| Self::Template => Some(false),
@ -4601,6 +4610,7 @@ impl KnownClass {
| Self::Iterator
| Self::NamedTupleFallback
| Self::NamedTupleLike
| Self::ConstraintSet
| Self::TypedDictFallback
| Self::BuiltinFunctionType
| Self::Template => false,
@ -4693,6 +4703,7 @@ impl KnownClass {
"InitVar" => Self::InitVar,
"NamedTupleFallback" => Self::NamedTupleFallback,
"NamedTupleLike" => Self::NamedTupleLike,
"ConstraintSet" => Self::ConstraintSet,
"TypedDictFallback" => Self::TypedDictFallback,
"Template" => Self::Template,
_ => return None,
@ -4761,6 +4772,7 @@ impl KnownClass {
| Self::NamedTupleFallback
| Self::TypedDictFallback
| Self::NamedTupleLike
| Self::ConstraintSet
| Self::Awaitable
| Self::Generator
| Self::Template => module == self.canonical_module(db),

View file

@ -166,7 +166,8 @@ impl<'db> ClassBase<'db> {
KnownInstanceType::TypeAliasType(_)
| KnownInstanceType::TypeVar(_)
| KnownInstanceType::Deprecated(_)
| KnownInstanceType::Field(_) => None,
| KnownInstanceType::Field(_)
| KnownInstanceType::ConstraintSet(_) => None,
},
Type::SpecialForm(special_form) => match special_form {

View file

@ -102,8 +102,12 @@ use smallvec::{SmallVec, smallvec};
use crate::Db;
use crate::types::{BoundTypeVarInstance, IntersectionType, Type, UnionType};
fn comparable<'db>(db: &'db dyn Db, left: Type<'db>, right: Type<'db>) -> bool {
left.is_subtype_of(db, right) || right.is_subtype_of(db, left)
}
fn incomparable<'db>(db: &'db dyn Db, left: Type<'db>, right: Type<'db>) -> bool {
!left.is_subtype_of(db, right) && !right.is_subtype_of(db, left)
!comparable(db, left, right)
}
/// Encodes the constraints under which a type property (e.g. assignability) holds.
@ -246,8 +250,8 @@ where
/// be simplified into a single clause.
///
/// [POPL2015]: https://doi.org/10.1145/2676726.2676991
#[derive(Clone, Debug)]
pub(crate) struct ConstraintSet<'db> {
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub struct ConstraintSet<'db> {
// NOTE: We use 2 here because there are a couple of places where we create unions of 2 clauses
// as temporary values — in particular when negating a constraint — and this lets us avoid
// spilling the temporary value to the heap.
@ -269,6 +273,42 @@ impl<'db> ConstraintSet<'db> {
}
}
pub(crate) fn range(
db: &'db dyn Db,
lower: Type<'db>,
typevar: BoundTypeVarInstance<'db>,
upper: Type<'db>,
) -> Self {
let lower = lower.bottom_materialization(db);
let upper = upper.top_materialization(db);
let constraint = Constraint::range(db, lower, upper).constrain(typevar);
let mut result = Self::never();
result.union_constraint(db, constraint);
result
}
pub(crate) fn not_equivalent(
db: &'db dyn Db,
typevar: BoundTypeVarInstance<'db>,
hole: Type<'db>,
) -> Self {
let constraint = Constraint::not_equivalent(db, hole).constrain(typevar);
let mut result = Self::never();
result.union_constraint(db, constraint);
result
}
pub(crate) fn incomparable(
db: &'db dyn Db,
typevar: BoundTypeVarInstance<'db>,
pivot: Type<'db>,
) -> Self {
let constraint = Constraint::incomparable(db, pivot).constrain(typevar);
let mut result = Self::never();
result.union_constraint(db, constraint);
result
}
/// Updates this set to be the union of itself and a constraint.
fn union_constraint(
&mut self,
@ -429,7 +469,7 @@ impl<'db> Constraints<'db> for ConstraintSet<'db> {
/// This is called a "constraint set", and denoted _C_, in [[POPL2015][]].
///
/// [POPL2015]: https://doi.org/10.1145/2676726.2676991
#[derive(Clone, Debug)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) struct ConstraintClause<'db> {
// NOTE: We use 1 here because most clauses only mention a single typevar.
constraints: SmallVec<[ConstrainedTypeVar<'db>; 1]>,
@ -810,7 +850,7 @@ impl<'db> ConstraintClause<'db> {
}
}
#[derive(Clone, Debug, Eq, PartialEq)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) struct ConstrainedTypeVar<'db> {
typevar: BoundTypeVarInstance<'db>,
constraint: Constraint<'db>,
@ -857,7 +897,7 @@ impl<'db> ConstrainedTypeVar<'db> {
}
}
#[derive(Clone, Debug, Eq, PartialEq)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) enum Constraint<'db> {
Range(RangeConstraint<'db>),
NotEquivalent(NotEquivalentConstraint<'db>),
@ -980,7 +1020,7 @@ impl<'db> Satisfiable<Constraint<'db>> {
}
}
#[derive(Clone, Debug, Eq, PartialEq)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) struct RangeConstraint<'db> {
lower: Type<'db>,
upper: Type<'db>,
@ -1054,7 +1094,7 @@ impl<'db> RangeConstraint<'db> {
db: &'db dyn Db,
other: &IncomparableConstraint<'db>,
) -> Simplifiable<Constraint<'db>> {
if other.ty.is_subtype_of(db, other.ty) || self.upper.is_subtype_of(db, other.ty) {
if other.ty.is_subtype_of(db, self.lower) || self.upper.is_subtype_of(db, other.ty) {
return Simplifiable::NeverSatisfiable;
}
@ -1189,7 +1229,7 @@ impl<'db> RangeConstraint<'db> {
}
}
#[derive(Clone, Debug, Eq, PartialEq)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) struct NotEquivalentConstraint<'db> {
ty: Type<'db>,
}
@ -1224,8 +1264,9 @@ impl<'db> NotEquivalentConstraint<'db> {
db: &'db dyn Db,
other: &IncomparableConstraint<'db>,
) -> Simplifiable<Constraint<'db>> {
// (α ≠ t) ∧ (a ≁ t) = a ≁ t
if self.ty.is_equivalent_to(db, other.ty) {
// If the hole and pivot are comparable, then removing the hole from the incomparable
// constraint doesn't do anything.
if comparable(db, self.ty, other.ty) {
return Simplifiable::Simplified(Constraint::Incomparable(other.clone()));
}
Simplifiable::NotSimplified(
@ -1302,7 +1343,7 @@ impl<'db> NotEquivalentConstraint<'db> {
}
}
#[derive(Clone, Debug, Eq, PartialEq)]
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
pub(crate) struct IncomparableConstraint<'db> {
ty: Type<'db>,
}

View file

@ -79,8 +79,9 @@ use crate::types::visitor::any_over_type;
use crate::types::{
BoundMethodType, BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, ClassType,
DeprecatedInstance, DynamicType, FindLegacyTypeVarsVisitor, HasRelationToVisitor,
IsEquivalentVisitor, KnownClass, NormalizedVisitor, SpecialFormType, Truthiness, Type,
TypeMapping, TypeRelation, UnionBuilder, all_members, binding_type, walk_type_mapping,
IsEquivalentVisitor, KnownClass, KnownInstanceType, NormalizedVisitor, SpecialFormType,
TrackedConstraintSet, Truthiness, Type, TypeMapping, TypeRelation, UnionBuilder, all_members,
binding_type, walk_type_mapping,
};
use crate::{Db, FxOrderSet, ModuleName, resolve_module};
@ -1255,10 +1256,12 @@ pub enum KnownFunction {
HasMember,
/// `ty_extensions.reveal_protocol_interface`
RevealProtocolInterface,
/// `ty_extensions.reveal_when_assignable_to`
RevealWhenAssignableTo,
/// `ty_extensions.reveal_when_subtype_of`
RevealWhenSubtypeOf,
/// `ty_extensions.range_constraint`
RangeConstraint,
/// `ty_extensions.not_equivalent_constraint`
NotEquivalentConstraint,
/// `ty_extensions.incomparable_constraint`
IncomparableConstraint,
}
impl KnownFunction {
@ -1324,8 +1327,9 @@ impl KnownFunction {
| Self::StaticAssert
| Self::HasMember
| Self::RevealProtocolInterface
| Self::RevealWhenAssignableTo
| Self::RevealWhenSubtypeOf
| Self::RangeConstraint
| Self::NotEquivalentConstraint
| Self::IncomparableConstraint
| Self::AllMembers => module.is_ty_extensions(),
Self::ImportModule => module.is_importlib(),
}
@ -1621,52 +1625,82 @@ impl KnownFunction {
overload.set_return_type(Type::module_literal(db, file, module));
}
KnownFunction::RevealWhenAssignableTo => {
let [Some(ty_a), Some(ty_b)] = overload.parameter_types() else {
return;
};
let constraints = ty_a.when_assignable_to::<ConstraintSet>(db, *ty_b);
let Some(builder) =
context.report_diagnostic(DiagnosticId::RevealedType, Severity::Info)
KnownFunction::RangeConstraint => {
let [
Some(lower),
Some(Type::NonInferableTypeVar(typevar)),
Some(upper),
] = parameter_types
else {
return;
};
let mut diag = builder.into_diagnostic("Assignability holds");
let span = context.span(call_expression);
if constraints.is_always_satisfied(db) {
diag.annotate(Annotation::primary(span).message("always"));
} else if constraints.is_never_satisfied(db) {
diag.annotate(Annotation::primary(span).message("never"));
} else {
diag.annotate(
Annotation::primary(span)
.message(format_args!("when {}", constraints.display(db))),
);
}
let constraints = ConstraintSet::range(db, *lower, *typevar, *upper);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
tracked,
)));
}
KnownFunction::RevealWhenSubtypeOf => {
let [Some(ty_a), Some(ty_b)] = overload.parameter_types() else {
KnownFunction::NotEquivalentConstraint => {
let [Some(Type::NonInferableTypeVar(typevar)), Some(hole)] = parameter_types else {
return;
};
let constraints = ty_a.when_subtype_of::<ConstraintSet>(db, *ty_b);
let Some(builder) =
context.report_diagnostic(DiagnosticId::RevealedType, Severity::Info)
if !hole.is_equivalent_to(db, hole.top_materialization(db)) {
if let Some(builder) =
context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
{
let mut diagnostic = builder.into_diagnostic(format_args!(
"Not-equivalent constraint must have a fully static type"
));
diagnostic.annotate(
Annotation::secondary(context.span(&call_expression.arguments.args[1]))
.message(format_args!(
"Type `{}` is not fully static",
hole.display(db)
)),
);
}
return;
}
let constraints = ConstraintSet::not_equivalent(db, *typevar, *hole);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
tracked,
)));
}
KnownFunction::IncomparableConstraint => {
let [Some(Type::NonInferableTypeVar(typevar)), Some(pivot)] = parameter_types
else {
return;
};
let mut diag = builder.into_diagnostic("Subtyping holds");
let span = context.span(call_expression);
if constraints.is_always_satisfied(db) {
diag.annotate(Annotation::primary(span).message("always"));
} else if constraints.is_never_satisfied(db) {
diag.annotate(Annotation::primary(span).message("never"));
} else {
diag.annotate(
Annotation::primary(span)
.message(format_args!("when {}", constraints.display(db))),
);
if !pivot.is_equivalent_to(db, pivot.top_materialization(db)) {
if let Some(builder) =
context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
{
let mut diagnostic = builder.into_diagnostic(format_args!(
"Incomparable constraint must have a fully static type"
));
diagnostic.annotate(
Annotation::secondary(context.span(&call_expression.arguments.args[1]))
.message(format_args!(
"Type `{}` is not fully static",
pivot.display(db)
)),
);
}
return;
}
let constraints = ConstraintSet::incomparable(db, *typevar, *pivot);
let tracked = TrackedConstraintSet::new(db, constraints);
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
tracked,
)));
}
_ => {}
@ -1729,8 +1763,9 @@ pub(crate) mod tests {
| KnownFunction::IsEquivalentTo
| KnownFunction::HasMember
| KnownFunction::RevealProtocolInterface
| KnownFunction::RevealWhenAssignableTo
| KnownFunction::RevealWhenSubtypeOf
| KnownFunction::RangeConstraint
| KnownFunction::NotEquivalentConstraint
| KnownFunction::IncomparableConstraint
| KnownFunction::AllMembers => KnownModule::TyExtensions,
KnownFunction::ImportModule => KnownModule::ImportLib,

View file

@ -93,6 +93,7 @@ use crate::semantic_index::{
};
use crate::types::call::{Binding, Bindings, CallArguments, CallError, CallErrorKind};
use crate::types::class::{CodeGeneratorKind, FieldKind, MetaclassErrorKind, MethodDecorator};
use crate::types::constraints::Constraints;
use crate::types::diagnostic::{
self, CALL_NON_CALLABLE, CONFLICTING_DECLARATIONS, CONFLICTING_METACLASS,
CYCLIC_CLASS_DEFINITION, DIVISION_BY_ZERO, DUPLICATE_KW_ONLY, INCONSISTENT_MRO,
@ -130,10 +131,10 @@ use crate::types::{
CallDunderError, CallableType, ClassLiteral, ClassType, DataclassParams, DynamicType,
IntersectionBuilder, IntersectionType, KnownClass, KnownInstanceType, LintDiagnosticGuard,
MemberLookupPolicy, MetaclassCandidate, PEP695TypeAliasType, Parameter, ParameterForm,
Parameters, SpecialFormType, SubclassOfType, Truthiness, Type, TypeAliasType,
TypeAndQualifiers, TypeIsType, TypeQualifiers, TypeVarBoundOrConstraintsEvaluation,
TypeVarDefaultEvaluation, TypeVarInstance, TypeVarKind, UnionBuilder, UnionType, binding_type,
todo_type,
Parameters, SpecialFormType, SubclassOfType, TrackedConstraintSet, Truthiness, Type,
TypeAliasType, TypeAndQualifiers, TypeIsType, TypeQualifiers,
TypeVarBoundOrConstraintsEvaluation, TypeVarDefaultEvaluation, TypeVarInstance, TypeVarKind,
UnionBuilder, UnionType, binding_type, todo_type,
};
use crate::unpack::{EvaluationMode, Unpack, UnpackPosition};
use crate::util::diagnostics::format_enumeration;
@ -7375,6 +7376,18 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
Type::IntLiteral(!i64::from(bool))
}
(
ast::UnaryOp::Invert,
Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)),
) => {
let constraints = constraints.constraints(self.db()).clone();
let result = constraints.negate(self.db());
Type::KnownInstance(KnownInstanceType::ConstraintSet(TrackedConstraintSet::new(
self.db(),
result,
)))
}
(ast::UnaryOp::Not, ty) => ty
.try_bool(self.db())
.unwrap_or_else(|err| {
@ -7726,6 +7739,32 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
op,
),
(
Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
ast::Operator::BitAnd,
) => {
let left = left.constraints(self.db()).clone();
let right = right.constraints(self.db()).clone();
let result = left.and(self.db(), || right);
Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
TrackedConstraintSet::new(self.db(), result),
)))
}
(
Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
ast::Operator::BitOr,
) => {
let left = left.constraints(self.db()).clone();
let right = right.constraints(self.db()).clone();
let result = left.or(self.db(), || right);
Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
TrackedConstraintSet::new(self.db(), result),
)))
}
// We've handled all of the special cases that we support for literals, so we need to
// fall back on looking for dunder methods on one of the operand types.
(
@ -10594,6 +10633,15 @@ impl<'db> TypeInferenceBuilder<'db, '_> {
}
Type::unknown()
}
KnownInstanceType::ConstraintSet(_) => {
self.infer_type_expression(&subscript.slice);
if let Some(builder) = self.context.report_lint(&INVALID_TYPE_FORM, subscript) {
builder.into_diagnostic(format_args!(
"`ty_extensions.ConstraintSet` is not allowed in type expressions",
));
}
Type::unknown()
}
KnownInstanceType::TypeVar(_) => {
self.infer_type_expression(&subscript.slice);
todo_type!("TypeVar annotations")