[ty] Handle nested types when creating specializations from constraint sets (#21530)
#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 = T` we can infer `T = 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`. `lower` and `upper` are 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 `lower` and `upper` _are_ typevars, not when they _contain_ typevars. That distinction is important, since it means the restriction does not affect our expressiveness: we can always rewrite `Never ≤ T ≤ U` (a constraint on `T`) into `T ≤ U ≤ object` (a constraint on `U`). The same is not true of `Never ≤ T ≤ list[U]` — there is no "inverse" of `list` that we could apply to both sides to transform this into a constraint on a bare `U`.
This commit is contained in:
@@ -303,3 +303,33 @@ def mutually_bound[T: Base, U]():
|
||||
# revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = Sub]
|
||||
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, U, Sub) & ConstraintSet.range(Never, U, T)))
|
||||
```
|
||||
|
||||
## Nested typevars
|
||||
|
||||
A typevar's constraint can _mention_ another typevar without _constraining_ it. In this example, `U`
|
||||
must be specialized to `list[T]`, but it cannot affect what `T` is specialized to.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, generic_context
|
||||
|
||||
def mentions[T, U]():
|
||||
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T])
|
||||
# revealed: ty_extensions.ConstraintSet[((T@mentions ≤ int) ∧ (U@mentions = list[T@mentions]))]
|
||||
reveal_type(constraints)
|
||||
# revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
|
||||
reveal_type(generic_context(mentions).specialize_constrained(constraints))
|
||||
```
|
||||
|
||||
If the constraint set contains mutually recursive bounds, specialization inference will not
|
||||
converge. This test ensures that our cycle detection prevents an endless loop or stack overflow in
|
||||
this case.
|
||||
|
||||
```py
|
||||
def divergent[T, U]():
|
||||
constraints = ConstraintSet.range(list[U], T, list[U]) & ConstraintSet.range(list[T], U, list[T])
|
||||
# revealed: ty_extensions.ConstraintSet[((T@divergent = list[U@divergent]) ∧ (U@divergent = list[T@divergent]))]
|
||||
reveal_type(constraints)
|
||||
# revealed: None
|
||||
reveal_type(generic_context(divergent).specialize_constrained(constraints))
|
||||
```
|
||||
|
||||
Reference in New Issue
Block a user