Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dcreager merged 8 commits into from
Nov 24, 2025
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7e98d29
allow missing types in specialize_recursive
dcreager Nov 20, 2025
465d53f
don't normalize specialization mdtest display
dcreager Nov 20, 2025
a4226fd
single tautologies
dcreager Nov 20, 2025
8a0b4c2
allow Never ≤ T ≤ object constraints
dcreager Nov 20, 2025
de391ee
fall back on default for unconstrained typevars
dcreager Nov 20, 2025
07636a4
Merge remote-tracking branch 'origin/main' into dcreager/unconstraine…
dcreager Nov 21, 2025
d3b2fd4
added TODOs
dcreager Nov 24, 2025
c1aeca1
Merge remote-tracking branch 'origin/main' into dcreager/unconstraine…
dcreager Nov 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()))

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -168,27 +171,31 @@ from typing import Any
# fmt: off

def constrained_by_gradual[T: (Base, Any)]():
Copy link
Contributor

@carljm carljm Nov 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a weird case, and the more I think about it, the weirder it gets.

I think the principles of constrained type var should probably be:

  1. We should always solve to one of the constrained types (or to Unknown or Any). This is the core invariant of constrained type variables.
  2. If the constraints don't allow us to narrow down to a single constrained type, but could allow multiple, we should prefer the subtype, if one constrained type is a subtype of the other. For example, for def f[T: (Base, Sub)](x: T) we should prefer solving f(typed_as sub) to Sub rather than Base, even though both solutions would be possible.
  3. If multiple constrained types are possible, and neither is a subtype of the other, we should... do what? Fall back to the typevar default?

But if we agree with these principles, then we can never solve this constrained type var to Base, because any set of constraints that would allow us to solve to Base would also allow solving to Any, therefore we can't narrow it down to one of the choices.

mypy seems to just always solve such a typevar to Any. (Mypy doesn't support typevar defaults, nor distinguish Any vs Unknown, so I can't really experiment with how it handles fallback-to-default.)

pyright also always solves to Any, unless the typevar is totally unconstrained, in which case it falls back to the typevar default (which I've explicitly specified to be Base in this example, but could also just implicitly be Unknown.) I'm not sure how pyright decides that f(base) or f(sub) should be Any rather than "the typevar default", given that those calls are compatible with either constrained type.

pyrefly does the same thing you originally did here (always solve to a fully static type), which I'm pretty sure is wrong. It fails both the promises of a constrained type var and of the gradual guarantee, and I suspect will cause false positive errors in practice (the fact that pyright and mypy both prefer solving to Any strengthens this intuition.) If the Any constrained type means "there is really some static type here, but we don't know what it is" (imagine its an Unknown from a failed import of a type), then it's wrong to solve to some arbitrary fully static type, because we don't know that's what the constrained type was "supposed" to be - and it could cause a lot of cascading errors.

(I think it's fine to punt all of this, but I will suggest some different TODOs below based on this analysis.)

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But if we agree with these principles, then we can never solve this constrained type var to Base, because any set of constraints that would allow us to solve to Base would also allow solving to Any, therefore we can't narrow it down to one of the choices.

Is it worth trying to consider which materializations of Any are valid specializations? If Base is a valid specialization but no subtypes are (if that were to violate some other requirement of the specialization), then the Any could not materialize to anything that would take precedence according to your rule (2).

Copy link
Contributor

@carljm carljm Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that makes sense! So if we have a lower bound of Base (e.g. because we got a call that provided an instance of Base as argument for this typevar), then we can solve to Base because it must be the most precise option.

# 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()))
Comment on lines +175 to +176
Copy link
Contributor

@carljm carljm Nov 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would expect this to solve to the typevar default, in this case Unknown. What information allows us to pick Base over Any here? (If we are picking between Base and Any, I think Any is probably the better choice in practice, and is what mypy/pyright choose, but I'm not sure what heuristic they are using.)

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What information allows us to pick Base over Any here?

This is a side effect of the change I added from this discussion #21414 (comment). If there are multiple solutions, my original plan was to produce the union of them. But I don't think that's correct, so instead we either:

  • find a single specialization that satisfies all of the solutions, or
  • return None to indicate an ambiguous result.

Here, the constraint of Any can materialize to any type T = *, and still satisfy ConstraintSet.always(). The constraint of Base only satisfies the constraint set when T = Base. The intersection of those two solutions is T = Base, and so that's what we return.

# 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)))
Comment on lines 177 to +179
Copy link
Contributor

@carljm carljm Nov 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here I think either Any or Unknown (typevar default) would be reasonable choices?

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep, this one already has Any as the TODO

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(This one I think the right TODO is Any not Unknown because here we are now explicitly saying that T can be any type, as opposed to not having said anything about what T can be. The latter clearly should fall back on the default. The former I don't think should.)

# 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]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Unrelated]
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)))
Comment on lines +191 to 192
Copy link
Contributor

@carljm carljm Nov 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as above cases, I think this should also solve to Any or Unknown

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added TODO

# 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)))
Comment on lines +198 to 199
Copy link
Contributor

@carljm carljm Nov 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And again here.

Copy link
Member Author

@dcreager dcreager Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added TODO

# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Sub]
Expand Down Expand Up @@ -288,15 +295,15 @@ 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()))

# 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)))
Expand Down
31 changes: 17 additions & 14 deletions crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
```

Expand Down Expand Up @@ -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))
```

Expand Down Expand Up @@ -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))
```

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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))
```

Expand All @@ -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))
```

Expand All @@ -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))
```
2 changes: 1 addition & 1 deletion crates/ty_python_semantic/src/types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8306,7 +8306,7 @@ impl<'db> KnownInstanceType<'db> {
write!(
f,
"ty_extensions.Specialization{}",
specialization.normalized(self.db).display_full(self.db)
specialization.display_full(self.db)
)
}
KnownInstanceType::UnionType(_) => f.write_str("types.UnionType"),
Expand Down
Loading
Loading