[ty] ~T should never be assignable to T

[AlexWaygood]

Summary

Currently we do not emit an error on this code:

from ty_extensions import Not

def f[T](x: T, y: Not[T]) -> T:
    x = y
    return x

But we should do! ~T should never be assignable to T.

This fixes a small regression introduced in 14fe122#diff-8049ab5af787dba29daa389bbe2b691560c15461ef536f122b1beab112a4b48aR1443-R1446, where a branch that previously returned false was replaced with a branch that returns C::always_satisfiable -- the opposite of what it used to be! The regression occurred because we didn't have any tests for this -- so I added some tests in this PR that fail on main. I only spotted the problem because I was going through the code of has_relation_to_impl with a fine toothcomb for #20602 😄

[github-actions]

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

[github-actions]

mypy_primer results

No ecosystem changes detected ✅
No memory usage changes detected ✅

[sharkdp]

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?

[AlexWaygood]

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?

[AlexWaygood]

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

[carljm]

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.

[AlexWaygood]

Right, I think that makes sense

[AlexWaygood]

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

[dcreager]

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.

[dcreager]

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.