[ty] Sync vendored typeshed stubs #21715
Merged
+108
−49
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
github-actions
bot
requested review from
AlexWaygood,
MichaReiser,
dcreager and
sharkdp
as code owners
Diagnostic diff on typing conformance testsNo changes detected when running ty on typing conformance tests ✅ |
|
sharkdp
force-pushed
the
typeshedbot/sync-typeshed
branch
from
60b7a85 to
7d79ebd
Compare
|
| Lint rule | Added | Removed | Changed |
|---|---|---|---|
unsupported-base |
1 | 2 | 0 |
| Total | 1 | 2 | 0 |
Member
|
#21744 should fix the macOS CI failure |
dcreager
added a commit
that referenced
this pull request
Dec 3, 2025
…21744) This fixes a non-determinism that we were seeing in the constraint set tests in #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.]
Member
|
Thank you @dcreager!! |
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.
Close and reopen this PR to trigger CI