diff --git a/doc/changelog/04-tactics/22415-janno-hint-mode-i-Changed.rst b/doc/changelog/04-tactics/22415-janno-hint-mode-i-Changed.rst new file mode 100644 index 000000000000..5421e0e0ef6f --- /dev/null +++ b/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 `_, + by Jan-Oliver Kaiser). diff --git a/doc/changelog/04-tactics/22415-janno-hint-mode-i-Fixed.rst b/doc/changelog/04-tactics/22415-janno-hint-mode-i-Fixed.rst new file mode 100644 index 000000000000..bbaafb9cd080 --- /dev/null +++ b/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 `_, + fixes `#22413 `_, + by Jan-Oliver Kaiser). diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 8475c1da2764..6c405c5edab8 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/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 diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 08c768125e78..3789e9ce2783 100644 --- a/tactics/class_tactics.ml +++ b/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 diff --git a/tactics/hints.ml b/tactics/hints.ml index 1f65e34ff28e..d65b53696b7c 100644 --- a/tactics/hints.ml +++ b/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 diff --git a/tactics/hints.mli b/tactics/hints.mli index 95c9a3dea0bf..d64f983c2895 100644 --- a/tactics/hints.mli +++ b/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. *) diff --git a/test-suite/bugs/bug_22413.v b/test-suite/bugs/bug_22413.v new file mode 100644 index 000000000000..b3b29f044dc1 --- /dev/null +++ b/test-suite/bugs/bug_22413.v @@ -0,0 +1,143 @@ +Module MultipleFrozenModes. + Class Foo (x y : nat). + + Global Instance foo_10_10 : Foo 10 10 := {}. + + Global Hint Mode Foo = - : typeclass_instances. + + Goal exists y, Foo 10 y. + Proof. eexists. typeclasses eauto. Qed. + + Global Hint Mode Foo - = : typeclass_instances. + + (* Multiple mode declarations are alternatives: the newer mode must not + prevent resolution under an older mode. *) + Goal exists y, Foo 10 y. + Proof. eexists. typeclasses eauto. Qed. + + (* Conversely, alternatives must not be merged into a more permissive mode: + neither declared mode allows both evars to be instantiated. *) + Goal exists x y, Foo x y. + Proof. eexists; eexists. Fail typeclasses eauto. Abort. +End MultipleFrozenModes. + +Module PermissiveAlternative. + Class C (n : nat). + + Global Instance c_1 : C 1 := {}. + + Global Hint Mode C ! : typeclass_instances. + Global Hint Mode C = : typeclass_instances. + + (* Although the newest mode freezes the evar, the older [!] mode permits + resolution because the evar is not at the head of the argument. *) + Goal exists n, C (S n). + Proof. eexists. typeclasses eauto. Qed. +End PermissiveAlternative. + +Module NonmatchingAlternative. + Class C (n : nat). + + Global Instance c_0 : C 0 := {}. + + Global Hint Mode C + : typeclass_instances. + Global Hint Mode C = : typeclass_instances. + + (* The [+] mode does not match an evar and must not make the matching [=] + mode more permissive. *) + Goal exists n, C n. + Proof. eexists. Fail typeclasses eauto. Abort. +End NonmatchingAlternative. + +Module StrictResolution. + #[local] Set Typeclasses Strict Resolution. + + Class C (x y : nat). + + Global Instance c_0_1 : C 0 1 := {}. + + Global Hint Mode C = - : typeclass_instances. + Global Hint Mode C - = : typeclass_instances. + + (* The second mode would permit the first evar to be instantiated, but Strict + Resolution takes precedence over every matching mode alternative. *) + Goal exists x, C x 1. + Proof. eexists. Fail typeclasses eauto. Abort. + + Goal C 0 1. + Proof. typeclasses eauto. Qed. +End StrictResolution. + +Module ExternModes. + Class C (n : nat). + + Global Instance c_0 : C 0 := {}. + Global Hint Extern 0 (C _) => exact c_0 : typeclass_instances. + + Global Hint Mode C + : typeclass_instances. + + Goal exists n, C n. + Proof. eexists. Fail typeclasses eauto. Abort. + + Global Hint Mode C = : typeclass_instances. + + (* A successful extern result is rejected if it instantiates an evar frozen + by the matching mode. Rejecting it also rolls back the assignment. *) + Goal exists n, C n. + Proof. + eexists ?[n]. + Fail typeclasses eauto. + instantiate (n := 1). + Abort. +End ExternModes. + +Module ExternAlternativeModes. + Class C (x y : nat). + + Definition c_y1 (x : nat) : C x 1. + Proof. constructor. Defined. + Global Hint Extern 0 (C ?x _) => exact (c_y1 x) : typeclass_instances. + + Global Hint Mode C = - : typeclass_instances. + Global Hint Mode C - = : typeclass_instances. + + (* The newer mode freezes [y], so its extern result is rejected. Search must + retry the extern under the older mode, which freezes [x] instead. *) + Goal exists x y, C x y /\ x = 0 /\ y = 1. + Proof. + eexists ?[x], ?[y]. + split. + - typeclasses eauto. + - split; reflexivity. + Qed. +End ExternAlternativeModes. + +Module ExternGeneratedSubgoals. + Class C (n : nat). + Class D (n : nat). + + Definition c_of_d (n : nat) (_ : D n) : C n. + Proof. constructor. Defined. + Global Instance d_0 : D 0 := {}. + Global Hint Extern 0 (C ?n) => eapply (c_of_d n) : typeclass_instances. + Global Hint Mode C = : typeclass_instances. + + (* The extern itself leaves [n] undefined. Its generated [D n] subgoal may + instantiate [n], since modes constrain only the hint application. *) + Goal exists n, C n. + Proof. eexists. typeclasses eauto. Qed. +End ExternGeneratedSubgoals. + +Module StrictExternException. + #[local] Set Typeclasses Strict Resolution. + + Class C (n : nat). + + Definition c_0 : C 0. + Proof. constructor. Defined. + Global Hint Extern 0 (C _) => exact c_0 : typeclass_instances. + + (* Strict Resolution historically does not constrain Hint Extern. *) + Goal exists n, C n. + Proof. eexists. typeclasses eauto. Qed. +End StrictExternException. diff --git a/test-suite/output/HintModeExtern.out b/test-suite/output/HintModeExtern.out new file mode 100644 index 000000000000..0f7fd1c621a4 --- /dev/null +++ b/test-suite/output/HintModeExtern.out @@ -0,0 +1,12 @@ +File "./output/HintModeExtern.v", line 10, characters 7-24: +The command has indeed failed with message: +Tactic failure: Proof search failed. +extern called +extern called +File "./output/HintModeExtern.v", line 20, characters 7-24: +The command has indeed failed with message: +Tactic failure: Proof search failed. +guarded extern called +File "./output/HintModeExtern.v", line 34, characters 7-24: +The command has indeed failed with message: +Tactic failure: Proof search failed. diff --git a/test-suite/output/HintModeExtern.v b/test-suite/output/HintModeExtern.v new file mode 100644 index 000000000000..5e175ba0d6d7 --- /dev/null +++ b/test-suite/output/HintModeExtern.v @@ -0,0 +1,35 @@ +Class C (x y : nat). + +Global Hint Extern 0 (C _ _) => idtac "extern called"; fail : typeclass_instances. + +Global Hint Mode C + + : typeclass_instances. + +Goal exists x y, C x y. +Proof. + eexists; eexists. + Fail typeclasses eauto. +Abort. + +Global Hint Mode C = - : typeclass_instances. +Global Hint Mode C - = : typeclass_instances. + +Goal exists x y, C x y. +Proof. + eexists; eexists. + (* Each mode for [C] generates an application attempt. *) + Fail typeclasses eauto. +Abort. + +Class D (n : nat). + +Axiom d_0 : D 0. +Global Hint Extern 0 (D _) => + idtac "guarded extern called"; exact d_0 : typeclass_instances. +Global Hint Mode D = : typeclass_instances. + +Goal exists n, D n. +Proof. + eexists. + (* The proof-state change is rolled back, but output is non-logical. *) + Fail typeclasses eauto. +Abort.