Fix coroutine witness trait solving with NLL-derived facts - #160940
Fix coroutine witness trait solving with NLL-derived facts#160940dingxiangfei2009 wants to merge 1 commit into
Conversation
When checking auto-trait bounds like Send on coroutine witness types, the solver creates independent placeholder regions for each bound variable in the witness binder. Even when NLL proves these regions are equal or have outlives relationships, the solver cannot use this information, causing false Send/Sync failures. This commit adds a mechanism to propagate NLL region constraints into the trait solver via an enriched ParamEnv: 1. Extract SCC data from NLL during mir_borrowck 2. Stall coroutine auto-trait goals using BorrowckPendingScc typing mode 3. Re-evaluate stalled goals inside mir_borrowck with an enriched ParamEnv containing CoroutineWitnessRegionConstraints 4. The solver merges these constraints into forall placeholder assumptions, enabling proof of region obligations Gated behind -Zdxf flag (requires -Znext-solver). Fixes rust-lang#87425, rust-lang#126551, rust-lang#71723, rust-lang#126550, rust-lang#149235. Partially addresses rust-lang#79648, rust-lang#110338.
8978a85 to
a20a467
Compare
|
The job Click to see the possible cause of the failure (guessed by this bot) |
|
☔ The latest upstream changes (presumably #158436) made this pull request unmergeable. Please resolve the merge conflicts by rebasing. |
|
It seems that you're trying to solve the same problem as assumptions on binders addresses? |
|
@adwinwhite Hmm problems in the same category yeah, but I found that there are tests in the patch that shows AoB cannot prove certain auto trait bounds, see AoB also has a small unsoundness issue which incorrectly dismissed outstanding higher ranked outlive constraints, see I mostly would see this as addition to AoB. There are bounds that AoB cannot prove alone and there are bounds which NLL data must work with AoB together to prove because WF facts are essential. |
When checking auto-trait bounds like Send on coroutine witness types, the solver creates independent placeholder regions for each bound variable in the witness binder. Even when NLL proves these regions are equal or have outlives relationships, the solver cannot use this information, causing Send/Sync bound checks to fail. But we can do better.
This commit adds a mechanism to propagate NLL region constraints into the trait solver via an enriched
ParamEnv. The rough idea is as follows.mir_borrowck, maximise the outlive relations in SCC and compute the quotient by relating lifetimes in the saved locals. This becomes the NLL facts that can "hydrate" theParamEnvper coroutine in the re-evaluation step.BorrowckPendingScctyping modemir_borrowckwith an enriched ParamEnv containingCoroutineWitnessRegionConstraints, the NLL facts that we mentioned.Gated behind -Zdxf flag, which is totally not serious and mostly requires -Znext-solver.
Fixes #87425, #126551, #71723, #126550, #149235.
Partially addresses #79648, #110338.
This is a throw-away patch, it exists only for discussion. Do not expect timely updates to keep it working or mergeable. Sorry!
I used LLMs to
RUSTC_LOGs to reconstruct proof trees