Diagnostics ICE when replaying proof trees with next-solver

[VicenteGusmao]

View all comments

When diagnostics replay proof tree state, rebuilding a canonical state can fail to match the current inference state. With -Znext-solver=globally, this could panic while reporting an error, avoiding the panic.

Make proof tree replay fallible in diagnostics and fall back to the current obligation when replay fails. Add a regression test for the higher-ranked PartialEq and PartialOrd case. Fixes #151304.

[rustbot]

Some changes occurred to the core trait solver

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

[rustbot]

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

Why was this reviewer chosen?

The reviewer was selected based on:

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

[BoxyUwU]

r? lcnr

[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

[lcnr]

@rustbot author

[rustbot]

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

[VicenteGusmao]

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.

[VicenteGusmao]

@rustbot ready

[ShoyuVanilla]

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.

rust/compiler/rustc_next_trait_solver/src/canonical/mod.rs

Lines 323 to 336 in c753cef

	// In case any fresh inference variables have been created between `state`
	// and the previous instantiation, extend `orig_values` for it.
	orig_values.extend(
	state.value.var_values.var_values.as_slice()[orig_values.len()..]
	.iter()
	.map(|&arg| delegate.fresh_var_for_kind_with_span(arg, span)),
	);
	let instantiation =
	compute_query_response_instantiation_values(delegate, orig_values, &state, span);
	let inspect::State { var_values, data } = delegate.instantiate_canonical(state, instantiation);
	unify_query_var_values(delegate, param_env, orig_values, var_values, span);

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>

rust/compiler/rustc_trait_selection/src/solve/delegate.rs

Lines 158 to 167 in c753cef

	fn fresh_var_for_kind_with_span(
	&self,
	arg: ty::GenericArg<'tcx>,
	span: Span,
	) -> ty::GenericArg<'tcx> {
	match arg.kind() {
	ty::GenericArgKind::Lifetime(_) => {
	self.next_region_var(RegionVariableOrigin::Misc(span)).into()
	}
	ty::GenericArgKind::Type(_) => self.next_ty_var(span).into(),

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.

[lcnr]

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

[VicenteGusmao]

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?

[lcnr]

• 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

[lcnr]

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

[VicenteGusmao]

Okay, I'll keep my comments more direct.

I'll try to implement the second approach.

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

[VicenteGusmao]

No worries! I have just rebased, but in order to do so I squashed the commits. It was causing merge conflicts in all the previews commits so I thought this was the best approach.

[VicenteGusmao]

@bors r=lcnr

[rust-bors]

@VicenteGusmao: 🔑 Insufficient privileges: not in review users

[VicenteGusmao]

Sorry, this is my first time contributing, wasn't I supposed to do that?

[VicenteGusmao]

@rustbot ready

[lcnr]

please add a few short sentences about this test.

the relevant rust issue, why it failed, and any other potentially useful information

View changes since the review

[VicenteGusmao]

Okay, I'm going to do that.

[lcnr]

now u can approve it urself after adding this short comment

@bors delegate+

[rust-bors]

✌️ @VicenteGusmao, you can now approve this pull request!

If @lcnr told you to "r=me" after making some further change, then please make that change and post @bors r=lcnr.

View changes since this delegation.

[VicenteGusmao]

@bors r=lcnr

[rust-bors]

📌 Commit 1cf12a5 has been approved by lcnr

It is now in the queue for this repository.

[VicenteGusmao]

@lcnr thank you for all the help!