[ty] Better handling of "derived information" in constraint sets

[dcreager]

This saga began with a regression in how we handle constraint sets where a typevar is constrained by another typevar, which #21068 first added support for:

def mutually_constrained[T, U]():
    # If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well.
    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
    static_assert(given_int.implies_subtype_of(T, int))

While working on #21414, I saw a regression in this test, which was strange, since that PR has nothing to do with this logic! The issue is that something in that PR made us instantiate the typevars T and U in a different order, giving them differently ordered salsa IDs. And importantly, we use these salsa IDs to define the variable ordering that is used in our constraint set BDDs. This showed that our "mutually constrained" logic only worked for one of the two possible orderings. (We can — and now do — test this in a brute-force way by copy/pasting the test with both typevar orderings.)

The underlying bug was in our ConstraintSet::simplify_and_domain method. It would correctly detect (U ≤ T ≤ U) ∧ (U ≤ int), because those two constraints affect different typevars, and from that, infer T ≤ int. But it wouldn't detect the equivalent pattern in (T ≤ U ≤ T) ∧ (U ≤ int), since those constraints affect the same typevar. At first I tried adding that as yet more pattern-match logic in the ever-growing simplify_and_domain method. But doing so caused other tests to start failing.

At that point, I realized that simplify_and_domain had gotten to the point where it was trying to do too much, and for conflicting consumers. It was first written as part of our display logic, where the goal is to remove redundant information from a BDD to make its string rendering simpler. But we also started using it to add "derived facts" to a BDD. A derived fact is a constraint that doesn't appear in the BDD directly, but which we can still infer to be true. Our failing test relies on derived facts — being able to infer that T ≤ int even though that particular constraint doesn't appear in the original BDD. Before, simplify_and_domain would trace through all of the constraints in a BDD, figure out the full set of derived facts, and add those derived facts to the BDD structure. This is brittle, because those derived facts are not universally true! In our example, T ≤ int only holds along the BDD paths where both T = U and U ≤ int. Other paths will test the negations of those constraints, and on those, we shouldn't infer T ≤ int. In theory it's possible (and we were trying) to use BDD operators to express that dependency...but that runs afoul of how we were simultaneously trying to remove information to make our displays simpler.

So, I ripped off the band-aid. simplify_and_domain is now only used for display purposes. I have not touched it at all, except to remove some logic that is definitely not used by our Display impl. Otherwise, I did not want to touch that house of cards for now, since the display logic is not load-bearing for any type inference logic.

For all non-display callers, we have a new sequent map data type, which tracks exactly the same derived information. But it does so (a) without trying to remove anything from the BDD, and (b) lazily, without updating the BDD structure.

So the end result is that all of the tests (including the new regressions) pass, via a more efficient (and hopefully better structured/documented) implementation, at the cost of hanging onto a pile of display-related tech debt that we'll want to clean up at some point.

[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

No ecosystem changes detected ✅

No memory usage changes detected ✅

[sharkdp]

Not a full review yet, but I might not have enough time to review the rest today, so sending two initial questions.

[sharkdp]

Just curious about the terminology here. The special thing about the equivalent term in logic seems to be that there can be multiple "consequents" on the right hand side. But none of the cases listed below seem to have that form?

[dcreager]

The representation does allow for multiple consequents (there is a Vec in the single_implications and pair_implications maps). But we never construct one directly, since each sequent that we construct corresponds to an implication where we infer one fact from something else we already know. But when that single-consequent sequent is folded in to the rest of the SequentMap, it might get combined with other sequents that have the same lhs, producing a combined sequent with multiple consequents. (And the consequents of a sequent are ORed, so if there's multiple derived facts that we can infer from the same set of given facts, we can choose which of them we need to use.)

[codspeed-hq]

CodSpeed Performance Report

Merging #21463 will not alter performance

_{Comparing dcreager/ordering-bug (a87c3d9) with main (e4a32ba)}

Summary

✅ 22 untouched
⏩ 30 skipped¹

Footnotes

1. 30 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩

[sharkdp]

Fantastic in-code documentation and writeup. I have the feeling that I understood roughly what is going on and it seems to make a lot of sense to me, but I'll also admit that my understanding is most certainly not deep enough to provide any meaningful input on the overall design. But all of the individual pieces seem consistent to me.