Experiment with considering evars in + mode rigid for TC resolution

cf coq#18078

tactics/class_tactics.ml

@@ -319,6 +319,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
     let hintl =
       CList.map
         (fun (db, m, tacs) ->
+           let allowed_evars = match m with
+             | NoMode -> allowed_evars
+             | WithMode evars -> evars
+           in
           let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in
           m, List.map (fun x -> tac_of_hint (flags, x)) tacs)
         hintl

tactics/hints.ml

@@ -532,7 +532,7 @@ type hint_db_name = string
 
 type mode_match =
   | NoMode
-  | WithMode of hint_mode array
+  | WithMode of Evarsolve.AllowedEvars.t
 
 type 'a with_mode =
   | ModeMatch of mode_match * 'a
@@ -603,26 +603,44 @@ struct
       (* Warn about no longer typable hint? *)
       None
 
-  let head_evar sigma c =
+  let has_head_evar sigma c =
     let rec hrec c = match EConstr.kind sigma c with
-      | Evar (evk,_)   -> evk
+      | Evar (evk,_)   -> true
       | App (c,_)      -> hrec c
       | Cast (c,_,_)   -> hrec c
-      | _              -> raise Evarutil.NoHeadEvar
+      | _              -> false
     in
     hrec c
 
   let match_mode sigma m arg =
     match m with
     | ModeInput -> not (occur_existential sigma arg)
-    | ModeNoHeadEvar ->
-       (try ignore(head_evar sigma arg); false
-                 with Evarutil.NoHeadEvar -> true)
+    | ModeNoHeadEvar -> not (has_head_evar sigma arg)
     | ModeOutput -> true
 
   let matches_mode sigma args mode =
-    if Array.length mode == Array.length args &&
-        Array.for_all2 (match_mode sigma) mode args then Some mode
+    if Array.length mode == Array.length args then
+      (* we don't need to compute evar sets if there's no ModeInput *)
+      if Array.exists (fun m -> m = ModeInput) mode then
+        let exception Mismatch in
+        begin try
+          let in_input, in_output = Array.fold_left2 (fun (in_input,in_output) m arg ->
+              match m with
+              | ModeInput -> (Evar.Set.union in_input (Evd.evars_of_term sigma arg), in_output)
+              | ModeNoHeadEvar | ModeOutput ->
+                if m = ModeNoHeadEvar && has_head_evar sigma arg then raise Mismatch
+                else (in_input, Evar.Set.union (Evd.evars_of_term sigma arg) in_output))
+              (Evar.Set.empty, Evar.Set.empty)
+              mode
+              args
+          in
+          let forbid = Evar.Set.diff in_input in_output in
+          Some (Evarsolve.AllowedEvars.except forbid)
+        with Mismatch -> None
+        end
+      else if Array.for_all2 (match_mode sigma) mode args
+      then Some Evarsolve.AllowedEvars.all
+      else None
     else None
 
   let matches_modes sigma args modes =

tactics/hints.mli

@@ -105,7 +105,7 @@ val glob_hints_path :
 
 type mode_match =
   | NoMode
-  | WithMode of hint_mode array
+  | WithMode of Evarsolve.AllowedEvars.t
 
 type 'a with_mode =
   | ModeMatch of mode_match * 'a

test-suite/bugs/bug_18078.v

@@ -0,0 +1,35 @@
+(* Meaning: P implies Q and the only reasonable way to
+   prove Q is to try proving P. *)
+Definition safe_implication(P: Prop)(Q: Prop): Prop := P -> Q.
+
+Create HintDb safe_implication.
+
+Ltac apply_safe_implication :=
+  lazymatch goal with
+  | |- ?Q =>
+      let H := fresh in
+      eassert (safe_implication _ Q) as H by (typeclasses eauto with safe_implication);
+      unfold safe_implication in H;
+      apply H;
+      clear H
+  end.
+
+Parameter f: nat -> nat -> Prop.
+Parameter g: nat -> Prop.
+Parameter h: nat -> Prop.
+
+Axiom f_same_args: forall x, safe_implication (g x) (f x x).
+Axiom f_first_arg_0: forall x, safe_implication (h x) (f 0 x).
+
+#[export] Hint Resolve f_first_arg_0 f_same_args : safe_implication.
+
+#[global] Hint Mode safe_implication - + : safe_implication.
+
+Goal forall a, 0 < a -> h a -> exists b, f 0 b /\ 0 < b.
+Proof.
+  intros. eexists. split.
+
+  apply_safe_implication.
+
+  all: eassumption.
+Qed.