Hint Mode =: Honor all registered modes, enforce = mode in Hint Extern

doc/changelog/04-tactics/22415-janno-hint-mode-i-Changed.rst

@@ -0,0 +1,7 @@
+- **Changed:**
+  :cmd:`Hint Mode` containing mode ``=`` now prevent :cmd:`Hint Extern` from
+  instantiating the corresponding existential variables. Code that relied on
+  :cmd:`Hint Extern` instantiating an argument marked with ``=`` will no longer
+  work.
+  (`#22415 <https://github.com/rocq-prover/rocq/pull/22415>`_,
+  by Jan-Oliver Kaiser).

doc/changelog/04-tactics/22415-janno-hint-mode-i-Fixed.rst

@@ -0,0 +1,6 @@
+- **Fixed:**
+  :cmd:`Hint Mode` declarations are now treated as alternatives when several
+  matching modes contain ``=``
+  (`#22415 <https://github.com/rocq-prover/rocq/pull/22415>`_,
+  fixes `#22413 <https://github.com/rocq-prover/rocq/issues/22413>`_,
+  by Jan-Oliver Kaiser).

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -869,14 +869,23 @@ Creating Hints
       match its corresponding mode.
 
       Mode ``=`` poses no restrictions on the *presence* of evars in the term.
-      Instead, it disallows *all* existential variables occurring in *any*
-      argument annotated with ``=`` from being instantiated during the
-      application of the hint for *any* reason. In particular, existential
-      variables occurring in several arguments with mixed modes of which at
-      least one is ``=`` will not be instantiated during hint application. This
-      restriction only applies to the unification of the hint's conclusion with
-      the query. It does not apply to subgoals generated by a successful hint
-      application. Mode ``=`` has no effect on :cmd:`Hint Extern`\s.
+      Instead, it prevents hints from instantiating *any* existential variable
+      occurring in an argument annotated with ``=`` during the application of
+      the hint.
+
+      Specifically, for :cmd:`Hint Resolve`, :cmd:`Hint Constructor`, and
+      :cmd:`Hint Immediate`, this restriction applies only to the unification
+      of the hint's conclusion with the current goal. Any subsequent resolution
+      of subgoals generated by the hint is not restricted by any ``=`` mode of
+      :n:`@qualid` (unless the subgoals are themselves applications of
+      :n:`@qualid`).
+
+      For ``=`` modes in :cmd:`Hint Extern`, typeclass resolution introduces a
+      check after the hint's tactic code which rejects any solution the hint
+      generates that results in the instantiation of any argument of
+      :n:`@qualid` with a ``=`` mode. This check is performed before typeclass
+      resolution continues with the subgoals resulting from the generated
+      solution.
 
       Only :tacn:`typeclasses eauto` uses these hints.
       :cmd:`Hint Mode` is especially useful for typeclasses, when one does not want

tactics/class_tactics.ml

@@ -216,9 +216,11 @@ let shelve_dependencies gls =
 
 let hintmap_of env sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> ModeMatch (NoMode, Hint_db.map_none ~secvars db)
+  | None ->
+    let no_mode = { mode_match = NoMode; mode_frozen_evars = Evar.Set.empty } in
+    fun db -> Some ([no_mode], Hint_db.map_none ~secvars db)
   | Some hdc ->
