Diagnostics ICE when replaying proof trees with next-solver

[VicenteGusmao]

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.