Janno/quadratic tc

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,35 @@ 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 =
+      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 ->
+        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
+       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 +631,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 +646,31 @@ 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.
+                 Keep higher-priority failures from the continuation, e.g.
+                 [ReachedLimit], so iterative deepening can continue. *)
+              tclCASE (fk' e) >>= function
+              | Fail ie as fail ->
+                begin match fst e with
+                | NoProgress ->
+                  let ie = merge_exceptions e ie in
+                  begin match fst ie with
+                  | NoProgress -> fk ie
+                  | _ -> kont (Fail ie)
+                  end
+                | _ -> 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 +691,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 +715,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 +730,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 +776,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 +1016,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"))

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

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

test-suite/success/Typeclasses.v

@@ -311,6 +311,55 @@ 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 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.
 
   Class TestClass2 := {}.