[ty] Add and test when constraint sets are satisfied by their typevars

[dcreager]

This PR adds a new satisfied_by_all_typevar method, which implements one of the final steps of actually using these dang constraint sets. Constraint sets exist to help us check assignability and subtyping of types in the presence of typevars. We construct a constraint set describing the conditions under which assignability holds between the two types. Then we check whether that constraint set is satisfied for the valid specializations of the relevant typevars (which is this new method).

We also add a new ty_extensions.ConstraintSet method so that we can test this method's behavior in mdtests, before hooking it up to the rest of the specialization inference machinery.

[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 ✅

[MichaReiser]

I don't think I understand why T <= Super satisfies T <= Base, given that Super isn't a subtype of Base. Or am I reading this the wrong way around? Or is the Never part important?

[dcreager]

We discussed this sync — the key point is that the implication is in the other direction. (The typevar bounds/constraints need to imply the constraint set being checked.) So here, T must specialize to a subtype of Base. Base is a subtype of Super, so every valid specialization of T is also a subtype of Super. (Technically, this test is in the inferable section, so we only need one valid specialization of T to satisfy the constraint set. In this case, every valid specialization does, so you'll see that this same test also holds down in the non-inferable section.)

[MichaReiser]

I don't think I understand the why but I trust you on this

[dcreager]

This is trying to show that Never is sneaky, especially for inferable typevars. Since T is inferable, we only need one specialization to satisfy the constraint set. Never is a valid specialization, since Never ≤ Base. And Never ≤ Unrelated, so the constraint set is satisfied for the T = Never case. That's enough for an inferable typevar.

The corresponding test in the non-inferable section fails, though, since there we need all valid specializations to satisfy the constraint set. And T = Base is a counter-example where it doesn't.

This tells me that it might help to change the structure of this file? Right now I have inferable/non-inferable as the top-level sections, and different kinds of typevar bounds/constraints as (unlabeled) subsections. Maybe instead I should have "unbounded", "bound", and "constrained" as the top-level sections, to more clearly call out how the behavior is different for inferable vs non-inferable?

[dcreager]

This tells me that it might help to change the structure of this file?

I did this, and added more explanatory comments for each example. Hopefully that helps clarify the logic a bit.

[MichaReiser]

Hmm, same here. Why is Super satisfying the constraint, given that it isn't Base or Unrelated?

[dcreager]

Same as above. This is in inferable position, so we only need one specialization of T to satisfy the constraint set. T = Base does, so the check passes. Down below in the non-inferable section, the check fails, because T = Unrelated is a valid specialization that doesn't satisfy the constraint set.

[MichaReiser]

This is great. Thanks for adding it

[MichaReiser]

Thanks again for taking the time to explain this to me during our phone call. The reasoning in the mdtests make sense to me. Altough I'm still finding the DSL slightly confusing. But maybe that just is because I fail to map it to an example using Python

[MichaReiser]

I'm still somewhat confused by the DSL here but I (maybe?) finally figured out how to read this?

Is my understanding correct that this results in:

Never <= any(Base, Unrelated) <= Super

which is true because Base satisfies this constraint.

And the next example is:

Never < forall(Base, Unrelated) < Super

which is false, because Unrelated doesn't satisfy this constraint.

The part I'm struggling with right now is what a real-world example of static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(inferable=tuple[T])) would look like?

[dcreager]

I'm still somewhat confused by the DSL here but I (maybe?) finally figured out how to read this?

I would formalize it differently, but I think your notation leads to the right understanding:

Is my understanding correct that this results in:

Never <= any(Base, Unrelated) <= Super

which is true because Base satisfies this constraint.

Yes

And the next example is:

Never < forall(Base, Unrelated) < Super

which is false, because Unrelated doesn't satisfy this constraint.

This should use <= instead of < like the first example, but otherwise yes.

The part I'm struggling with right now is what a real-world example of static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(inferable=tuple[T])) would look like?

I'm actually not sure what Python I could write that would result in this check either! We need something that wants to check that an instance of T is assignable to Super. The non-inferable case is easy:

def f[T: (Base, Unrelated)](t: T):
    x: Super = t

But in the T inferable case, we would be invoking this function. And I'm not sure what Python code would lead to a T ≤ Super check.

The problem is that I can't limit myself to implementing these algorithms for constraint set checks that have obvious Python analogues. 😅

[dcreager]

But in the T inferable case, we would be invoking this function. And I'm not sure what Python code would lead to a T ≤ Super check.

Ah maybe via the return type:

def f[T: (Base, Unrelated)]() -> T:
    raise NotImplementedError

x: Super = f()

(Disregard the fact that there is no real function body that we could write that would satisfy that signature!)