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.

[VicenteGusmao]

Resolved a minor merge conflict. My commit is ready for review.

[VicenteGusmao]

@lcnr, can you please review my code when you have the time? If you need any explanation about some of the code feel free to ask anything.

[lcnr]

sorry for the late review, have been quite busy due to rustweek

View changes since this review

[lcnr]

this function name feels confusing, I'd inline the loop

[VicenteGusmao]

Okay, I'll do that.

[lcnr]

do we have some other method here or could we just name this fresh_var_for_kind

[VicenteGusmao]

You're right, I can change the name to fresh_var_for_kind.

[lcnr]

Suggested change

	fn max_input_universe_for_replay<D, I>(
	// What does this do and why
	fn max_input_universe_for_canonical_state<D, I>(

[VicenteGusmao]

I'll rename this function to the name you suggested and I'm thinking of commenting above it with the following explanation:

Recover the caller-side max input universe for replaying a canonical state.

Proof tree canonical states store universe indices relative to the original max input universe, so replay has to recover that base universe from the current orig_values before recreating placeholders and replay-only fresh vars.

[lcnr]

don't we already have such a visitor? https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/region_constraint/fn.max_universe.html

[VicenteGusmao]

I tried using rustc_type_ir::region_constraint::max_universe here, but
it doesn't match what this replay path needs.

In this case we need the max input universe from when the canonical
state was originally recorded. max_universe looks at the current
resolved contents of orig_values, and after more solving those can
already mention placeholders from later replay work.

That makes it compute a larger base universe than the original one,
which shifts the replayed placeholders and brings back the same mismatch
during instantiation. So I kept a local helper for this path.

[VicenteGusmao]

No worries! I'll see what you have commented on the code.

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