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

[dcreager]

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.

[astral-sh-bot]

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

[astral-sh-bot]

mypy_primer results

Changes were detected when running on open source projects

scikit-build-core (https://github.com/scikit-build/scikit-build-core)
+ src/scikit_build_core/build/wheel.py:98:20: error[no-matching-overload] No overload of bound method `__init__` matches arguments
- Found 44 diagnostics
+ Found 45 diagnostics

No memory usage changes detected ✅

[carljm]

Awesome!

[carljm]

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.)

[dcreager]

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).

[carljm]

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.

[carljm]

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.)

[dcreager]

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.

[carljm]

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

[dcreager]

Yep, this one already has Any as the TODO

[dcreager]

(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.)

[carljm]

Pyright and mypy would also solve this to Any. Similar to above, I'm not sure why we'd pick Base over Any here as a solution.

[dcreager]

Added TODO

[carljm]

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

[dcreager]

Added TODO

[carljm]

And again here.

[dcreager]

Added TODO

[carljm]

Mostly just curiosity: is there an important reason why we frame this as ¬C₁ → false rather than C₁ → true? Are these different in some way? The prose here suggests not.

[dcreager]

"C₁ is always true" is true → C₁, not C₁ → true. But given that change, you're right that true → C₁ and ¬C₁ → false are the same thing. One focuses on what is always true, and the other focuses on what's impossible. The focus of this data structure is to track situations that are impossible, so I thought it would be best to frame it with false on the rhs.

Though I guess that means I could go further and rewrite some the examples below ­— for instance C₁ ∧ C₂ → D and C₁ ∧ C₂ ∧ ¬D → false are equivalent in exactly the same way!