[ty] Only normalize constraint bounds for display #21516
+79
−41
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
dcreager
requested review from
AlexWaygood,
carljm and
sharkdp
as code owners
Diagnostic diff on typing conformance testsNo changes detected when running ty on typing conformance tests ✅ |
|
carljm
approved these changes
Nov 18, 2025
sharkdp
approved these changes
Nov 19, 2025
| ) { | ||
| // These might seem redundant with the intersection check below, since `a → b` means that | ||
| // `a ∧ b = a`. But we are not normalizing constraint bounds, and these clauses help us | ||
| // identity constraints that are identical besides e.g. ordering of union/intersection |
Contributor
There was a problem hiding this comment.
Suggested change
| // identity constraints that are identical besides e.g. ordering of union/intersection | |
| // identify constraints that are identical besides e.g. ordering of union/intersection |
Comment on lines
+2312
to
+2317
| if left_constraint.implies(db, right_constraint) { | ||
| self.add_single_implication(left_constraint, right_constraint); | ||
| } | ||
| if right_constraint.implies(db, left_constraint) { | ||
| self.add_single_implication(right_constraint, left_constraint); | ||
| } |
Contributor
There was a problem hiding this comment.
The explanation above seems to imply that we could (should?) return early here? Because if a → b always implies a ∧ b = a, then the code below would otherwise add two additional a → b implications and one a → a implication, both of which seem unnecessary?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We were previously normalizing the upper and lower bounds of each constraint when constructing constraint sets. Like in #21463, this was for conflated reasons: It made constraint set displays nicer, since we wouldn't render multiple constraints with obviously equivalent bounds. (Think
T ≤ A & BandT ≤ B & A) But it was also useful for correctness, since prior to #21463 we were (trying to) add the full transitive closure to a constraint set's BDD, and normalization gave a useful reduction in the number of nodes in a typical BDD.Now that we don't store the transitive closure explicitly, that second reason is no longer relevant. Our sequent map can store that full transitive closure much more efficiently than the expanded BDD would have. This helps fix some false positives on #20933, where we're seeing some (incorrect, need to be fixed, but ideally not blocking this effort) assignability failures between a type and its normalization.
Normalization is still useful for display purposes, and so we do normalize the upper/lower bounds before building up our display representation of a constraint set BDD.