trait_solver: Reject canonical responses with placeholder universe leaks - #160955
trait_solver: Reject canonical responses with placeholder universe leaks#160955Dnreikronos wants to merge 5 commits into
Conversation
Cover opaque returns of `impl for<T> Trait<T>` under -Zassumptions-on-binders so proof-tree replay no longer ICEs on placeholder universe mismatches.
Proof-tree visitors previously treated instantiate_nested_goals failure as a successful visit via VisitorResult::output(), which is Continue for ControlFlow. CoerceVisitor must Break instead so coerce_unsized rejects inapplicable candidate replay rather than treating it as a valid unsizing path.
|
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
|
r? @folkertdev rustbot has assigned @folkertdev. Use Why was this reviewer chosen?The reviewer was selected based on:
|
|
r? types |
This comment was marked as resolved.
This comment was marked as resolved.
|
r? @BoxyUwU for assumptions on binders stuff |
|
|
|
I don't understand how this differs from #159725. Are these PRs not both handling the case of placeholder types/consts in canonical responses resulting in universe errors? I think that in general we don't really want to be complicating the trait solver for I don't understand what about this test case is made worse by -Zassumptions-on-binders. Can you write a bit about what goals we're proving and what binders we have and what the involved region constraints are and their associated rewriting steps? That'll help me figure out whether there's some other solution we can do here or if we should just wontfix this for the time being |
|
Sup, @BoxyUwU :)! I still pushed this one because the AOB ICE looks different ( I made apply fallible because I don't want to put a placeholder into a var that can't see it. The query never notices. Canonicalization dumps both sides in the root universe, leak check is looking at that, and only when we instantiate again do we have the same For the AOB test we're proving The panic is imo applying that is wrong. I also don't want to twist the solver around |
Fixes #160802
-Zassumptions-on-bindersplus animpl for<T> Trait<T>RPIT was ICEing in proof-tree replay whenunify_query_var_valueshit.unwrap()on a Sorts error for the same binder placeholder living in two universes. Imo that unwrap was always a bit cursed on the diagnostics path, idk why we kept trusting it this long.Canonical response/state apply is fallible now and turns those leaks into
NoSolutioninstead of panicking. Region-only placeholders don't block valid region lowering. Also madeCoerceVisitorBreak when nested candidate replay fails, since Continue was treating a failed instantiate as "unsizing ok" (btwVisitorResult::outputis Continue forControlFlow, easy to miss). Added the issue repro plus a few universe-leak regressions.Fyi the
prev_universeproof-tree fix is already on main and I kept it. Irl I'd rather get this in asap than bike-shed the diagnostics wording further, but ltm if you'd rather the failed replay surface louder than a quietNoSolution.