trait solver: Capture binder region constraints while relating#157984
trait solver: Capture binder region constraints while relating#157984Dnreikronos wants to merge 4 commits into
Conversation
|
r? @mejrs rustbot has assigned @mejrs. Use Why was this reviewer chosen?The reviewer was selected based on:
|
This comment has been minimized.
This comment has been minimized.
f411fec to
d78cef7
Compare
|
r? @lcnr |
|
r? BoxyUwU |
|
|
| } | ||
| } | ||
|
|
||
| let resolve_region = |r: I::Region| match r.kind() { |
There was a problem hiding this comment.
why resolve regions?
| } | ||
| ty::Invariant => { | ||
| region_constraints.push(RegionConstraint::RegionOutlives(a, b)); | ||
| region_constraints.push(RegionConstraint::RegionOutlives(b, a)); |
There was a problem hiding this comment.
is it possible to call infcx.register_solver_region_constraint here instead of building a list and manually propagating them all upwards?
There was a problem hiding this comment.
yeah, i think you're right. imo regions should call infcx.register_solver_region_constraint directly when -Zassumptions-on-binders is on, and use sub_regions / equate_regions only on the old path.
with that i can drop the *_with_region_constraints plumbing too. fwiw i don't think resolving the regions first is needed anymore unless one of the tests says otherwise.
There was a problem hiding this comment.
this logic shouldn't be used under -Zassumptions-on-binders, actually in theory sub_regions probably should ICE under -Zassumptions-on-binders because those region constraints don't really do anything
There was a problem hiding this comment.
or maybe sub_regions should be registering new style region constraints... unsure
There was a problem hiding this comment.
yeah, this is the same issue. i'll make SolverRelating::regions avoid sub_regions / equate_regions under -Zassumptions-on-binders and register the new-style constraints directly instead. imo changing sub_regions itself can be a follow-up if we still want that after this.
This comment has been minimized.
This comment has been minimized.
|
@BoxyUwU fwiw, i think the ci failure is still compatible with your suggestion. the direct registration path lgtm to me, but the current version is probably registering from too many relation contexts. the bad bit seems to be solverrelating::regions(): under -zassumptions-on-binders it always pushes regionoutlives into the solver constraint storage. some of those relation calls happen under enter_forall_with_empty_assumptions, so later placeholder handling has no assumptions to discharge the constraint and we hit the max_universe(...) < u assert. imo the fix is not to go back to manually bubbling a list everywhere. i'd rather keep direct registration, but only in contexts where the solver owns the binder assumptions, or keep the constraints local while relating a binder and pull them out before registering. idk which shape is cleaner yet, but unconditional registration in regions() seems too wide. |
|
follow-up after pushing 0d93b4c: i tried to keep the direct-registration shape, but idk, it still looked too broad in practice. buffering constraints around binder relation did not clear the reported failures for me. imo the safer fix is to keep the region constraints local while relating, then register the collected next-gen constraint only from the solver-owned relation entrypoints. ltm this still follows the direction boxy was pointing at, without letting solverrelating::regions() register constraints from the empty-assumption binder probes. i checked the same failure cases locally:
|
in theory that shouldn't cause us to hit an assert. if we have empty assumptions then we'll rewrite the constraints to i would like to fully understand what's going on with the ICEs when always registering the next gen region constraints :3 can you look more into what's going on there, if you could push the code that causes those ICEs to happen so I can see the CI failure too that would be useful :3 |
|
i looked into the unconditional direct-registration version locally. imo it confirms the failure mode from my earlier guess: the new repro tests pass, but the broader assumptions-on-binders set fails. specifically:
so idk, direct registration from i can push the failing experiment to a separate branch if seeing ci on that exact shape would help, but i'd rather not force-push it over this pr branch since the current version is passing. checked with:
|
|
like I said, I don't understand why it's hitting that assertion 😅 can you explain why that assertion is getting hit. i can't properly evaluate this alternate approach without understanding why the other one doesn't work |
|
The job Click to see the possible cause of the failure (guessed by this bot) |
|
yeah, my bad! i think i explained the empty-assumptions bit too confidently there. i pushed the direct registration version again so ci can show the actual failure: 31be28b idk yet why it ends up at the |
Fixes #157859
The issue repro is a pretty good example of how this slipped through: the principal upcast path looked fixed, but other relation paths could still drop binder-region constraints. Fwiw, I think centralizing this in the relation code is the cleaner move here, instead of chasing every object-upcast call site one by one.
This records NextGen region constraints from normal relation, structural alias equality, and the small goal-returning relation helper used by object candidate code. ReVars keep their concrete outlives edges too, so we don't flatten useful info into plain ambiguity. Added the original issue repro and a projection-bound variant, e.g. the kind of path I'd expect to regress later if this only lived in the principal upcast code.