Some changes occurred to the core trait solver

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

r? @TaKO8Ki

rustbot has assigned @TaKO8Ki.
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

r? lcnr

this is a surprising failure, while revisiting goals can get different results with proof trees, instantiating the response generally shouldn't fail 🤔 can you provide some more detail how this test ends up returning some canonical state we cannot instantiate. What is the constraint we get when replying the proof tree but not while actually proving the goal

please generally move fix #issuenum into the PR description instead of the title

@rustbot author

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

The failure is not in the original proof of the goal, but in the diagnostics-only replay of a stored CanonicalState.

We save a canonical state while proving the goal, and later try to replay that state after more trait solving has happened in the same infcx. At that point, the saved var_values no longer necessarily unify with the current orig_values, so instantiating the replayed state can fail even though the original goal evaluation itself completed normally.

For this testcase, the ICE only happens with -Znext-solver=globally, and only while reconstructing nested goals from proof trees for error reporting.

I have not yet isolated the exact replay mismatch for this testcase, i.e. the specific constraint that is present during replay but not during the original proof, but I can instrument that next if that would be useful.

I have also moved the #issuenum from the title to the PR description.

@rustbot ready

We save a canonical state while proving the goal, and later try to replay that state after more trait solving has happened in the same infcx. At that point, the saved var_values no longer necessarily unify with the current orig_values, so instantiating the replayed state can fail even though the original goal evaluation itself completed normally.

This is a bit incorrect. We usually unify the var_values from the query response with the original values when the goal evaluation succeeds, to apply what we have learned from the goal evaluation. But in this case, the goal has failed so we haven't unified them before instantiating the nested goals for proof tree to make diagnostics.

What happens in the problematic code is the following:

We have a failed root goal for<T> T: PartialEq to emit fulfillment error so we try to instantiate it within proof tree.

But as there aren't any orig value for T at the beginning when we have canonicalized it, we insert a fresh ty var for it in L325.

But this inserts a new ty var in the infcx's current universe rather than the universe of var kind bound to that canonical var value, which is a HR as being in for<T>

So, the error is created while trying to unify the ty var from root universe to the binder's universe and I guess we should fix fresh_var_for_kind_with_span to create variable in the relevant universe.

so this is caused by a universe error 🤔 yeah, that's an annoying problem, so we should instantiate the canonical state and between that and unifying the var_values should we create the infer vars 🤔

unsure how to impl this as we don't support instantiating a response without guessing having a var_value guess first. I guess we could create infer vars which are just in the MAX_UNIVERSE. I think this shouldn't blow up anything

Ahh, that makes sense — thanks for the clarification.

You're right that my previous explanation was off.

So the core issue seems to be that fresh_var_for_kind_with_span is creating inference variables in the wrong universe for these higher-ranked canonical vars, which then leads to a universe mismatch during unification.

For possible fixes, I see two options:

• Adjust fresh_var_for_kind_with_span to create variables in the correct universe (more principled)
• Or create fresh vars in MAX_UNIVERSE in this diagnostics-only path (more pragmatic)

I can try prototyping either approach. Do you have a preference for which direction better fits the solver design?

• Adjust fresh_var_for_kind_with_span to create variables in the correct universe (more principled)

hard to do as with the current setup we need to crate the variables before we enter create these new universes. so the second alternative should be easier

in case you are using an LLM to generate/cleanup your messages, please don't. try to state your current understanding in your own words, otherwise it's hard to figure out your current understanding and what I actually need to respond to. It also makes it hard to know whether it's worth it to correct cases where the perspective/framing is slightly off. Even if writing it yourself is less structured or clear, that's still preferable to me. idk if there's a more complete writeup i can point u to here

Okay, I'll keep my comments more direct.

I'll try to implement the second approach.

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.