From ac16a9fc87ef2338efc82d956db5d0863b35c602 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Mon, 10 Nov 2025 09:09:09 -0500 Subject: [PATCH] add failing tests --- .../type_properties/implies_subtype_of.md | 198 +++++++++++++++++- 1 file changed, 196 insertions(+), 2 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index ecb1adcada..e4f8d2267c 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -12,8 +12,7 @@ a particular constraint set hold_. ## Concrete types 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 -considered concrete.) +fully static type that does not contain a typevar.) ```py 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)) ``` +## 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