add failing test

This commit is contained in:
Douglas Creager 2025-11-13 08:40:42 -05:00
parent e4a32ba644
commit f4e46c9a2c

View file

@ -173,7 +173,10 @@ def given_constraints[T]():
static_assert(given_str.implies_subtype_of(T, str)) 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 ```py
def mutually_constrained[T, U](): 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, bool))
static_assert(not given_int.implies_subtype_of(T, str)) 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. # 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) given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
static_assert(given_int.implies_subtype_of(T, 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[bool]))
static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str])) 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 # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Covariant[T] ≤ Covariant[int]). # (Covariant[T] ≤ Covariant[int]).
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, 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[bool], Contravariant[T]))
static_assert(not given_int.implies_subtype_of(Contravariant[str], 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 # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
# (Contravariant[int] ≤ Contravariant[T]). # (Contravariant[int] ≤ Contravariant[T]).
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int) 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[bool]))
static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str])) 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 # 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]). # 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) given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(int, U, int)