Typeclass resolution regression from #22037: goals with no applicable hint fail eagerly, losing solutions found via later unifications (breaks fiat-crypto)

[JasonGross]

[Investigation and write-up by Claude (Fable 5) via Claude Code, on behalf of @JasonGross.]

Description of the problem

Since #22037 ("Fix goal-tactic association in typeclass search", merged as b53550e), typeclass resolution fails eagerly when a goal has no applicable hint: the failure backtracks into earlier goals and the remaining goals are never attempted. But a goal with no applicable hint at that point of the search may still become solvable once the remaining goals instantiate its evars by unification, so this loses solutions.

This broke fiat-crypto on rocq/rocq-prover:dev (see the detailed investigation in mit-plv/fiat-crypto#2356): in src/Bedrock/End2End/X25519/MontgomeryLadder.v, elaborating ladderstep_body spawns 9 interdependent typeclass evars; the ?field_parameters : FieldParameters goal has no directly applicable hint (the instance's discharged hint carries stale secvars — on all rocq versions, hint dbs are byte-identical between good/bad commits), and is only solvable through unification against frep25519 : FieldRepresentation, i.e. through a later goal of the same resolution. Before #22037 the (buggy) goal-tactic association accidentally ran the remaining goals in the failed goal's slot, so resolution succeeded; with the association fixed, Set Typeclasses Debug shows the FieldRepresentation goal is never attempted (0 occurrences of looking for FieldRepresentation vs 1 on the parent commit), and all 9 evars are reported unresolved. Reverting #22037 on 2274c5dc56 restores the fiat-crypto build.

The NonStuckFailure deferral mechanism does not apply because it is conditioned on all_mode_match, which is false for classes without declared Hint Modes (class_tactics.ml: let all_mode_match = List.for_all (fun m -> m != NoMode) modes).

Small Rocq file to illustrate the semantic gap

The following distills the dependency shape. It fails both before and after #22037 (before #22037 it only succeeds when the goal ordering happens to shuffle favorably, as in the fiat-crypto case), and arguably should succeed: resolving ?b with b0 determines ?a := a0.

Class A : Type := {}.
Class B (a : A) : Type := {}.
Axiom a0 : A.
Axiom b0 : B a0.
#[local] Existing Instance b0.
Definition body {a : A} {b : @B a} : nat := 0.
Definition foo := body.
(* Error: Cannot infer the implicit parameter a of body whose type is "A"
   (no type class instance found). *)

A proposed fix (PR to follow) is to defer the first NoApplicableHint failure of a goal like a non-stuck failure while other goals remain in out-of-order mode, retrying it after further progress through the generation machinery introduced by #22037. With that fix, both the example above and fiat-crypto (verified against the full dep stack: MontgomeryLadder.v compiles) work, the test suite passes (including output/bug_21044.v and the success/Typeclasses.v additions from #22037), and the goal-tactic association and anti-quadratic behavior of #22037 are preserved.

Version of Rocq where this bug occurs

master at 2274c5d (and any commit ≥ b53550e); first shipped in rocq/rocq-prover:dev images between 2026-06-15 (c87d4f7338, works) and 2026-07-01 (2274c5dc56, fails).

Last version of Rocq where the bug did not occur

For the fiat-crypto regression: master at c87d4f7 (parent window of #22037). The distilled example above also fails on older versions (it requires the new deferral to succeed).

[Janno]

Here is a reproducer of the bug that works before #22037 but not after:

Class Q := {}.
#[local] Instance q0 : Q := {}.

Class P (u : unit) := {}.
#[local] Hint Mode P - : typeclass_instances.
#[local] Instance p_any {u : unit} `{Q} : P u := {}.

Class A := {}.
Class B (u : unit) (p : P u) (a : A) := {}.

Definition a0 : A := Build_A.
#[local] Instance b0 : B tt p_any a0 := Build_B tt p_any a0.

Axiom foo : forall {u : unit} {p : P u} {a : A} {b : B u p a}, True.

Definition test : True := foo.

My analysis in #22228 (comment) seems to be correct. To fix this the right way would be to not fail as eagerly. But we will break at least hott and probably a few other developments in CI that had to work around TC search failing eagerly on goals that appear in the type of later goals and could be instantiated that way (even without any hints for their own class).

Interestingly enough, I don't think there should even be TC searches for field_parameter (or a in the reproducer). The only scenario in which this can currently happen is in the pretyper. Hints applied by TC search itself do not expose parameters used in other parameters as TC goals. (This is a huge problem sometimes but that's besides the point.)

[Janno]

Interestingly enough, I don't think there should even be TC searches for field_parameter (or a in the reproducer). The only scenario in which this can currently happen is in the pretyper. Hints applied by TC search itself do not expose parameters used in other parameters as TC goals. (This is a huge problem sometimes but that's besides the point.)

Just to illustrate this point, here's a very slightly changed version that one could reasonably expect to run exactly the same typeclass search as the example above. However, this one works both before and after #22037 because the dependently-used parameter is never scheduled as a TC goal during the search.

Class Q := {}.
#[local] Instance q0 : Q := {}.

Class P (u : unit) := {}.
#[local] Hint Mode P - : typeclass_instances.
#[local] Instance p_any {u : unit} `{Q} : P u := {}.

Class A := {}.
Class B (u : unit) (p : P u) (a : A) := {}.

Definition a0 : A := Build_A.
#[local] Instance b0 : B tt p_any a0 := Build_B tt p_any a0.

Existing Class True.
Instance foo {u : unit} {p : P u} {a : A} {b : B u p a} : True := I.

Definition test : True.
Proof.
  apply _.
Qed.