Fix: WF ICE assumptions on binders

[ssenthilnathan3]

View all comments

Fixes #160293

-Zassumptions-on-binders ICEs because the solver's well_formed_goals passes terms with resolvable inference variables to unnormalized_obligations, which asserts they're already resolved (unlike other callers).

Resolve inference variables before computing WF obligations.

[rustbot]

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

[rustbot]

Thanks for the pull request, and welcome! The Rust Project is excited to review your changes, and you should hear from @adwinwhite (or someone else) some time within the next two weeks.

Please see the contribution instructions for more information. Namely, in order to ensure the minimum review times lag, PR authors and assigned reviewers should ensure that the review label (S-waiting-on-review and S-waiting-on-author) stays updated, invoking these commands when appropriate:

• @rustbot author: the review is finished, PR author should check the comments and take action accordingly
• @rustbot review: the author is ready for a review, this PR will be queued again in the reviewer's queue

Why was this reviewer chosen?

The reviewer was selected based on:

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

[adwinwhite]

@rustbot author

[rustbot]

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

[ssenthilnathan3]

@rustbot review

[adwinwhite]

I think we should look into the callers of enter_forall_with_assumptions and find out why we have unresolved vars there. It should be easy to find out which caller is relevant from the ICE backtrace :>

[ssenthilnathan3]

I think we should look into the callers of enter_forall_with_assumptions and find out why we have unresolved vars there. It should be easy to find out which caller is relevant from the ICE backtrace :>

I think the only caller of enter_forall_with_assumptions is compute_goal, which gets the predicate from enter_canonical (fresh vars). The ICE comes from a nested call deep in the probe:

eager_resolve_vars in evaluate_goal_raw uses opportunistic_resolve_ty_var, so some type vars may escape canonicalization unresolved, get unified later during equating, and then a deeper nested forall visits them in the RawAssumptions visitor.

The fix resolves them in visit_ty/visit_const before computing WF obligations, matching what the debug_assert_eq! in unnormalized_obligations expects.

Let me know if I'm overlooking something here.

[adwinwhite]

I think the only caller of enter_forall_with_assumptions is compute_goal, which gets the predicate from enter_canonical (fresh vars). The ICE comes from a nested call deep in the probe:

How so? ripgrep would show 6 callers. And compute_goal uses resolved vars already since the goal is instantiated from canonical form directly.

[ssenthilnathan3]

I think the only caller of enter_forall_with_assumptions is compute_goal, which gets the predicate from enter_canonical (fresh vars). The ICE comes from a nested call deep in the probe:

How so? ripgrep would show 6 callers. And compute_goal uses resolved vars already since the goal is instantiated from canonical form directly.

Sorry.. you're right, I only checked compute_goal.

And yes, there are 6 callers that could trigger this pattern, but fixing at every caller would be fragile.

The visitor-level resolve matches the convention: callers of unnormalized_obligations should resolve first (same as implied_outlives_bounds.rs:100).

[adwinwhite]

Convention is different in the next solver. We do not expect random unresolved vars here.

[adwinwhite]

Those target_projections come from existential predicates of trait object(ty::Dyn) and the trait object type is normalized here which resolves infer vars. Unsure why we get unresolved infer vars later.

Sorry for being pedantic over this. It's totally fine if you don't want to dig further and we can merge the original fix with a FIXME that we didn't find the source of the unresolved vars.

[ssenthilnathan3]

Those target_projections come from existential predicates of trait object(ty::Dyn) and the trait object type is normalized here which resolves infer vars. Unsure why we get unresolved infer vars later.

Sorry for being pedantic over this. It's totally fine if you don't want to dig further and we can merge the original fix with a FIXME that we didn't find the source of the unresolved vars.

thanks for the direction!! i’d like to dig into this a bit further. i’ll try to trace where the target_projection state changes and probably fine why the infer vars end up unresolved later

[ssenthilnathan3]

@adwinwhite, i did some tracing. the principal eq in the Trait arm resolves the vars in the unification table, but the projection binder still holds the old var ids since the terms are interned/immutable. when the Projection arm runs, those vars are stale but resolvable.

i'll add this explanation to the FIXME and keep the call-site resolution as the fix :)

[adwinwhite]

👍 Good job. We don't need the FIXME then. Just keep current fix and add comments on resolve_if_possible calls.

I think we should add a debug_assert resolve_vars_if_possible(value) = value in enter_forall as it doesn't resolve vars inside. I wonder why that doesn't cause problems before. This can be a follow up.

[adwinwhite]

some final nits :>

View changes since this review

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

[adwinwhite]

Thanks!
@bors r+ rollup

[rust-bors]

📌 Commit 5b3fb6b has been approved by adwinwhite

It is now in the queue for this repository.