[ty] Only normalize constraint bounds for display #21516
Conversation
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 ✅ |
|
| 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); | ||
| } |
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?
There was a problem hiding this comment.
There are other protections in place against both of those: The single_implications and pair_implications maps now have sets to store all of the consequents, so two copies of a → b will automatically get de-duped, no matter how they're created. And similarly, add_single_implication and add_pair_implication will skip any sequent of the form a → a, a ∧ b → a, or a ∧ b → b, since they are not useful.
Co-authored-by: David Peter <[email protected]>
* origin/main: [ty] Fix flaky tests on macos (#21524) [ty] Add tests for generic implicit type aliases (#21522) [ty] Semantic tokens: consistently add the `DEFINITION` modifier (#21521) Only render hyperlinks for terminals known to support them (#21519) [ty] Keep colorizing `mypy_primer` output (#21515) [ty] Exit with `2` if there's any IO error (#21508) [`ruff`] Fix false positive for complex conversion specifiers in `logging-eager-conversion` (`RUF065`) (#21464) [ty] tighten up handling of subscripts in type expressions (#21503)
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.