Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions

Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers

13 files changed, 101 insertions, 56 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 5ca16ae1fe..bcb73f8fd0 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -18,6 +18,7 @@ Unreleased changes
 
 **Tactic language**
 
+- Modes are now taken into account by `typeclasses eauto` for local hypotheses.
 
 **SSReflect**
 
diff --git a/clib/cSig.mli b/clib/cSig.mli
index 859018ca4b..0012bcef17 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -68,6 +68,8 @@ sig
     val remove: key -> 'a t -> 'a t
     val merge:
          (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+    val union:
+      (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
     val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
     val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
     val iter: (key -> 'a -> unit) -> 'a t -> unit
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 09ffb39c21..db59ef47b0 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -290,6 +290,14 @@ struct
     in
     Int.Map.merge fm s1 s2
 
+  let union f s1 s2 =
+    let fm h m1 m2 =
+      let m = Map.union f m1 m2 in
+      if Map.is_empty m then None
+      else Some m
+    in
+    Int.Map.union fm s1 s2
+
   let compare f s1 s2 =
     let fc m1 m2 = Map.compare f m1 m2 in
     Int.Map.compare fc s1 s2
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a5e9023732..77a6ee79cc 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -405,6 +405,8 @@ few other commands related to typeclasses.
      resolution with the local hypotheses use full conversion during
      unification.
 
+   + When considering local hypotheses, we use the union of all the modes
+     declared in the given databases.
 
    .. cmdv:: typeclasses eauto @num
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..aa14f66df6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
     let declarenew g =
       LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
-    let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+    let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
         uctx_local = local;
         uctx_seff_univs = seff;
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 46ff6340b4..fcbf305f9d 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
           (acc, [], LMap.empty, LMap.empty) l
         in
         let left = CList.uniquize (List.filter (not_lower lower) left) in
-        (acc, left, LMap.union newlow lower)
+        (acc, left, LMap.lunion newlow lower)
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8263c68bf5..b1bbc25fe6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -231,18 +231,15 @@ module LMap = struct
   module M = HMap.Make (Level)
   include M
 
-  let union l r = 
-    merge (fun _k l r ->
-      match l, r with
-      | Some _, _ -> l
-      | _, _ -> r) l r
+  let lunion l r =
+    union (fun _k l _r -> Some l) l r
 
-  let subst_union l r = 
-    merge (fun _k l r ->
+  let subst_union l r =
+    union (fun _k l r ->
       match l, r with
-      | Some (Some _), _ -> l
-      | Some None, None -> l
-      | _, _ -> r) l r
+      | Some _, _ -> Some l
+      | None, None -> Some l
+      | _, _ -> Some r) l r
 
   let diff ext orig =
     fold (fun u v acc -> 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 5543c35741..db178c4bb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -223,8 +223,8 @@ module LMap :
 sig
   include CMap.ExtS with type key = Level.t and module Set := LSet
 
-  val union : 'a t -> 'a t -> 'a t
-  (** [union x y] favors the bindings in the first map. *)
+  val lunion : 'a t -> 'a t -> 'a t
+  (** [lunion x y] favors the bindings in the first map. *)
 
   val diff : 'a t -> 'a t -> 'a t
   (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1ac7d201a..160e4f164e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -548,7 +548,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
           make_apply_entry ~name env sigma flags pri false])
     else []
 
-let make_hints g st only_classes sign =
+let make_hints g (modes,st) only_classes sign =
   let hintlist =
     List.fold_left
       (fun hints hyp ->
@@ -565,7 +565,9 @@ let make_hints g st only_classes sign =
           in hint @ hints
         else hints)
       ([]) sign
-  in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
+  in
+  let db = Hint_db.add_modes modes @@ Hint_db.empty st true in
+  Hint_db.add_list (pf_env g) (project g) hintlist db
 
 module Search = struct
   type autoinfo =
@@ -578,29 +580,29 @@ module Search = struct
 
   (** Local hints *)
   let autogoal_cache = Summary.ref ~name:"autogoal_cache"
-      (DirPath.empty, true, Context.Named.empty,
+      (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty,
        Hint_db.empty TransparentState.full true)
 
-  let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
+  let make_autogoal_hints only_classes (modes,st as mst) g =
     let open Proofview in
     let open Tacmach.New in
     let sign = Goal.hyps g in
-    let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
+    let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in
     let cwd = Lib.cwd () in
     let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in
     if DirPath.equal cwd dir &&
          (onlyc == only_classes) &&
            Context.Named.equal eq sign sign' &&
-             Hint_db.transparent_state cached_hints == st
+             cached_modes == modes
     then cached_hints
     else
       let hints = make_hints {it = Goal.goal g; sigma = project g}
-                             st only_classes sign
+                             mst only_classes sign
       in
-      autogoal_cache := (cwd, only_classes, sign, hints); hints
+      autogoal_cache := (cwd, only_classes, sign, modes, hints); hints
 
-  let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
-    let hints = make_autogoal_hints only_classes ~st g in
+  let make_autogoal mst only_classes dep cut i g =
+    let hints = make_autogoal_hints only_classes mst g in
     { search_hints = hints;
       search_depth = [i]; last_tac = lazy (str"none");
       search_dep = dep;
@@ -695,7 +697,8 @@ module Search = struct
           if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
           then
             let st = Hint_db.transparent_state info.search_hints in
-            make_autogoal_hints info.search_only_classes ~st gl'
+            let modes = Hint_db.modes info.search_hints in
+            make_autogoal_hints info.search_only_classes (modes,st) gl'
           else info.search_hints
         in
         let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in
@@ -830,19 +833,19 @@ module Search = struct
                       (fun e' -> let (e, info) = merge_exceptions e e' in
                               Proofview.tclZERO ~info e))
 
-  let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
+  let search_tac_gl mst only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
     let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
-    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+    let info = make_autogoal mst only_classes dep (cut_of_hints hints) i gl in
     search_tac hints depth 1 info
 
-  let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
+  let search_tac mst only_classes dep hints depth =
     let open Proofview in
     let tac sigma gls i =
       Goal.enter
         begin fun gl ->
-          search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
+          search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end
     in
       Proofview.Unsafe.tclGETGOALS >>= fun gls ->
       let gls = CList.map Proofview.drop_state gls in
@@ -867,11 +870,11 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=TransparentState.full) ?(unique=false)
+  let eauto_tac mst ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
     let tac =
-      let search = search_tac ~st only_classes dep hints in
+      let search = search_tac mst only_classes dep hints in
       let dfs =
         match strategy with
         | None -> not (get_typeclasses_iterative_deepening ())
@@ -915,8 +918,8 @@ module Search = struct
                                             | Some i -> str ", with depth limit " ++ int i));
     tac
 
-  let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
-    Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints
+  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
 
   let run_on_evars env evm p tac =
     match evars_to_goals p evm with
@@ -968,8 +971,8 @@ module Search = struct
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
-  let evars_eauto env evd depth only_classes unique dep st hints p =
-    let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+  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 res = run_on_evars env evd p eauto_tac in
     match res with
     | None -> evd
@@ -983,11 +986,11 @@ module Search = struct
 
   let typeclasses_resolve env evd debug depth unique p =
     let db = searchtable_map typeclasses_db in
-    typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
+    let st = Hint_db.transparent_state db in
+    let modes = Hint_db.modes db in
+    typeclasses_eauto env evd ?depth unique (modes,st) [db] p
 end
 
-(** Binding to either V85 or Search implementations. *)
-
 let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
                       ?strategy ~depth dbs =
   let dbs = List.map_filter
@@ -996,8 +999,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
               dbs
   in
   let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+  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 ~st ~only_classes ?strategy ~depth ~dep:true dbs
+  Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
@@ -1140,11 +1145,12 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
   let st = Hint_db.transparent_state hints in
+  let modes = Hint_db.modes hints in
   let depth = get_typeclasses_depth () in
   let gls' =
       try
         Proofview.V82.of_tactic
-        (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
+        (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls
       with Refiner.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c950e3de3d..b9291f6124 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -27,9 +27,18 @@ type search_strategy = Dfs | Bfs
 
 val set_typeclasses_strategy : search_strategy -> unit
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
-                        depth:(Int.t option) ->
-                        Hints.hint_db_name list -> unit Proofview.tactic
+val typeclasses_eauto :
+  ?only_classes:bool
+  (** Should non-class goals be shelved and resolved at the end *)
+  -> ?st:TransparentState.t
+  (** The transparent_state used when working with local hypotheses  *)
+  -> ?strategy:search_strategy
+  (** Is a traversing-strategy specified? *)
+  -> depth:(Int.t option)
+  (** Bounded or unbounded search *)
+  -> Hints.hint_db_name list
+  (** The list of hint databases to use *)
+  -> unit Proofview.tactic
 
 val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
@@ -41,8 +50,8 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
 module Search : sig
   val eauto_tac :
-    ?st:TransparentState.t
-    (** The transparent_state used when working with local hypotheses  *)
+    Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
+    (** The transparent_state and modes used when working with local hypotheses  *)
     -> ?unique:bool
     (** Should we force a unique solution *)
     -> only_classes:bool
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 11a8816159..cc56c1c425 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -289,8 +289,6 @@ let lookup_tacs sigma concl st se =
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
-module Constr_map = Map.Make(GlobRef.Ordered)
-
 let is_transparent_gr ts = function
   | VarRef id -> TransparentState.is_transparent_variable ts id
   | ConstRef cst -> TransparentState.is_transparent_constant ts cst
@@ -520,6 +518,8 @@ val add_cut : hints_path -> t -> t
 val add_mode : GlobRef.t -> hint_mode array -> t -> t
 val cut : t -> hints_path
 val unfolds : t -> Id.Set.t * Cset.t
+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
 
@@ -532,7 +532,7 @@ struct
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
     use_dn : bool;
-    hintdb_map : search_entry Constr_map.t;
+    hintdb_map : search_entry GlobRef.Map.t;
     (* A list of unindexed entries starting with an unfoldable constant
        or with no associated pattern. *)
     hintdb_nopat : (GlobRef.t option * stored_data) list;
@@ -548,12 +548,12 @@ struct
 			  hintdb_unfolds = (Id.Set.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
-			  hintdb_map = Constr_map.empty;
+                          hintdb_map = GlobRef.Map.empty;
 			  hintdb_nopat = [];
 			  hintdb_name = name; }
 
   let find key db =
-    try Constr_map.find key db.hintdb_map
+    try GlobRef.Map.find key db.hintdb_map
     with Not_found -> empty_se
  
   let realize_tac secvars (id,tac) =
@@ -650,11 +650,11 @@ struct
 	  else db
       | Some gr ->
 	  let oval = find gr db in
-	    { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+            { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
 
   let rebuild_db st' db =
     let db' =
-      { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map;
+      { db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map;
 	hintdb_state = st'; hintdb_nopat = [] }
     in
       List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
@@ -693,7 +693,7 @@ struct
   let remove_list grs db =
     let filter (_, h) =
       match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
-    let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
+    let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
@@ -706,11 +706,11 @@ struct
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
     f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
-    Constr_map.iter iter_se db.hintdb_map
+    GlobRef.Map.iter iter_se db.hintdb_map
 
   let fold f db accu =
     let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
-    Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
+    GlobRef.Map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
 
   let transparent_state db = db.hintdb_state
 
@@ -724,12 +724,21 @@ struct
   let add_mode gr m db =
     let se = find gr db in
     let se = { se with sentry_mode = m :: se.sentry_mode } in
-    { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
+    { db with hintdb_map = GlobRef.Map.add gr se db.hintdb_map }
 
   let cut db = db.hintdb_cut
 
   let unfolds db = db.hintdb_unfolds
 
+  let add_modes modes db =
+    let f gr e me =
+      Some { e with sentry_mode = me.sentry_mode @ e.sentry_mode }
+    in
+    let mode_entries = GlobRef.Map.map (fun m -> { empty_se with sentry_mode = m }) modes in
+    { db with hintdb_map = GlobRef.Map.union f db.hintdb_map mode_entries }
+
+  let modes db = GlobRef.Map.map (fun se -> se.sentry_mode) db.hintdb_map
+
   let use_dn db = db.use_dn
 
 end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 90a8b7fe52..7b8f96cdd8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -162,6 +162,9 @@ module Hint_db :
     val cut : t -> hints_path
 
     val unfolds : t -> Id.Set.t * Cset.t
+
+    val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+    val modes : t -> hint_mode array list GlobRef.Map.t
   end
 
 type hint_db = Hint_db.t
diff --git a/test-suite/bugs/closed/bug_5752.v b/test-suite/bugs/closed/bug_5752.v
new file mode 100644
index 0000000000..b4218d66df
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5752.v
@@ -0,0 +1,8 @@
+Class C (A : Type) := c : A.
+
+Hint Mode C ! : typeclass_instances.
+
+Goal forall f : (forall A, C A -> C (list A)), True.
+intros.
+  Check c. (* Loops if modes are ignored. *)
+Abort.