-    fun db -> Hint_db.map_eauto env sigma ~secvars hdc concl db
+    fun db -> Hint_db.map_eauto_modes env sigma ~secvars hdc concl db
 
 type hint_v = {
   hint_tac : unit Proofview.tactic;
@@ -274,7 +276,18 @@ and e_my_find_search db_list local_db secvars hdc complete env sigma concl0 =
       end
     | _ -> None
   in
-  let tac_of_hint (flags,h) =
+  let protect_frozen_evars frozen_evars tac =
+    if Evar.Set.is_empty frozen_evars then tac
+    else
+      Proofview.tclBIND tac (fun () ->
+        Proofview.tclEVARMAP >>= fun sigma ->
+        if Evar.Set.for_all (Evd.is_undefined sigma) frozen_evars then
+          Proofview.tclUNIT ()
+        else
+          Tacticals.tclZEROMSG
+            (str "Hint Extern instantiated an evar frozen by Hint Mode ="))
+  in
+  let tac_of_hint (flags, frozen_evars, h) =
     let name = FullHint.name h in
     let tac = function
       | Res_pf h ->
@@ -296,7 +309,8 @@ and e_my_find_search db_list local_db secvars hdc complete env sigma concl0 =
         Tacticals.tclTHEN fst snd
       | Unfold_nth c ->
         Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
-      | Extern (p, tacast) -> conclPattern concl0 p tacast
+      | Extern (p, tacast) ->
+        protect_frozen_evars frozen_evars (conclPattern concl0 p tacast)
     in
     let tac = FullHint.run h tac in
     let tac = if complete then Tacticals.tclCOMPLETE tac else tac in
@@ -313,8 +327,8 @@ and e_my_find_search db_list local_db secvars hdc complete env sigma concl0 =
   in
   let hint_of_db = hintmap_of env sigma hdc secvars concl in
   let hintl = List.map_filter (fun db -> match hint_of_db db with
-      | ModeMatch (m, l) -> Some (db, m, l)
-      | ModeMismatch -> None)
+      | Some (modes, hints) -> Some (db, modes, hints)
+      | None -> None)
       (local_db :: db_list)
   in
   (* In case there is a mode mismatch in all the databases we get stuck.
@@ -324,22 +338,52 @@ and e_my_find_search db_list local_db secvars hdc complete env sigma concl0 =
   else
     let hintl =
       CList.map
-        (fun (db, m, tacs) ->
+        (fun (db, modes, tacs) ->
            let all = Evarsolve.AllowedEvars.all in
-           let allowed_evars = match allowed_evars, m with
-             | _, NoMode -> Option.default all allowed_evars
+           let allowed_evars = match allowed_evars, modes with
+             | _, [{ mode_match = NoMode }] -> [Option.default all allowed_evars]
              (* [allowed_evars] from [Strict Resolution] take precedence over
-                the (necessarily less restrictive) set of allowed evars from
+                the (necessarily less restrictive) sets of allowed evars from
                 [Hint Mode =] *)
-             | Some allowed_evars, WithMode _ -> allowed_evars
-             | None, WithMode evars -> evars
+             | Some allowed_evars, _ -> [allowed_evars]
+             | None, modes ->
+               List.map (function
+                 | { mode_match = WithMode evars } -> evars
+                 | { mode_match = NoMode } -> assert false)
+                 modes
            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)
+           let map_hint hint =
+             let make_tac allowed_evars frozen_evars =
+               let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in
+               tac_of_hint (flags, frozen_evars, hint)
+             in
+             match FullHint.repr hint, allowed_evars with
+             | Extern _, _ ->
+               (* Extern tactics do not use the unification flags, but each
+                  matching mode imposes its own frozen-evar postcondition. *)
+               List.map
+                 (fun { mode_frozen_evars } -> make_tac all mode_frozen_evars)
+                 modes
+             (* Unfold hints do not instantiate evars, so mode alternatives
+                would produce identical tactics. *)
+             | Unfold_nth _, allowed_evars :: _ ->
+               [make_tac allowed_evars Evar.Set.empty]
+             | _, [] -> assert false
+             | _ ->
+               List.map
+                 (fun allowed_evars -> make_tac allowed_evars Evar.Set.empty)
+                 allowed_evars
+           in
+           modes, List.concat_map map_hint tacs)
         hintl
     in
     let modes, hintl = List.split hintl in
-    let all_mode_match = List.for_all (fun m -> m != NoMode) modes in
+    let has_mode =
+      List.for_all (function
+        | { mode_match = NoMode } -> false
+        | { mode_match = WithMode _ } -> true)
+    in
+    let all_mode_match = List.for_all has_mode modes in
     let hintl = match hintl with
       (* Optim: only sort if multiple hint sources were involved *)
       | [hintl] -> hintl

tactics/hints.ml

@@ -600,6 +600,11 @@ type mode_match =
   | NoMode
   | WithMode of Evarsolve.AllowedEvars.t
 
+type mode_restriction = {
+  mode_match : mode_match;
+  mode_frozen_evars : Evar.Set.t;
+}
+
 type 'a with_mode =
   | ModeMatch of mode_match * 'a
   | ModeMismatch
@@ -612,6 +617,9 @@ val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : Environ.env -> secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_eauto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
                 (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
+val map_eauto_modes : Environ.env -> evar_map -> secvars:Id.Pred.t ->
+                (GlobRef.t * constr array) -> constr -> t ->
+                (mode_restriction list * full_hint list) option
 val map_auto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
                (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val add_list : env -> evar_map -> hint_entry list -> t -> t
@@ -688,41 +696,51 @@ struct
     in
     hrec c
 
-  let match_mode sigma m arg =
-    match m with
-    | ModeInput -> not (occur_existential sigma arg)
-    | ModeNoHeadEvar -> has_no_head_evar sigma arg
-    | ModeOutput -> true
-    | _ -> assert false
-
   let matches_mode sigma args 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 = ModeFrozen) mode then
-        let exception Mismatch in
-        begin try
-          (* forbid all evars appearing in arguments with [ModeFrozen],
-             unconditionally, even when they appear in other arguments. *)
-          let f forbid m arg =
-            match m with
-            | ModeNoHeadEvar when not (has_no_head_evar sigma arg) -> raise Mismatch
-            | ModeInput when occur_existential sigma arg -> raise Mismatch
-            | ModeFrozen -> Evar.Set.union forbid (Evd.evars_of_term sigma arg)
-            | ModeNoHeadEvar | ModeInput | ModeOutput -> forbid
-          in
-          let forbid = Array.fold_left2 f Evar.Set.empty mode args 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
+      let exception Mismatch in
+      begin try
+        (* Forbid all evars appearing in arguments with [ModeFrozen],
+           unconditionally, even when they appear in other arguments. *)
+        let f forbid m arg =
+          match m with
+          | ModeNoHeadEvar when not (has_no_head_evar sigma arg) -> raise Mismatch
+          | ModeInput when occur_existential sigma arg -> raise Mismatch
+          | ModeFrozen -> Evar.Set.union forbid (Evd.evars_of_term sigma arg)
+          | ModeNoHeadEvar | ModeInput | ModeOutput -> forbid
+        in
+        Some (Array.fold_left2 f Evar.Set.empty mode args)
+      with Mismatch -> None
+      end
     else None
 
   let matches_modes sigma args modes =
-    if List.is_empty modes then Some NoMode
+    if List.is_empty modes then
+      Some [{ mode_match = NoMode; mode_frozen_evars = Evar.Set.empty }]
     else
-      Option.map (fun x -> WithMode x) (List.find_map (matches_mode sigma args) modes)
+      (* Modes are alternatives. Keep their restrictions separate: merging the
+         sets of allowed evars could permit an application that satisfies none
+         of the declared modes. *)
+      let rec aux forbids = function
+        | [] ->
+          let to_restriction forbid =
+            let allowed =
+              if Evar.Set.is_empty forbid then Evarsolve.AllowedEvars.all
+              else Evarsolve.AllowedEvars.except forbid
+            in
+            { mode_match = WithMode allowed; mode_frozen_evars = forbid }
+          in
+          List.rev_map to_restriction forbids
+        | mode :: modes ->
+          match matches_mode sigma args mode with
+          | None -> aux forbids modes
+          | Some forbid ->
+            if List.exists (Evar.Set.equal forbid) forbids then aux forbids modes
+            else aux (forbid :: forbids) modes
+      in
+      match aux [] modes with
+      | [] -> None
+      | modes -> Some modes
 
   let merge_entry secvars db nopat pat =
     let fold uid accu = UID.Map.get uid db.hintdb_data :: accu in
@@ -750,13 +768,19 @@ struct
     merge_entry secvars db [] pat
 
   (* [c] contains an existential *)
-  let map_eauto env sigma ~secvars (k,args) concl db =
+  let map_eauto_modes env sigma ~secvars (k,args) concl db =
     let se = find env k db in
-      match matches_modes sigma args se.sentry_mode with
-      | Some m ->
-        let pat = lookup_tacs env sigma concl db.hintdb_data se in
-        ModeMatch (m, merge_entry secvars db [] pat)
-      | None -> ModeMismatch
+    match matches_modes sigma args se.sentry_mode with
+    | Some modes ->
+      let pat = lookup_tacs env sigma concl db.hintdb_data se in
+      Some (modes, merge_entry secvars db [] pat)
+    | None -> None
+
+  let map_eauto env sigma ~secvars hdc concl db =
+    match map_eauto_modes env sigma ~secvars hdc concl db with
+    | Some ({ mode_match } :: _, hints) -> ModeMatch (mode_match, hints)
+    | Some ([], _) -> assert false
+    | None -> ModeMismatch
 
   let is_exact = function
     | Give_exact _ -> true

tactics/hints.mli

@@ -106,6 +106,11 @@ type mode_match =
   | NoMode
   | WithMode of Evarsolve.AllowedEvars.t
 
+type mode_restriction = {
+  mode_match : mode_match;
+  mode_frozen_evars : Evar.Set.t;
+}
+
 type 'a with_mode =
   | ModeMatch of mode_match * 'a
   | ModeMismatch
@@ -135,6 +140,15 @@ module Hint_db :
         Returns a [ModeMismatch] if there are declared modes and none matches. *)
     val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
+    (** As [map_eauto], but returns the nonempty list of distinct matching
+        mode restrictions in lookup order, including the evars frozen by each
+        restriction. The result is [None] when modes are declared but none
+        matches, and the mode list contains one [NoMode] restriction when none
+        are declared. *)
+    val map_eauto_modes : env -> evar_map -> secvars:Id.Pred.t ->
+      (GlobRef.t * constr array) -> constr -> t ->
+      (mode_restriction list * FullHint.t list) option
+
     (** All hints associated to the reference.
         Precondition: no evars should appear in the arguments, so no modes
         are checked. *)