[ty] Add mdtests that exercise constraint sets

[dcreager]

This PR adds a new ty_extensions.ConstraintSet class, which is used to expose constraint sets to our mdtest framework. This lets us write a large collection of unit tests that exercise the invariants and rewrite rules of our constraint set implementation.

As part of this, is_assignable_to and friends are updated to return a ConstraintSet instead of a bool, and we implement ConstraintSet.__bool__ to return when a constraint set is always satisfied. That lets us still use static_assert(is_assignable_to(...)), since the assertion will coerce the constraint set to a bool, and also lets us reveal_type(is_assignable_to(...)) to see more detail about whether/when the two types are assignable. That lets us get rid of reveal_when_assignable_to and friends, since they are now redundant with the expanded capabilities of is_assignable_to.

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

[carljm]

Nice!

[carljm]

Why doesn't this union simplify to SubSub <= T <= Super?

[dcreager]

There can be types that satisfy SubSub ≤ T ≤ Super but which aren't comparable to Sub or Base, and which therefore shouldn't be included in the union.

So with just set theory, if the possible values are 0, 1, and 2, you get a type lattice of

   012
01  02  12
 0   1   2
     ∅

Then we might have

SubSub = ∅
Sub    = 1
Base   = 12
Super  = 012

SubSub ≤ T ≤ Base  = {∅, 1, 2, 12}
Sub ≤ T ≤ Super    = {1, 01, 12, 012}

The union should be

(SubSub ≤ T ≤ Base) ∪ (Sub ≤ T ≤ Super) = {∅, 1, 2, 01, 12, 012}

but the simplification you suggest would be

SubSub ≤ T ≤ Super = {∅, 0, 1, 2, 01, 02, 12, 012}

0 and 02 are included in the simplification but not in the actual union.

Translating that into Python, an example problem type would be Super \ Sub*, where Sub* indicates instances of just Sub, but not any of its subclasses. (So in English, the problem type is "instances of Super, or any subclass of Super other than Sub". That type is not in SubSub ≤ T ≤ Base, since it includes Super, which is outside the range. It's also not in Sub ≤ T ≤ Super, because it does not include Sub. But it is in SubSub ≤ T ≤ Super.

[carljm]

Makes sense, thank you! Might be worth recording a short version of this as a comment?

[dcreager]

Done