Skip to content

[ty] ~T should never be assignable to T #20606

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
merged 1 commit into from
Oct 2, 2025
Merged

[ty] ~T should never be assignable to T #20606

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 14 additions & 0 deletions crates/ty_python_semantic/resources/mdtest/generics/legacy/functions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -522,3 +522,17 @@ age, name = team.employees[0]
reveal_type(age) # revealed: Age
reveal_type(name) # revealed: Name
```

## `~T` is never assignable to `T`

```py
from typing import TypeVar
from ty_extensions import Not

T = TypeVar("T")

def f(x: T, y: Not[T]) -> T:
x = y # error: [invalid-assignment]
y = x # error: [invalid-assignment]
return x
```
11 changes: 11 additions & 0 deletions crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -537,3 +537,14 @@ def _(x: int):
# TODO: this should be `tuple[C, int]` as well, once we support implicit `self`
reveal_type(C().implicit_self(x)) # revealed: tuple[Unknown, int]
```

## `~T` is never assignable to `T`

```py
from ty_extensions import Not

def f[T](x: T, y: Not[T]) -> T:
x = y # error: [invalid-assignment]
y = x # error: [invalid-assignment]
return x
```
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 @@ -1562,7 +1562,7 @@ impl<'db> Type<'db> {
(Type::Intersection(intersection), Type::NonInferableTypeVar(_))
if intersection.negative(db).contains(&target) =>
{
ConstraintSet::from(true)
ConstraintSet::from(false)
Copy link
Contributor

@sharkdp sharkdp Sep 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I'm slightly surprised that we need these branches at all. Shouldn't the union/intersection branches take care of this, if T <: T is modeled correctly?

Also, is the statement "~T is never assignable to T" correct if T could specialize to Any? Or do we not have to take this case into account, for some reason?

Copy link
Member Author

Choose a reason for hiding this comment

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

I'm slightly surprised that we need these branches at all. Shouldn't the union/intersection branches take care of this, if T <: T is modeled correctly?

Yes -- ideally we'd have the NonInferrableTypeVar branches below the Union and Intersection branches. Then we wouldn't need these branches at all, as you say. Unfortunately, however, value-constrained TypeVars make this quite hard, as they require special handling with regards to unions:

ruff/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md

Lines 227 to 257 in 3f640da

A constrained fully static typevar is assignable to the union of its constraints, but not to any of
the constraints individually. None of the constraints are subtypes of the typevar, though the
intersection of all of its constraints is a subtype of the typevar.
```py
from ty_extensions import Intersection
def constrained[T: (Base, Unrelated)](t: T) -> None:
reveal_type(is_assignable_to(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Base)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Base | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_assignable_to(T, Sub | Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_assignable_to(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Super)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Base)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Sub)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(T, Super | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Base | Unrelated)) # revealed: ty_extensions.ConstraintSet[always]
reveal_type(is_subtype_of(T, Sub | Unrelated)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Super | Unrelated, T)) # revealed: ty_extensions.ConstraintSet[never]
reveal_type(is_subtype_of(Intersection[Base, Unrelated], T)) # revealed: ty_extensions.ConstraintSet[always]

Also, is the statement "~T is never assignable to T" correct if T could specialize to Any? Or do we not have to take this case into account, for some reason?

Hmm, interesting question. I think that also calls into doubt the validity of this pre-existing branch -- if the TypeVar could be solved to Any, it should not be considered a subtype of itself:

ruff/crates/ty_python_semantic/src/types.rs

Lines 1568 to 1576 in 3f640da

// Two identical typevars must always solve to the same type, so they are always
// subtypes of each other and assignable to each other.
//
// Note that this is not handled by the early return at the beginning of this method,
// since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive.
(
Type::NonInferableTypeVar(lhs_bound_typevar),
Type::NonInferableTypeVar(rhs_bound_typevar),
) if lhs_bound_typevar == rhs_bound_typevar => ConstraintSet::from(true),

I wonder if this is something that @dcreager's work on constraint sets could help with? If the relation is TypeRelation::Subtyping, we could possibly return a constraint set from these branches that indicates that self is a subtype of target only if neither self nor target is solved to Any?

Copy link
Member Author

@AlexWaygood AlexWaygood Sep 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I wonder if this is something that @dcreager's work on constraint sets could help with? If the relation is TypeRelation::Subtyping, we could possibly return a constraint set from these branches that indicates that self is a subtype of target only if neither self nor target is solved to Any?

But that doesn't really make sense, of course, because these are non-inferable type variables -- type variables from the perspective of inside a function or class body... I think this does lead to the conclusion that T cannot be a subtype of T (where T is a non-inferable type variable); it can only be assignable to T. No matter what the bounds or constraints on a type variable are, it could always be specialised to Any, so you can't really ever conclude that a non-inferable type variable is ever a subtype of (or disjoint from) anything, I don't think

Copy link
Contributor

Choose a reason for hiding this comment

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

I don't think we need to account for the possibility that a typevar is specialized to Any here. The key is that it's the same typevar, so it would have to be specialized to the same Any in both usages -- which is really the same as saying it's specialized to some unknown type (which is already what we were accounting for). But since it's the same type for both occurrences of T, the conclusions here still apply.

Copy link
Member Author

Choose a reason for hiding this comment

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

Right, I think that makes sense

Copy link
Member Author

Choose a reason for hiding this comment

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

so... the conclusion from Carl's comment is that the logic in this PR is correct?

Copy link
Member

Choose a reason for hiding this comment

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

I don't think we need to account for the possibility that a typevar is specialized to Any here. The key is that it's the same typevar, so it would have to be specialized to the same Any in both usages

Right, I'd even reword this slightly to say that typevar inference will never infer a gradual type for a typevar. (A typevar can be specialized to Unknown if we don't infer anything for it, and it has no default, but I consider that different than explicitly infering a gradual type for it.)

I'm slightly surprised that we need these branches at all. Shouldn't the union/intersection branches take care of this, if T <: T is modeled correctly?

The current way we're handling assignability of typevars is very brittle and dependent on these kinds of hacks, because of "rounding error" that's introduced by the early conversions of the assignability checks of union/intersection elements into a true/false value. #20093 is working on using constraint sets to model the assignability of a typevar, which will allow us to correctly model when e.g. each element of a union is assignable "sometimes", but in a way that combines to "always" when you merge them together. That will hopefully remove the need for these match arms completely. But having the mdtest here will be good to avoid a regression when that lands.

}

// Two identical typevars must always solve to the same type, so they are always
Expand Down
Loading