From e687fe41f5dfdd13a151cf0616e8c009a325ce28 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 11:20:48 +0200 Subject: [PATCH 1/6] Add output test for #21044 --- test-suite/output/bug_21044.out | 13 +++++++++++++ test-suite/output/bug_21044.v | 13 +++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 test-suite/output/bug_21044.out create mode 100644 test-suite/output/bug_21044.v diff --git a/test-suite/output/bug_21044.out b/test-suite/output/bug_21044.out new file mode 100644 index 000000000000..c74e92567e55 --- /dev/null +++ b/test-suite/output/bug_21044.out @@ -0,0 +1,13 @@ +Debug: +Calling typeclass resolution with flags: depth = ∞,unique = false,fail = false +Debug: 1: looking for (A ?P ?Q) with backtracking +Debug: 1.1: simple apply a on (A ?P ?Q), 0 subgoal(s) +Debug: 2: looking for (B ?P ?Q) with backtracking +File "./output/bug_21044.v", line 13, characters 6-15: +Error: Illegal application (Non-functional construction): +The expression "foo ?a ?b" of type "True" +cannot be applied to the term + "?y" : "?T" + + +coqc exited with code 1 diff --git a/test-suite/output/bug_21044.v b/test-suite/output/bug_21044.v new file mode 100644 index 000000000000..2f8f53c63b99 --- /dev/null +++ b/test-suite/output/bug_21044.v @@ -0,0 +1,13 @@ +Class A (P Q : Prop) := {}. +Instance a {P Q} : A P Q := {}. +Hint Mode A - - : typeclass_instances. + +Class B (P Q : Prop) := {}. +Hint Mode B - ! : typeclass_instances. + +Axiom foo : forall {P Q}, + A P Q -> + B P Q -> True. + +Set Typeclasses Debug Verbosity 1. +Check foo _ _ _ _ _ _ _ _ _ _ _. From 6e3771b2e01b4f475049ff41915e4836c9a5d5d9 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 12:05:55 +0200 Subject: [PATCH 2/6] Fix accounting and focussing of goals stuck due to Hint Mode --- tactics/class_tactics.ml | 67 ++++++++++++++++++++++++++++++---------- 1 file changed, 51 insertions(+), 16 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1cc0ed55cd60..26ab293c87ab 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -498,6 +498,9 @@ module Search = struct exception ReachedLimit exception NoApplicableHint exception StuckGoal + (* Internal marker used when all remaining goals are postponed and none + can make progress. It is reported as [NoApplicableHint] at the boundary. *) + exception NoProgress (** ReachedLimit has priority over NoApplicableHint to handle iterative deepening: it should fail when no hints are applicable, @@ -545,7 +548,7 @@ module Search = struct let pr_internal_exception ie = match fst ie with | ReachedLimit -> str "Proof-search reached its limit." - | NoApplicableHint -> str "Proof-search failed." + | NoApplicableHint | NoProgress -> str "Proof-search failed." | StuckGoal | NonStuckFailure -> str "Proof-search got stuck." | e -> CErrors.iprint ie @@ -573,7 +576,7 @@ module Search = struct | IsNonStuckFailure -> str "stuck failure" - let pr_search_goal sigma (glid, ev, status, _) = + let pr_search_goal sigma (glid, ev, status, _, _) = str"Goal " ++ int glid ++ str" evar: " ++ Evar.print ev ++ str " status: " ++ pr_goal_status status let pr_search_goals sigma = @@ -583,8 +586,25 @@ module Search = struct let open Pp in let open Proofview in let open Proofview.Notations in - let rec fixpoint progress tacs stuck fk = - let next (glid, ev, status, tac) tacs stuck = + (* Tactics are created for the initial goals, but postponing stuck goals + and backtracking can reorder the proofview. Refocus by evar, not by + the current goal position. *) + let focus_goal ev tac = + tclEVARMAP >>= fun sigma -> + match Evarutil.advance sigma ev with + | None -> tclUNIT () + | Some ev -> + Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in + match CList.index_opt Evar.equal ev gls with + | None -> tclUNIT () + | Some i -> tclFOCUS ~nosuchgoal:(tclUNIT ()) i i tac + in + (* Count successful goal resolutions. A postponed goal is retried only + after a later success, not merely because progress happened before it + got stuck. *) + let rec fixpoint generation tacs stuck fk = + let next (glid, ev, status, tac, _) tacs stuck = let () = ppdebug 1 (fun () -> str "considering goal " ++ int glid ++ str " of status " ++ pr_goal_status status) @@ -601,8 +621,7 @@ module Search = struct | StuckGoal -> IsStuckGoal | _ -> assert false in - cycle 1 (* Puts the first goal last *) <*> - fixpoint progress tacs ((glid, ev, status, tac) :: stuck) fk (* Launches the search on the rest of the goals *) + fixpoint generation tacs ((glid, ev, status, tac, generation) :: stuck) fk (* Launches the search on the rest of the goals *) | Fail ie -> let () = ppdebug 1 (fun () -> str "Goal " ++ int glid ++ str" has no more solutions, returning exception: " @@ -617,12 +636,24 @@ module Search = struct we backtrack to the next result of tac, etc.... Ultimately if none of the solutions for tac work, we will come back to the failure continuation fk in one of the above cases *) - fixpoint true tacs stuck (fun e -> tclCASE (fk' e) >>= kont) + fixpoint (succ generation) tacs stuck (fun e -> + (* Try the next solution of the current tactic. If there is no + such solution after a no-progress failure, preserve that + failure instead of treating the current goal as newly stuck; + otherwise tactics already known to be stuck get run again. *) + tclCASE (fk' e) >>= function + | Fail _ as fail -> + begin match fst e with + | NoProgress -> tclZERO ~info:(snd e) NoProgress + | _ -> kont fail + end + | next -> kont next) in tclCASE tac >>= kont in tclEVARMAP >>= fun sigma -> let () = ppdebug 1 (fun () -> - let stuck, failed = List.partition (fun (_, _, status, _) -> status = IsStuckGoal) stuck in + let stuck, failed = List.partition (fun (_, _, status, _, _) -> status = IsStuckGoal) stuck in + let progress = List.exists (fun (_, _, _, _, stuck_at) -> stuck_at < generation) stuck in str"Calling fixpoint on : " ++ int (List.length tacs) ++ str" initial goals" ++ str", " ++ int (List.length stuck) ++ str" stuck goals" ++ @@ -643,17 +674,19 @@ module Search = struct we might have other solutions available through fk. *) tclOR (tclUNIT ()) fk | stuck -> - if progress then fixpoint false stuck [] fk + let retry, stuck = List.partition (fun (_, _, _, _, stuck_at) -> stuck_at < generation) stuck in + if not (List.is_empty retry) then fixpoint generation retry stuck fk else (* No progress can be made on the stuck goals arising from this resolution, try a different solution on the non-stuck goals, if any. *) begin - tclORELSE (fk (NoApplicableHint, Exninfo.null)) + tclORELSE (fk (NoProgress, Exninfo.null)) (fun (e, info) -> let () = ppdebug 1 (fun () -> int (List.length stuck) ++ str " remaining goals left, no progress, calling continuation failed") in + let e = match e with NoProgress -> NoApplicableHint | e -> e in (* We keep the stuck goals to display to the user *) if best_effort then - let stuckgls, failedgls = List.partition (fun (_, _, status, _) -> + let stuckgls, failedgls = List.partition (fun (_, _, status, _, _) -> match status with | IsStuckGoal -> true | IsNonStuckFailure -> false @@ -665,7 +698,7 @@ module Search = struct (* We shelve the stuck goals but we keep the non-stuck failures in the goal list. This is for compat with Coq 8.12 but might not be the wisest choice in the long run. *) - let to_shelve = List.map (fun (glid, ev, _, _) -> ev) stuckgls in + let to_shelve = List.map (fun (glid, ev, _, _, _) -> ev) stuckgls in let () = ppdebug 1 (fun () -> str "Shelving subgoals: " ++ prlist_with_sep spc Evar.print to_shelve) @@ -680,10 +713,12 @@ module Search = struct It might happen that an initial goal is solved during the resolution of another goal, hence the `tclUNIT` in case there is no goal for the tactic to apply anymore. *) let tacs = List.map2_i - (fun i gls tac -> (succ i, Proofview.drop_state gls, IsInitial, tclFOCUS ~nosuchgoal:(tclUNIT ()) 1 1 tac)) + (fun i gls tac -> + let ev = Proofview.drop_state gls in + (succ i, ev, IsInitial, focus_goal ev tac, 0)) 0 gls tacs in - fixpoint false tacs [] (fun (e, info) -> tclZERO ~info e) <*> + fixpoint 0 tacs [] (fun (e, info) -> tclZERO ~info e) <*> pr_goals (str "Result goals after fixpoint: ") @@ -724,7 +759,7 @@ module Search = struct let derivs = path_derivate env info.search_cut name in let pr_error ie = ppdebug 1 (fun () -> - let idx = if fst ie == NoApplicableHint then pred !idx else !idx in + let idx = match fst ie with NoApplicableHint | NoProgress -> pred !idx | _ -> !idx in let header = pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ @@ -964,7 +999,7 @@ module Search = struct match e with | ReachedLimit -> Tacticals.tclFAIL ~info (str"Proof search reached its limit") - | NoApplicableHint -> + | NoApplicableHint | NoProgress -> Tacticals.tclFAIL ~info (str"Proof search failed" ++ (if Option.is_empty depth then mt() else str" without reaching its limit")) From 500871febcbdfd3c386ace5a1478df60a96ac536 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 12:38:43 +0200 Subject: [PATCH 3/6] Add iterative deepening test case --- test-suite/success/Typeclasses.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index de500e0606a6..40ac86b58ba4 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -311,6 +311,32 @@ Module IterativeDeepening. End IterativeDeepening. +Module IterativeDeepening2. + + Set Typeclasses Iterative Deepening. + + Inductive T := t. + Class A (x : T) := a : nat. + Class B (x : T) := b : nat. + Class C := c : nat. + Class D := d : nat. + + #[export] Hint Mode B ! : typeclass_instances. + + #[export] Instance A_bad {x} : A x := 0. + #[export] Instance A_good : C -> A t := fun _ => 1. + #[export] Instance C_from_D : D -> C := fun _ => 2. + #[export] Instance D_inst : D := 3. + #[export] Instance B_t : B t := 4. + + Goal {x : T & A x * B x}. + Proof. + eexists; split; typeclasses eauto 4. + Qed. + +End IterativeDeepening2. + + Module AxiomsAreNotInstances. Class TestClass2 := {}. From 6d1a6e69a0c0be2bd163530ed98efe6a872eb193 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 12:50:44 +0200 Subject: [PATCH 4/6] Fix iterative deepening test case --- tactics/class_tactics.ml | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 26ab293c87ab..a39effc705fd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -590,15 +590,25 @@ module Search = struct and backtracking can reorder the proofview. Refocus by evar, not by the current goal position. *) let focus_goal ev tac = + let rec find_goal ev i = function + | [] -> None + | gl :: gls -> + if Evar.equal ev (Proofview.drop_state gl) then Some i + else find_goal ev (succ i) gls + in tclEVARMAP >>= fun sigma -> match Evarutil.advance sigma ev with | None -> tclUNIT () | Some ev -> Unsafe.tclGETGOALS >>= fun gls -> - let gls = CList.map Proofview.drop_state gls in - match CList.index_opt Evar.equal ev gls with - | None -> tclUNIT () - | Some i -> tclFOCUS ~nosuchgoal:(tclUNIT ()) i i tac + match find_goal ev 1 gls with + | None -> + let () = ppdebug 1 (fun () -> + str "Goal evar " ++ Evar.print ev ++ + str " is no longer focused but remains undefined") + in + tclZERO StuckGoal + | Some i -> tclFOCUS ~nosuchgoal:(tclZERO StuckGoal) i i tac in (* Count successful goal resolutions. A postponed goal is retried only after a later success, not merely because progress happened before it @@ -640,11 +650,18 @@ module Search = struct (* Try the next solution of the current tactic. If there is no such solution after a no-progress failure, preserve that failure instead of treating the current goal as newly stuck; - otherwise tactics already known to be stuck get run again. *) + otherwise tactics already known to be stuck get run again. + Keep higher-priority failures from the continuation, e.g. + [ReachedLimit], so iterative deepening can continue. *) tclCASE (fk' e) >>= function - | Fail _ as fail -> + | Fail ie as fail -> begin match fst e with - | NoProgress -> tclZERO ~info:(snd e) NoProgress + | NoProgress -> + let ie = merge_exceptions e ie in + begin match fst ie with + | NoProgress -> tclZERO ~info:(snd ie) NoProgress + | _ -> kont (Fail ie) + end | _ -> kont fail end | next -> kont next) From c64cb2b13c14be5d1740e3398a45e4e7c1a82185 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 14:46:28 +0200 Subject: [PATCH 5/6] Add backtracking test case --- test-suite/success/Typeclasses.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 40ac86b58ba4..61b796e8edb8 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -336,6 +336,29 @@ Module IterativeDeepening2. End IterativeDeepening2. +Module BacktrackAfterNoProgress. + + Class A (x : unit) := a : nat. + Class B (x : unit) := b : nat. + Class C (x : unit) := c : nat. + + Local Hint Mode B ! : typeclass_instances. + + Local Instance A_any {x} : A x := 0. + Local Instance C_any {x} : C x | 0 := 0. + Local Instance C_tt : C tt | 10 := 1. + Local Instance B_tt : B tt := 0. + + (* The first [C x] solution leaves [x] undefined, so [B x] is + postponed by its mode. After solving [A x], search retries [B x] + and must still backtrack to the second [C x] solution. *) + Goal { x : unit & C x * B x * A x }. + Proof. + eexists; repeat split; typeclasses eauto. + Qed. + +End BacktrackAfterNoProgress. + Module AxiomsAreNotInstances. From 0c6e5feee2a5c31191fe335f1bd0904eace2a402 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 18 May 2026 14:57:58 +0200 Subject: [PATCH 6/6] Fix backtracking test case --- tactics/class_tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a39effc705fd..8518e167a531 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -659,7 +659,7 @@ module Search = struct | NoProgress -> let ie = merge_exceptions e ie in begin match fst ie with - | NoProgress -> tclZERO ~info:(snd ie) NoProgress + | NoProgress -> fk ie | _ -> kont (Fail ie) end | _ -> kont fail