trait solver: Capture binder region constraints while relating

[Dnreikronos]

View all comments

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.

[rustbot]

r? @mejrs

rustbot has assigned @mejrs.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

Why was this reviewer chosen?

The reviewer was selected based on:

• Owners of files modified in this PR: compiler, types
• compiler, types expanded to 73 candidates
• Random selection from 21 candidates

[mejrs]

r? @lcnr

[lcnr]

r? BoxyUwU

[rustbot]

BoxyUwU is currently at their maximum review capacity.
They may take a while to respond.

[Dnreikronos]

@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.

[Dnreikronos]

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:

• x.py check compiler/rustc_type_ir compiler/rustc_next_trait_solver
• x.py test tests/ui/assumptions_on_binders/alias_outlives.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-1.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-2.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-3.rs tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.rs tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.rs
• x.py test tidy

[BoxyUwU]

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.

in theory that shouldn't cause us to hit an assert. if we have empty assumptions then we'll rewrite the constraints to false and (eventually) get an error 🤔 if we were doing this in a enter_forall_without_assumptions it would make sense to me we get ICEs. though I wouldn't expect it to be due to the max_universe(..) < n assertion 🤔 I would expect it to be due to missing entries in the assumptions list in the InferCtxt.

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

[Dnreikronos]

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:

• alias_outlives.rs hits the max_universe(infcx, constraint.clone()) < u assertion
• the type_relation_binders_inside_solver-* tests either ice or reject code that should pass

so idk, direct registration from solverrelating::regions() still feels too broad to me. lgtm in principle, but only if we can keep it out of binder probes with empty assumptions. ltm the current local-collection shape is the safer boundary for now: collect while relating, then register from the solver-owned relation entrypoints.

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:

• x.py check compiler/rustc_type_ir compiler/rustc_next_trait_solver
• x.py test tests/ui/assumptions_on_binders/alias_outlives.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-1.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-2.rs tests/ui/assumptions_on_binders/type_relation_binders_inside_solver-3.rs tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.rs tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.rs
• x.py test tidy

[BoxyUwU]

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

[Dnreikronos]

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 max_universe assert instead of just rewriting to false, so ltm the useful next step is to let ci capture the full logs on this exact shape.

[BoxyUwU]

@rustbot author

gonna do that while you figure out what's going on there, if you're having trouble we can chat about it over zulip and try figure it out together

[rustbot]

Reminder, once the PR becomes ready for a review, use @rustbot ready.

[Dnreikronos]

@rustbot ready

[BoxyUwU]

im having a hard time understanding what motivated this change 🤔 can you give an example with:

• an alias outlives assumption
• the alias being matched against it
• what the region constraints we get are
• why those region constraints are mishandled in some way if we dont do this line of code
• what region constraints we get instead if we do this line of code

View changes since the review

[Dnreikronos]

fyi I checked this with a local trace on tests/ui/assumptions_on_binders/alias_outlives.rs, and I think I have a better handle on what is happening now.

The passing case has this env assumption:

<T as AliasHaver>::Assoc: 'static

To prove T::Assoc: for<'a> Trait<'a>, we enter the binder and prove T::Assoc: Trait<'!a_u1>. Selecting the blanket impl introduces an impl lifetime var, '?0 in my trace.

Before this normalization, the relevant constraint was:

