[ty] Distinguish "unconstrained" from "constrained to any type" (#21539)

Before, we would collapse any constraint of the form `Never ≤ T ≤
object` down to the "always true" constraint set. This is correct in
terms of BDD semantics, but loses information, since "not constraining a
typevar at all" is different than "constraining a typevar to take on any
type". Once we get to specialization inference, we should fall back on
the typevar's default for the former, but not for the latter.

This is much easier to support now that we have a sequent map, since we
need to treat `¬(Never ≤ T ≤ object)` as being impossible, and prune it
when we walk through BDD paths, just like we do for other impossible
combinations.
This commit is contained in:
Douglas Creager
2025-11-24 15:23:09 -05:00
committed by GitHub
parent d379f3826f
commit 7e277667d1
5 changed files with 162 additions and 86 deletions

View File

@@ -22,8 +22,10 @@ from ty_extensions import ConstraintSet, generic_context
# fmt: off
def unbounded[T]():
# revealed: ty_extensions.Specialization[T@unbounded = object]
# revealed: ty_extensions.Specialization[T@unbounded = Unknown]
reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.always()))
# revealed: ty_extensions.Specialization[T@unbounded = object]
reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, object)))
# revealed: None
reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.never()))
@@ -88,6 +90,7 @@ that makes the test succeed.
from typing import Any
def bounded_by_gradual[T: Any]():
# TODO: revealed: ty_extensions.Specialization[T@bounded_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@bounded_by_gradual = object]
reveal_type(generic_context(bounded_by_gradual).specialize_constrained(ConstraintSet.always()))
# revealed: None
@@ -168,12 +171,16 @@ from typing import Any
# fmt: off
def constrained_by_gradual[T: (Base, Any)]():
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Unknown]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.always()))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = object]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.always()))
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, object)))
# revealed: None
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.never()))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Base)))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
@@ -181,14 +188,14 @@ def constrained_by_gradual[T: (Base, Any)]():
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Super]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Super)))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Super]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Super, T, Super)))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = object]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Sub, T, object)))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Sub]
@@ -288,7 +295,7 @@ class Unrelated: ...
# fmt: off
def mutually_bound[T: Base, U]():
# revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = object]
# revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = Unknown]
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.always()))
# revealed: None
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.never()))
@@ -296,7 +303,7 @@ def mutually_bound[T: Base, U]():
# revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = Base]
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, U, T)))
# revealed: ty_extensions.Specialization[T@mutually_bound = Sub, U@mutually_bound = object]
# revealed: ty_extensions.Specialization[T@mutually_bound = Sub, U@mutually_bound = Unknown]
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, T, Sub)))
# revealed: ty_extensions.Specialization[T@mutually_bound = Sub, U@mutually_bound = Sub]
reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, T, Sub) & ConstraintSet.range(Never, U, T)))

View File

@@ -66,12 +66,15 @@ def _[T]() -> None:
reveal_type(ConstraintSet.range(Base, T, object))
```
And a range constraint with _both_ a lower bound of `Never` and an upper bound of `object` does not
constrain the typevar at all.
And a range constraint with a lower bound of `Never` and an upper bound of `object` allows the
typevar to take on any type. We treat this differently than the `always` constraint set. During
specialization inference, that allows us to distinguish between not constraining a typevar (and
therefore falling back on its default specialization) and explicitly constraining it to any subtype
of `object`.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@_ = *)]
reveal_type(ConstraintSet.range(Never, T, object))
```
@@ -156,7 +159,7 @@ cannot be satisfied at all.
```py
def _[T]() -> None:
# revealed: ty_extensions.ConstraintSet[never]
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ *)]
reveal_type(~ConstraintSet.range(Never, T, object))
```
@@ -654,7 +657,7 @@ def _[T]() -> None:
reveal_type(~ConstraintSet.range(Never, T, Base))
# revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_)]
reveal_type(~ConstraintSet.range(Sub, T, object))
# revealed: ty_extensions.ConstraintSet[never]
# revealed: ty_extensions.ConstraintSet[(T@_ ≠ *)]
reveal_type(~ConstraintSet.range(Never, T, object))
```
@@ -811,7 +814,7 @@ def f[T]():
# "domain", which maps valid inputs to `true` and invalid inputs to `false`. This means that two
# constraint sets that are both always satisfied will not be identical if they have different
# domains!
always = ConstraintSet.range(Never, T, object)
always = ConstraintSet.always()
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(always)
static_assert(always)
@@ -846,11 +849,11 @@ from typing import Never
from ty_extensions import ConstraintSet
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(Never, T, T))
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(T, T, object))
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(T, T, T))
```
@@ -862,11 +865,11 @@ as shown above.)
from ty_extensions import Intersection
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(Never, T, T | None))
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(Intersection[T, None], T, object))
# revealed: ty_extensions.ConstraintSet[always]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar = *)]
reveal_type(ConstraintSet.range(Intersection[T, None], T, T | None))
```
@@ -877,8 +880,8 @@ constraint set can never be satisfied, since every type is disjoint with its neg
from ty_extensions import Not
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[never]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar ≠ *)]
reveal_type(ConstraintSet.range(Intersection[Not[T], None], T, object))
# revealed: ty_extensions.ConstraintSet[never]
# revealed: ty_extensions.ConstraintSet[(T@same_typevar ≠ *)]
reveal_type(ConstraintSet.range(Not[T], T, object))
```