add failing tests

This commit is contained in:
Douglas Creager 2025-11-10 09:09:09 -05:00
parent 33b942c7ad
commit ac16a9fc87
1 changed files with 196 additions and 2 deletions

View File

@ -12,8 +12,7 @@ a particular constraint set hold_.
## Concrete types ## Concrete types
For concrete types, constraint implication is exactly the same as subtyping. (A concrete type is any For concrete types, constraint implication is exactly the same as subtyping. (A concrete type is any
fully static type that is not a typevar. It can _contain_ a typevar, though — `list[T]` is fully static type that does not contain a typevar.)
considered concrete.)
```py ```py
from ty_extensions import ConstraintSet, is_subtype_of, static_assert from ty_extensions import ConstraintSet, is_subtype_of, static_assert
@ -191,4 +190,199 @@ def mutually_constrained[T, U]():
static_assert(not given_int.implies_subtype_of(T, str)) static_assert(not given_int.implies_subtype_of(T, str))
``` ```
## Compound types
All of the relationships in the above section also apply when a typevar appears in a compound type.
```py
from typing import Never
from ty_extensions import ConstraintSet, static_assert
class Covariant[T]:
def get(self) -> T:
raise ValueError
def given_constraints[T]():
static_assert(not ConstraintSet.always().implies_subtype_of(Covariant[T], Covariant[int]))
static_assert(not ConstraintSet.always().implies_subtype_of(Covariant[T], Covariant[bool]))
static_assert(not ConstraintSet.always().implies_subtype_of(Covariant[T], Covariant[str]))
# These are vacuously true; false implies anything
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[int]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[bool]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[str]))
# For a covariant typevar, (T ≤ int) implies that (Covariant[T] ≤ Covariant[int]).
given_int = ConstraintSet.range(Never, T, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
given_bool = ConstraintSet.range(Never, T, bool)
# TODO: no error
# error: [static-assert-error]
static_assert(given_bool.implies_subtype_of(Covariant[T], Covariant[int]))
# TODO: no error
# error: [static-assert-error]
static_assert(given_bool.implies_subtype_of(Covariant[T], Covariant[bool]))
static_assert(not given_bool.implies_subtype_of(Covariant[T], Covariant[str]))
def mutually_constrained[T, U]():
# If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Covariant[T] ≤ Covariant[int]).
given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
# If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Covariant[T] ≤ Covariant[int]).
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
```
Many of the relationships are reversed for typevars that appear in contravariant types.
```py
class Contravariant[T]:
def set(self, value: T):
pass
def given_constraints[T]():
static_assert(not ConstraintSet.always().implies_subtype_of(Contravariant[int], Contravariant[T]))
static_assert(not ConstraintSet.always().implies_subtype_of(Contravariant[bool], Contravariant[T]))
static_assert(not ConstraintSet.always().implies_subtype_of(Contravariant[str], Contravariant[T]))
# These are vacuously true; false implies anything
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[int], Contravariant[T]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[bool], Contravariant[T]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[str], Contravariant[T]))
# For a contravariant typevar, (T ≤ int) implies that (Contravariant[int] ≤ Contravariant[T]).
# (The order of the comparison is reversed because of contravariance.)
given_int = ConstraintSet.range(Never, T, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
given_bool = ConstraintSet.range(Never, T, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_bool.implies_subtype_of(Contravariant[int], Contravariant[T]))
# TODO: no error
# error: [static-assert-error]
static_assert(given_bool.implies_subtype_of(Contravariant[bool], Contravariant[T]))
static_assert(not given_bool.implies_subtype_of(Contravariant[str], Contravariant[T]))
def mutually_constrained[T, U]():
# If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Contravariant[int] ≤ Contravariant[T]).
given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
# If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Contravariant[int] ≤ Contravariant[T]).
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
```
For invariant typevars, subtyping of the typevar does not imply subtyping of the compound type in
either direction. But an equality constraint on the typevar does.
```py
class Invariant[T]:
def get(self) -> T:
raise ValueError
def set(self, value: T):
pass
def given_constraints[T]():
static_assert(not ConstraintSet.always().implies_subtype_of(Invariant[T], Invariant[int]))
static_assert(not ConstraintSet.always().implies_subtype_of(Invariant[T], Invariant[bool]))
static_assert(not ConstraintSet.always().implies_subtype_of(Invariant[T], Invariant[str]))
# These are vacuously true; false implies anything
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[int]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[bool]))
# TODO: no error
# error: [static-assert-error]
static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[str]))
# For an invariant typevar, (T ≤ int) does not imply that (Invariant[T] ≤ Invariant[int]).
given_int = ConstraintSet.range(Never, T, int)
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[int]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
# It also does not imply the contravariant ordering (Invariant[int] ≤ Invariant[T]).
static_assert(not given_int.implies_subtype_of(Invariant[int], Invariant[T]))
static_assert(not given_int.implies_subtype_of(Invariant[bool], Invariant[T]))
static_assert(not given_int.implies_subtype_of(Invariant[str], Invariant[T]))
# But (T = int) does imply both.
given_int = ConstraintSet.range(int, T, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Invariant[T], Invariant[int]))
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Invariant[int], Invariant[T]))
static_assert(not given_int.implies_subtype_of(Invariant[bool], Invariant[T]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
static_assert(not given_int.implies_subtype_of(Invariant[str], Invariant[T]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
def mutually_constrained[T, U]():
# If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well. But because T is invariant, that
# does _not_ imply that (Invariant[T] ≤ Invariant[int]).
given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[int]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
# If (T = U ∧ U = int), then (T = int) must be true as well. That is an equality constraint, so
# even though T is invariant, it does imply that (Invariant[T] ≤ Invariant[int]).
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(Invariant[T], Invariant[int]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
```
[subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence