Implementing postponed constraints in TC resolution

A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)

This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).

Add more examples of the semantics of TC resolution with apply in test-suite

Properly catch ModeMatchFailure on calls to map_e*

Add fixed bug 9058 to the test-suite

Close #9058

Add documentation

Fixes after Gaëtan's review.

Main change is to not use exceptions for control-flow

Update tactics/class_tactics.ml

Clearer and more efficient mode mismatch dispatch

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

Remove exninfo argument

6 files changed, 149 insertions, 60 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1dde820075..d68f9271ec 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -303,7 +303,9 @@ let hintmap_of sigma secvars hdc concl =
   | None -> Hint_db.map_none ~secvars
   | Some hdc ->
      if occur_existential sigma concl then
-       Hint_db.map_existential sigma ~secvars hdc concl
+       (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with
+                  | ModeMatch l -> l
+                  | ModeMismatch -> [])
      else Hint_db.map_auto sigma ~secvars hdc concl
 
 let exists_evaluable_reference env = function
@@ -366,11 +368,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
           let st = Hint_db.transparent_state db in
           let flags, l =
             let l =
-              match hdc with None -> Hint_db.map_none ~secvars db
+              match hdc with
+              | None -> Hint_db.map_none ~secvars db
               | Some hdc ->
                   if TransparentState.is_empty st
                   then Hint_db.map_auto sigma ~secvars hdc concl db
-                  else Hint_db.map_existential sigma ~secvars hdc concl db
+                  else match Hint_db.map_existential sigma ~secvars hdc concl db with
+                      | ModeMatch l -> l
+                      | ModeMismatch -> []
             in auto_flags_of_state st, l
           in List.map (fun x -> (Some flags,x)) l)
         (local_db::db_list)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e3f2f18b44..25bd9cc8a8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -309,12 +309,12 @@ let shelve_dependencies gls =
 
 let hintmap_of sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none ~secvars db
+  | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db)
   | Some hdc ->
      fun db ->
-     if Hint_db.use_dn db then (* Using dnet *)
-       Hint_db.map_eauto sigma ~secvars hdc concl db
-     else Hint_db.map_existential sigma ~secvars hdc concl db
+       if Hint_db.use_dn db then (* Using dnet *)
+         Hint_db.map_eauto sigma ~secvars hdc concl db
+      else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
@@ -362,15 +362,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
       | _ -> AllowAll
     with e when CErrors.noncritical e -> AllowAll
   in
-  let hint_of_db = hintmap_of sigma hdc secvars concl in
-  let hintl =
-    List.map_append
-      (fun db ->
-        let tacs = hint_of_db db in
-        let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in
-          List.map (fun x -> (flags, x)) tacs)
-      (local_db::db_list)
-  in
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) ->
       let tac = function
@@ -428,19 +419,40 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
         match repr_hint t with
         | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
         | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
-  in List.map tac_of_hint hintl
+  in
+  let hint_of_db = hintmap_of sigma hdc secvars concl in
+  let hintl = List.map_filter (fun db -> match hint_of_db db with
+      | ModeMatch l -> Some (db, l)
+      | ModeMismatch -> None)
+      (local_db :: db_list)
+  in
+  (* In case there is a mode mismatch in all the databases we get stuck.
+     Otherwise we consider the hints that match.
+     Recall the local database uses the union of all the modes in the other databases. *)
+  if List.is_empty hintl then ModeMismatch
+  else
+    let hintl =
+      CList.map_append
+        (fun (db, tacs) ->
+          let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in
+          List.map (fun x -> (flags, x)) tacs)
+        hintl
+    in
+    ModeMatch (List.map tac_of_hint hintl)
 
 and e_trivial_resolve db_list local_db secvars only_classes env sigma concl =
   let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars hd true only_classes env sigma concl
+    (match e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with
+    | ModeMatch l -> l
+    | ModeMismatch -> [])
   with Not_found -> []
 
 let e_possible_resolve db_list local_db secvars only_classes env sigma concl =
   let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
     e_my_find_search db_list local_db secvars hd false only_classes env sigma concl
-  with Not_found -> []
+  with Not_found -> ModeMatch []
 
 let cut_of_hints h =
   List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
@@ -606,6 +618,7 @@ module Search = struct
   (** In the proof engine failures are represented as exceptions *)
   exception ReachedLimitEx
   exception NoApplicableEx
+  exception StuckClass
 
   (** ReachedLimitEx has priority over NoApplicableEx to handle
       iterative deepening: it should fail when no hints are applicable,
@@ -644,8 +657,11 @@ module Search = struct
            (if backtrack then str" with backtracking"
             else str" without backtracking"));
     let secvars = compute_secvars gl in
-    let poss =
-      e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in
+    match e_possible_resolve hints info.search_hints secvars
+            info.search_only_classes env sigma concl with
+    | ModeMismatch ->
+      Proofview.tclZERO StuckClass
+    | ModeMatch poss ->
     (* If no goal depends on the solution of this one or the
        instances are irrelevant/assumed to be unique, then
        we don't need to backtrack, as long as no evar appears in the goal
@@ -783,6 +799,7 @@ module Search = struct
                 str" possibilities");
          match e with
          | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
+         | (StuckClass,ie) -> Proofview.tclZERO ~info:ie StuckClass
          | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableEx
     in
     if backtrack then aux (NoApplicableEx,Exninfo.null) poss
@@ -841,11 +858,21 @@ module Search = struct
         begin fun gl ->
           search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end
     in
+    let tac_or_stuck sigma gls i =
+      Proofview.tclOR
+       (tac sigma gls i)
+       (function (StuckClass, _) ->
+          if !typeclasses_debug > 1 then
+            Feedback.msg_debug
+              Pp.(str "Proof search got stuck on a constraint, postponing it.");
+           Proofview.tclUNIT ()
+        | (e, ie) -> Proofview.tclZERO ~info:ie e)
+     in
       Proofview.Unsafe.tclGETGOALS >>= fun gls ->
       let gls = CList.map Proofview.drop_state gls in
       Proofview.tclEVARMAP >>= fun sigma ->
       let j = List.length gls in
-      (tclDISPATCH (List.init j (fun i -> tac sigma gls i)))
+      (tclDISPATCH (List.init j (fun i -> tac_or_stuck sigma gls i)))
 
   let fix_iterative t =
     let rec aux depth =
@@ -864,7 +891,7 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac mst ?(unique=false)
+  let eauto_tac_stuck mst ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
     let tac =
@@ -902,6 +929,37 @@ module Search = struct
         Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
       else tac
     in
+    let rec fixpoint step laststuck =
+      tac <*>
+      Proofview.tclEVARMAP >>= fun sigma ->
+      Proofview.Unsafe.tclGETGOALS >>= fun stuck ->
+      begin
+        if !typeclasses_debug > 0 then
+          Feedback.msg_debug Pp.(str "Finished run " ++ int step ++ str " of resolution.");
+        let stuck = List.map Proofview_monad.drop_state stuck in
+        let stuckset = Evar.Set.of_list stuck in
+        let () =
+          if !typeclasses_debug > 1 then
+            if Evar.Set.cardinal stuckset > 0 then
+               Feedback.msg_debug Pp.(str "Stuck goals after resolution: " ++ fnl () ++
+                Pp.prlist_with_sep spc (fun ev -> Printer.pr_goal {it = ev; sigma}) stuck)
+            else Feedback.msg_debug Pp.(str "No stuck goals after resolution.")
+        in
+        if Evar.Set.is_empty stuckset then tclUNIT ()
+        else if Evar.Set.equal laststuck stuckset then
+          begin
+            if !typeclasses_debug > 1 then Feedback.msg_debug Pp.(str "No progress made.");
+            tclUNIT ()
+          end
+        else begin
+          assert(Evar.Set.subset stuckset laststuck);
+          (* Progress was made *)
+          if !typeclasses_debug > 1 then
+            Feedback.msg_debug Pp.(str "Progress made, restarting resolution on stuck goals.");
+          fixpoint (succ step) stuckset
+        end
+      end
+    in
     with_shelf numgoals >>= fun (initshelf, i) ->
     (if !typeclasses_debug > 1 then
        Feedback.msg_debug (str"Starting resolution with " ++ int i ++
@@ -910,24 +968,28 @@ module Search = struct
                              (if only_classes then str " in only_classes mode" else str " in regular mode") ++
                              match depth with None -> str ", unbounded"
                                             | Some i -> str ", with depth limit " ++ int i));
-    tac
+    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+      let gls = CList.map Proofview.drop_state gls in
+      fixpoint 1 (Evar.Set.of_list gls)
 
   let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints =
-    Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints
+    Hints.wrap_hint_warning @@ eauto_tac_stuck mst ?unique ~only_classes ?strategy ~depth ~dep hints
 
   let run_on_evars env evm p tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
     | Some (goals, nongoals) ->
-       let goals =
+       let goalsl =
          if !typeclasses_dependency_order then
            top_sort evm goals
          else Evar.Set.elements goals
        in
+       let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>=
+         fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in
        let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
        let fgoals = Evd.save_future_goals evm in
        let _, pv = Proofview.init evm [] in
-       let pv = Proofview.unshelve goals pv in
+       let pv = Proofview.unshelve goalsl pv in
        try
          (* Instance may try to call this before a proof is set up!
             Thus, give_me_the_proof will fail. Beware! *)
@@ -938,35 +1000,35 @@ module Search = struct
             * with | Proof_global.NoCurrentProof -> *)
            Id.of_string "instance", false
          in
-         let (), pv', (unsafe, shelved, gaveup), _ =
-           Proofview.apply ~name ~poly env tac pv
-         in
-         if not (List.is_empty gaveup) then
-           CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
-         if Proofview.finished pv' then
+         let finish pv' shelved =
            let evm' = Proofview.return pv' in
-           assert(Evd.fold_undefined (fun ev _ acc ->
-                      let okev = Evd.mem evm ev || List.mem ev shelved in
-                      if not okev then
-                        Feedback.msg_debug
-                          (str "leaking evar " ++ int (Evar.repr ev) ++
-                             spc () ++ pr_ev evm' ev);
-                      acc && okev) evm' true);
+             assert(Evd.fold_undefined (fun ev _ acc ->
+                     let okev = Evd.mem evm ev || List.mem ev shelved in
+                     if not okev then
+                       Feedback.msg_debug
+                         (str "leaking evar " ++ int (Evar.repr ev) ++
+                            spc () ++ pr_ev evm' ev);
+                     acc && okev) evm' true);
            let fgoals = Evd.shelve_on_future_goals shelved fgoals in
            let evm' = Evd.restore_future_goals evm' fgoals in
            let nongoals' =
              Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
                  | Some ev' -> Evar.Set.add ev acc
-                 | None -> acc) nongoals (Evd.get_typeclass_evars evm')
+                 | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm')
            in
            let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
            let evm' = Evd.set_typeclass_evars evm' nongoals' in
-           Some evm'
-         else raise Not_found
+             Some evm'
+        in
+        let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in
+        if not (List.is_empty gaveup) then
+          CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
+        if Proofview.finished pv' then finish pv' shelved
+        else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
   let evars_eauto env evd depth only_classes unique dep mst hints p =
-    let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+    let eauto_tac = eauto_tac_stuck mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
     let res = run_on_evars env evd p eauto_tac in
     match res with
     | None -> evd
@@ -996,7 +1058,11 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
   let modes = List.map Hint_db.modes dbs in
   let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in
   let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
-  Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs
+  Proofview.tclIGNORE
+    (Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs)
+    (* Stuck goals can remain here, we could shelve them, but this way
+       the user can use `solve [typeclasses eauto]` to  check there are
+       no stuck goals remaining, or use [typeclasses eauto; shelve] himself. *)
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index dc94e6a6fb..02b24bc145 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -66,4 +66,6 @@ module Search : sig
     -> Hints.hint_db list
     (** The list of hint databases to use *)
     -> unit Proofview.tactic
+    (** Note: there might be stuck goals due to mode declarations
+      remaining even in case of success of the tactic. *)
 end
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index aca6b4734a..9715661985 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -124,7 +124,10 @@ let hintmap_of sigma secvars hdc concl =
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
      if occur_existential sigma concl then
-       (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db)
+       (fun db ->
+          match Hint_db.map_existential sigma ~secvars hdc concl db with
+          | ModeMatch l -> l
+          | ModeMismatch -> [])
      else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 731792e34e..e9ed43e3de 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -499,6 +499,10 @@ let rec subst_hints_path subst hp =
 
 type hint_db_name = string
 
+type 'a with_mode =
+  | ModeMatch of 'a
+  | ModeMismatch
+
 module Hint_db :
 sig
 type t
@@ -507,9 +511,9 @@ val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
-                      (GlobRef.t * constr array) -> constr -> t -> full_hint list
+                      (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
 val map_eauto : evar_map -> secvars:Id.Pred.t ->
-                (GlobRef.t * constr array) -> constr -> t -> full_hint list
+                (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
 val map_auto : evar_map -> secvars:Id.Pred.t ->
                (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val add_one : env -> evar_map -> hint_entry -> t -> t
@@ -528,7 +532,6 @@ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
 val modes : t -> hint_mode array list GlobRef.Map.t
 val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
   t -> 'a -> 'a
-
 end =
 struct
 
@@ -618,8 +621,8 @@ struct
   let map_existential sigma ~secvars (k,args) concl db =
     let se = find k db in
       if matches_modes sigma args se.sentry_mode then
-        merge_entry secvars db se.sentry_nopat se.sentry_pat
-      else merge_entry secvars db [] []
+        ModeMatch (merge_entry secvars db se.sentry_nopat se.sentry_pat)
+      else ModeMismatch
 
   (* [c] contains an existential *)
   let map_eauto sigma ~secvars (k,args) concl db =
@@ -627,8 +630,8 @@ struct
       if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
         let pat = lookup_tacs sigma concl st se in
-        merge_entry secvars db [] pat
-      else merge_entry secvars db [] []
+        ModeMatch (merge_entry secvars db [] pat)
+      else ModeMismatch
 
   let is_exact = function
     | Give_exact _ -> true
@@ -1519,7 +1522,9 @@ let pr_hint_term env sigma cl =
       let fn = try
           let hdc = decompose_app_bound sigma cl in
             if occur_existential sigma cl then
-              Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl
+              (fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with
+              | ModeMatch l -> l
+              | ModeMismatch -> [])
             else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
         with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
       in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 7bb17489bf..2663f65851 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -125,6 +125,10 @@ val glob_hints_path_atom :
 val glob_hints_path :
   Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen
 
+type 'a with_mode =
+  | ModeMatch of 'a
+  | ModeMismatch
+
 module Hint_db :
   sig
     type t
@@ -140,16 +144,20 @@ module Hint_db :
     val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the
-        arguments, _not_ using the discrimination net. *)
+        arguments, _not_ using the discrimination net.
+        Returns a [ModeMismatch] if there are declared modes and none matches.
+        *)
     val map_existential : evar_map -> secvars:Id.Pred.t ->
-      (GlobRef.t * constr array) -> constr -> t -> full_hint list
+      (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
 
     (** All hints associated to the reference, respecting modes if evars appear in the
-        arguments and using the discrimination net. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
+        arguments and using the discrimination net.
+        Returns a [ModeMismatch] if there are declared modes and none matches. *)
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
 
-    (** All hints associated to the reference, respecting modes if evars appear in the
-        arguments. *)
+    (** All hints associated to the reference.
+        Precondition: no evars should appear in the arguments, so no modes
+        are checked. *)
     val map_auto : evar_map -> secvars:Id.Pred.t ->
        (GlobRef.t * constr array) -> constr -> t -> full_hint list