[ty] Handle nested types when creating specializations from constraint sets #21530
+179
−5
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.
#21414 added the ability to create a specialization from a constraint set. It handled mutually constrained typevars just fine, e.g. given
T ≤ int ∧ U = Twe can inferT = int, U = int.But it didn't handle nested constraints correctly, e.g.
T ≤ int ∧ U = list[T]. Now we do! This requires doing a fixed-point "apply the specialization to itself" step to propagate the assignments of any nested typevars, and then a cycle detection check to make sure we don't have an infinite expansion in the specialization.This gets at an interesting nuance in our constraint set structure that @sharkdp has asked about before. Constraint sets are BDDs, and each internal node represents an individual constraint, of the form
lower ≤ T ≤ upper.lowerandupperare allowed to be other typevars, but only if they appear "later" in the arbitary ordering that we establish over typevars. The main purpose of this is to avoid infinite expansion for mutually constrained typevars.However, that restriction doesn't help us here, because only applies when
lowerandupperare typevars, not when they contain typevars. That distinction is important, since it means the restriction does not affect our expressiveness: we can always rewriteNever ≤ T ≤ U(a constraint onT) intoT ≤ U ≤ object(a constraint onU). The same is not true ofNever ≤ T ≤ list[U]— there is no "inverse" oflistthat we could apply to both sides to transform this into a constraint on a bareU.