mirror of https://github.com/astral-sh/ruff
45842cc034
This fixes a non-determinism that we were seeing in the constraint set tests in https://github.com/astral-sh/ruff/pull/21715. In this test, we create the following constraint set, and then try to create a specialization from it: ``` (T@constrained_by_gradual_list = list[Base]) ∨ (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ``` That is, `T` is either specifically `list[Base]`, or it's any `list`. Our current heuristics say that, absent other restrictions, we should specialize `T` to the more specific type (`list[Base]`). In the correct test output, we end up creating a BDD that looks like this: ``` (T@constrained_by_gradual_list = list[Base]) ┡━₁ always └─₀ (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ┡━₁ always └─₀ never ``` In the incorrect output, the BDD looks like this: ``` (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ┡━₁ always └─₀ never ``` The difference is the ordering of the two individual constraints. Both constraints appear in the first BDD, but the second BDD only contains `T is any list`. If we were to force the second BDD to contain both constraints, it would look like this: ``` (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ┡━₁ always └─₀ (T@constrained_by_gradual_list = list[Base]) ┡━₁ always └─₀ never ``` This is the standard shape for an OR of two constraints. However! Those two constraints are not independent of each other! If `T` is specifically `list[Base]`, then it's definitely also "any `list`". From that, we can infer the contrapositive: that if `T` is not any list, then it cannot be `list[Base]` specifically. When we encounter impossible situations like that, we prune that path in the BDD, and treat it as `false`. That rewrites the second BDD to the following: ``` (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ┡━₁ always └─₀ (T@constrained_by_gradual_list = list[Base]) ┡━₁ never <-- IMPOSSIBLE, rewritten to never └─₀ never ``` We then would see that that BDD node is redundant, since both of its outgoing edges point at the `never` node. Our BDDs are _reduced_, which means we have to remove that redundant node, resulting in the BDD we saw above: ``` (Bottom[list[Any]] ≤ T@constrained_by_gradual_list ≤ Top[list[Any]]) ┡━₁ always └─₀ never <-- redundant node removed ``` The end result is that we were "forgetting" about the `T = list[Base]` constraint, but only for some BDD variable orderings. To fix this, I'm leaning in to the fact that our BDDs really do need to "remember" all of the constraints that they were created with. Some combinations might not be possible, but we now have the sequent map, which is quite good at detecting and pruning those. So now our BDDs are _quasi-reduced_, which just means that redundant nodes are allowed. (At first I was worried that allowing redundant nodes would be an unsound "fix the glitch". But it turns out they're real! [This](https://ieeexplore.ieee.org/abstract/document/130209) is the paper that introduces them, though it's very difficult to read. Knuth mentions them in §7.1.4 of [TAOCP](https://course.khoury.northeastern.edu/csu690/ssl/bdd-knuth.pdf), and [this paper](https://par.nsf.gov/servlets/purl/10128966) has a nice short summary of them in §2.) While we're here, I've added a bunch of `debug` and `trace` level log messages to the constraint set implementation. I was getting tired of having to add these by hands over and over. To enable them, just set `TY_LOG` in your environment, e.g. ```sh env TY_LOG=ty_python_semantic::types::constraints::SequentMap=trace ty check ... ``` [Note, this has an `internal` label because are still not using `specialize_constrained` in anything user-facing yet.] |
||
|---|---|---|
| .. | ||
| resources | ||
| src | ||
| tests | ||
| Cargo.toml | ||
| build.rs | ||
| mdtest.py | ||
| mdtest.py.lock | ||