RegionOutlives('!1_...ReqTrait::'a, '?0)
RegionOutlives('?0, '!1_...ReqTrait::'a)
AliasTyOutlivesViaEnv(<T as AliasHaver>::Assoc: '?0)
PlaceholderTyOutlives(!0, '?0)

So the alias being matched is <T as AliasHaver>::Assoc, but its outlives target is '?0, not the placeholder directly.

After normalization, the same constraint becomes:

RegionOutlives('!1_...ReqTrait::'a, '!1_...ReqTrait::'a)
RegionOutlives('!1_...ReqTrait::'a, '!1_...ReqTrait::'a)
AliasTyOutlivesViaEnv(<T as AliasHaver>::Assoc: '!1_...ReqTrait::'a)
PlaceholderTyOutlives(!0, '!1_...ReqTrait::'a)

Then matching against <T as AliasHaver>::Assoc: 'static gives:

RegionOutlives('static, '!1_...ReqTrait::'a)

For the failing case, where the env only has <T as AliasHaver>::Assoc: 'a, it gives:

RegionOutlives('a/#0, '!1_...ReqTrait::'a)

and that stays unsatisfied, which is what we want.

Without this normalization, the trace keeps the alias target as '?0, and REGIONCK_ENV_PASS fails with:

error[E0283]: type annotations needed: cannot satisfy `for<'a> <T as AliasHaver>::Assoc: Trait<'a>`

My read is that alias/env matching gets here before the later region closure pass. We already know '?0 == '!a_u1 in the same And branch, but unless we make that visible first, the alias outlives path sees a current-universe var instead of the placeholder shape it needs.

idk if this is the nicest layer for it, but the trace made the motivation a lot clearer to me. ltm if you want the raw trace bits and I can paste them too.

[BoxyUwU]

What actually goes wrong when we have these constraints:

RegionOutlives('!1_...ReqTrait::'a, '?0)
RegionOutlives('?0, '!1_...ReqTrait::'a)
AliasTyOutlivesViaEnv(<T as AliasHaver>::Assoc: '?0)
PlaceholderTyOutlives(!0, '?0)

im having a hard time understanding how we go from that to an Ambiguity somewhere. I'm assuming that this is happening in alias_outlives_candidates_from_assumptions when trying to rewrite AliasTyOutlivesViaEnv? I would expect that we get back a RegionOutlives('static, '?0) constraint from that, i don't understand why that would go on to cause problems :3

[Dnreikronos]

yeah, your expectation would be right if <T as AliasHaver>::Assoc: 'static was in the assumptions available here. fyi i traced this again and that's the bit i was missing.

while handling U1, i found that get_placeholder_assumptions(U1) has type_outlives: []. the 'static assumption comes from the root param env, so alias_outlives_candidates_from_assumptions gives Or([]) here instead of RegionOutlives('static, '?0).

the rewrite then tries to move AliasTyOutlivesViaEnv(...: '?0) out of U1, but PlaceholderReplacer only replaces placeholders, not revars. '?0 stays in U1, the max_universe(candidate) < u check fails, and that adds Ambiguity. btw, there are still candidates that could work once this gets back to the root, but evaluate_solver_constraint sees the ambiguous branch and nothing that's already true in U1, so the whole Or becomes ambiguous before any of them get there.

normalization changes '?0 to the placeholder it's equated with first. PlaceholderReplacer can bind that, which lets the alias-outlives candidate escape U1. once it gets back to the root, the full env is there and the 'static assumption can be matched.

so imo your reasoning is right. if RegionOutlives('static, '?0) existed here, the later closure should handle it. that edge just never gets produced at this point because the root assumption isn't available yet.

idk if normalization is the nicest layer for this tbh, it does feel a little blunt to me. imo doing it before the rewrite still makes sense though, since that's where the equality and the type-outlives constraint are together in the same And. ltm if you want the raw trace bits :)

[BoxyUwU]

the max_universe(candidate) < u check fails, and that adds Ambiguity

what do you mean by this? can you link me to the place that adds the ambiguity? as far as I'm aware we only add ambiguity when we have None assumptions for a binder (or when handling AliasTyOutlivesViaEnv during coherence)

evaluate_solver_constraint sees the ambiguous branch and nothing that's already true in U1, so the whole Or becomes ambiguous before any of them get there.

this also seems problematic to me 😅 I don't think that evaluating OR(ambig, 'a: 'b) should result in ambig that feels wrong 🤔 I would probably expect us to just keep that as is. I guess this isn't technically wrong but it does make us wildly conservative wrt considering things to be ambiguous when they might still be fine...

I would probably like us to fix this too 🤔

the rewrite then tries to move AliasTyOutlivesViaEnv(...: '?0) out of U1, but PlaceholderReplacer only replaces placeholders, not revars

I think this is something we should "just" fix 🤔 we should be rewriting <T as Trait>::Assoc: '?x_u1 to for<'a> <T as Trait>::Assoc: 'a when rewriting things in u1. Or more generally, we should never be rewriting type outlives constraints to different type outlives in the same universe. The max_universe should either be lowered or they should now be region outlives constraints

as a fix this is slightly conservative 🤔 which is unfortunate, but I would need to spend a lot more time thinking about this before adding some form of "resolving regions" (or normalization as you've called it).

[BoxyUwU]

thx for your comment by the way it's cleared up a lot to me about things here (so much stuff is scuffed from my original impl of -Zassumptions-on-binders! lol!)

[rustbot]

This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

[Dnreikronos]

@BoxyUwU fyi I rebased this after #154989 landed and resolved the conflict with the old structural relating code.

I kept the behavior from the earlier review. Under -Zassumptions-on-binders, SolverRelating::regions registers new solver constraints directly. It does not resolve the regions first, and the temporary *_with_region_constraints plumbing is gone. sub_regions / equate_regions stay on the old path only.

Upstream moved response unification into ResponseRelating, so I ported the same handling there instead of restoring the APIs that #154989 removed. imo that fits the new setup better.

I kept normalize_equated_region_vars for the other thread. Alias/env matching runs before the later region closure, so it needs to see that '?0 and the placeholder are equal inside the same And branch. Without the normalization, the passing AliasHaver::Assoc: 'static case still sees '?0 and ends up ambiguous. After normalization it sees the placeholder, gets the expected 'static outlives edge, and the non-static case still fails.

btw I changed "conjunction" to "the same And branch" in the comment. idk if normalization here is the nicest possible layer, but imo the trace makes the ordering issue pretty convincing.

[BoxyUwU]

@rustbot author

[Dnreikronos]

@rustbot ready