From f4e46c9a2c7a10c5eace3b56fcf80810a030bcd9 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 13 Nov 2025 08:40:42 -0500 Subject: [PATCH] add failing test --- .../type_properties/implies_subtype_of.md | 69 ++++++++++++++++++- 1 file changed, 68 insertions(+), 1 deletion(-) 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 35768ef76d..1a72da9464 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 @@ -173,7 +173,10 @@ def given_constraints[T](): static_assert(given_str.implies_subtype_of(T, str)) ``` -This might require propagating constraints from other typevars. +This might require propagating constraints from other typevars. (Note that we perform the test +twice, with different variable orderings. Our BDD implementation uses the Salsa IDs of each typevar +as part of the variable ordering. Reversing the typevar order helps us verify that we don't have any +BDD logic that is dependent on which variable ordering we end up with.) ```py def mutually_constrained[T, U](): @@ -183,6 +186,19 @@ def mutually_constrained[T, U](): static_assert(not given_int.implies_subtype_of(T, bool)) static_assert(not given_int.implies_subtype_of(T, str)) + # If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well. + given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int) + static_assert(given_int.implies_subtype_of(T, int)) + static_assert(not given_int.implies_subtype_of(T, bool)) + static_assert(not given_int.implies_subtype_of(T, str)) + +def mutually_constrained[U, T](): + # If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well. + given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int) + static_assert(given_int.implies_subtype_of(T, int)) + static_assert(not given_int.implies_subtype_of(T, bool)) + static_assert(not given_int.implies_subtype_of(T, str)) + # If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well. given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int) static_assert(given_int.implies_subtype_of(T, int)) @@ -236,6 +252,22 @@ def mutually_constrained[T, U](): 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) + 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])) + +# Repeat the test with a different typevar ordering +def mutually_constrained[U, T](): + # 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) + 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) @@ -281,6 +313,22 @@ def mutually_constrained[T, U](): 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) + 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])) + +# Repeat the test with a different typevar ordering +def mutually_constrained[U, T](): + # 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) + 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) @@ -338,6 +386,25 @@ def mutually_constrained[T, U](): 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(U, T, U) & ConstraintSet.range(int, U, int) + static_assert(given_int.implies_subtype_of(Invariant[T], Invariant[int])) + static_assert(given_int.implies_subtype_of(Invariant[int], Invariant[T])) + static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool])) + static_assert(not given_int.implies_subtype_of(Invariant[bool], Invariant[T])) + static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str])) + static_assert(not given_int.implies_subtype_of(Invariant[str], Invariant[T])) + +# Repeat the test with a different typevar ordering +def mutually_constrained[U, T](): + # 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(U, T, U) & ConstraintSet.range(int, U, int)