[ty] Update "constraint implication" relation to work on constraints between two typevars #21068
+82
−11
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
It's possible for a constraint to mention two typevars. For instance, in the body of
the baseline constraint set would be
(T ≤ S) ∧ (S ≤ int). That is,Smust specialize to some subtype ofint, andTmust specialize to a subtype of the type thatSspecializes 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 ≤ intmust always hold:This did not require major changes to the implementation of
implies_subtype_of. That method already relies on how oursimplifyanddomainmethods 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 ≤ SandS ≤ something, orS ≤ Tandsomething ≤ S. In those cases, transitivity lets us add a new derived constraint thatT ≤ somethingorsomething ≤ T, respectively. Having done that, our existingimplies_subtype_oflogic finds and takes into account that derived constraint.