mirror of https://github.com/astral-sh/ruff
f67236b932
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: ```py 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. |
||
|---|---|---|
| .. | ||
| annotations | ||
| assignment | ||
| binary | ||
| boolean | ||
| boundness_declaredness | ||
| call | ||
| class | ||
| comparison | ||
| comprehensions | ||
| conditional | ||
| dataclasses | ||
| declaration | ||
| diagnostics | ||
| directives | ||
| doc | ||
| exception | ||
| expression | ||
| function | ||
| generics | ||
| ide_support | ||
| import | ||
| literal | ||
| loops | ||
| narrow | ||
| regression | ||
| scopes | ||
| shadowing | ||
| snapshots | ||
| stubs | ||
| subscript | ||
| suppressions | ||
| type_compendium | ||
| type_of | ||
| type_properties | ||
| type_qualifiers | ||
| unary | ||
| with | ||
| .mdformat.toml | ||
| async.md | ||
| attributes.md | ||
| bidirectional.md | ||
| classes.md | ||
| cycle.md | ||
| decorators.md | ||
| del.md | ||
| deprecated.md | ||
| descriptor_protocol.md | ||
| enums.md | ||
| exhaustiveness_checking.md | ||
| final.md | ||
| implicit_type_aliases.md | ||
| instance_layout_conflict.md | ||
| intersection_types.md | ||
| invalid_syntax.md | ||
| known_constants.md | ||
| literal_promotion.md | ||
| mdtest_config.md | ||
| mdtest_custom_typeshed.md | ||
| metaclass.md | ||
| mro.md | ||
| named_tuple.md | ||
| overloads.md | ||
| paramspec.md | ||
| pep613_type_aliases.md | ||
| pep695_type_aliases.md | ||
| properties.md | ||
| protocols.md | ||
| public_types.md | ||
| statically_known_branches.md | ||
| sys_platform.md | ||
| sys_version_info.md | ||
| t_strings.md | ||
| terminal_statements.md | ||
| ty_extensions.md | ||
| typed_dict.md | ||
| union_types.md | ||
| unpacking.md | ||
| unreachable.md | ||