[ty] Update "constraint implication" relation to work on constraints between two typevars

[dcreager]

It's possible for a constraint to mention two typevars. For instance, in the body of

def f[S: int, T: S](): ...

the baseline constraint set would be (T ≤ S) ∧ (S ≤ int). That is, S must specialize to some subtype of int, and T must specialize to a subtype of the type that S specializes to.

This PR updates the new "constraint implication" relationship from #21010 to work on these kinds of constraint sets. For instance, in the example above, we should be able to see that T ≤ int must always hold:

def f[S, T]():
    constraints = ConstraintSet.range(Never, S, int) & ConstraintSet.range(Never, T, S)
    static_assert(constraints.implies_subtype_of(T, int))  # now succeeds!

This did not require major changes to the implementation of implies_subtype_of. That method already relies on how our simplify and domain methods expand a constraint set to include the transitive closure of the constraints that it mentions, and to mark certain combinations of constraints as impossible. Previously, that transitive closure logic only looked at pairs of constraints that constrain the same typevar. (For instance, to notice that (T ≤ bool) ∧ ¬(T ≤ int) is impossible.)

Now we also look at pairs of constraints that constraint different typevars, if one of the constraints is bound by the other — that is, pairs of the form T ≤ S and S ≤ something, or S ≤ T and something ≤ S. In those cases, transitivity lets us add a new derived constraint that T ≤ something or something ≤ T, respectively. Having done that, our existing implies_subtype_of logic finds and takes into account that derived constraint.

[github-actions]

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

[github-actions]

mypy_primer results

No ecosystem changes detected ✅
No memory usage changes detected ✅

[codspeed-hq]

CodSpeed Performance Report

Merging #21068 will not alter performance

_{Comparing dcreager/subtype-given-typevars (c054447) with main (d0aebaa)}

Summary

✅ 22 untouched
⏩ 30 skipped¹

Footnotes

1. 30 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩

[MichaReiser]

More an understand question for me. What's the difference between Never and passing U?

[dcreager]

range(Never, T, U) is Never ≤ T ≤ U, which simplifies to T ≤ U since every type is a supertype of Never.

range(U, T, U) is U ≤ T ≤ U, which simplifies to T = U.

So the first one is "T must be a subtype of U", and the second one is "T must be exactly the same type as U"

[MichaReiser]

Makes sense to me