resolve_tc c solves typeclasses appearing in c

doc/changelog/04-tactics/13071-resolve-tc-in-term.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  :tacn:`resolve_tc` to resolve typeclass evars appearing in a given term
+  (`#13071 <https://github.com/coq/coq/pull/13071>`_,
+  by Gaëtan Gilbert).

doc/sphinx/addendum/type-classes.rst

@@ -518,6 +518,17 @@ Command summary
    subgoals created by the lemma application, rather than doing typeclass
    resolution locally at the hint application time.
 
+.. tacn:: resolve_tc @ident
+
+   The tactic `resolve_tc` resolves the existential variables
+   appearing in the term bound to :n:`@ident` whose types are
+   typeclasses. It fails if any of them cannot be resolved.
+
+   This tactic works even when no goals are focused, so for instance
+   `let c := open_constr:(something) in exact c; resolve_tc c` will
+   solve the typeclass holes in `something` which remain after the
+   unification done by :tacn:`exact`.
+
 .. _TypeclassesTransparent:
 
 Typeclasses Transparent, Typeclasses Opaque

plugins/ltac/g_ltac.mlg

@@ -144,6 +144,7 @@ GRAMMAR EXTEND Gram
       | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
           { CAst.make ~loc (TacSolve l) }
       | IDENT "idtac"; l = LIST0 message_token -> { CAst.make ~loc (TacId l) }
+      | IDENT "resolve_tc"; id=identref -> { CAst.make ~loc (TacResolveTC id ) }
       | g=failkw; n = [ n = nat_or_var -> { n } | -> { fail_default_value } ];
           l = LIST0 message_token -> { CAst.make ~loc (TacFail (g,n,l)) }
       | st = simple_tactic -> { st }

plugins/ltac/pptactic.ml

@@ -1030,6 +1030,7 @@ let pr_goal_selector ~toplevel s =
             | TacComplete t ->
               pr_tac (LevelLe lcomplete) t, lcomplete
             | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, ltactical
+            | TacResolveTC id -> keyword "resolve_tc" ++ spc() ++ pr_lident id, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom t ->

plugins/ltac/tacexpr.ml

@@ -233,6 +233,7 @@ and 'a gen_tactic_expr_r =
   | TacFun of 'a gen_tactic_fun_ast
   | TacArg of 'a gen_tactic_arg
   | TacSelect of Goal_select.t * 'a gen_tactic_expr
+  | TacResolveTC of lident
   (* For ML extensions *)
   | TacML of ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)

plugins/ltac/tacexpr.mli

@@ -232,6 +232,7 @@ and 'a gen_tactic_expr_r =
   | TacFun of 'a gen_tactic_fun_ast
   | TacArg of 'a gen_tactic_arg
   | TacSelect of Goal_select.t * 'a gen_tactic_expr
+  | TacResolveTC of lident
   (* For ML extensions *)
   | TacML of ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)

plugins/ltac/tacintern.ml

@@ -667,6 +667,7 @@ and intern_tactic_seq onlytac ist tac =
   | TacArg a -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
   | TacSelect (sel, tac) ->
       ist.ltacvars, CAst.make ?loc (TacSelect (sel, intern_pure_tactic ist tac))
+  | TacResolveTC id -> ist.ltacvars, CAst.make ?loc (TacResolveTC id)
 
   (* For extensions *)
   | TacAlias (s,l) ->

plugins/ltac/tacinterp.ml

@@ -408,6 +408,16 @@ let interp_int_or_var_as_list ist = function
 let interp_int_or_var_list ist l =
   List.flatten (List.map (interp_int_or_var_as_list ist) l)
 
+let interp_resolve_tc ist {CAst.v=id; loc} =
+    let c = try Names.Id.Map.find id ist.Geninterp.lfun
+      with Not_found -> CErrors.user_err ?loc Pp.(Id.print id ++ str " not bound.")
+    in
+    let c = match Taccoerce.Value.to_constr c with
+      | Some c -> c
+      | None -> Loc.raise ?loc (Taccoerce.CannotCoerceTo "a term")
+    in
+    Class_tactics.resolve_tc c
+
 (* Interprets a bound variable (especially an existing hypothesis) *)
 let interp_hyp ist env sigma ({loc;v=id} as locid) =
   (* Look first in lfun for a value coercible to a variable *)
@@ -1199,6 +1209,8 @@ and eval_tactic_ist ist tac : unit Proofview.tactic =
   | TacComplete tac -> Tacticals.tclCOMPLETE (interp_tactic ist tac)
   | TacArg _ -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
   | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
+  | TacResolveTC id -> interp_resolve_tc ist id
+
   (* For extensions *)
   | TacAlias (s,l) ->
       let alias = Tacenv.interp_alias s in

plugins/ltac/tacsubst.ml

@@ -219,6 +219,7 @@ and subst_tactic subst = CAst.map (function
   | TacComplete tac -> TacComplete (subst_tactic subst tac)
   | TacArg a -> TacArg (subst_tacarg subst a)
   | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
+  | TacResolveTC id -> TacResolveTC id
 
   (* For extensions *)
   | TacAlias (s,l) ->

plugins/ltac/tactic_debug.ml

@@ -377,6 +377,7 @@ let tac_loc tac =
   | TacFun _ -> "TacFun"
   | TacArg _ -> "TacArg"
   | TacSelect _ -> "TacSelect"
+  | TacResolveTC _ -> "TacResolveTC"
   | TacML _ -> "TacML"
   | TacAlias _ -> "TacAlias"
   in

pretyping/typeclasses.mli

@@ -140,3 +140,5 @@ val error_unresolvable : env -> evar_map -> Evar.Set.t -> 'a
     it is up to the plugin to do so. *)
 val set_solve_all_instances : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) -> unit
 val set_solve_one_instance : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) -> unit
+
+val get_typeclasses_unique_solutions : unit -> bool

tactics/class_tactics.ml

@@ -1322,3 +1322,15 @@ let autoapply c i =
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.evar_source (Evd.find_undefined sigma ev))))) sigma in
       Proofview.Unsafe.tclEVARS sigma) end
+
+let resolve_tc c =
+  let open Proofview.Notations in
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let depth = get_typeclasses_depth () in
+  let unique = get_typeclasses_unique_solutions () in
+  let evars = Evarutil.undefined_evars_of_term sigma c in
+  let filter = (fun ev _ -> Evar.Set.mem ev evars) in
+  let fail = true in
+  let sigma = resolve_all_evars depth unique env (initial_select_evars filter) sigma fail in
+  Proofview.Unsafe.tclEVARS sigma

tactics/class_tactics.mli

@@ -55,6 +55,8 @@ val is_ground : constr -> unit Proofview.tactic
 
 val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
+val resolve_tc : constr -> unit Proofview.tactic
+
 module Search : sig
   val eauto_tac :
     Hints.hint_mode array list GlobRef.Map.t * TransparentState.t

test-suite/success/resolve_tc.v

@@ -0,0 +1,22 @@
+Class C := c {}.
+Local Existing Instance c.
+
+(* check that exact doesn't do the resolution *)
+Lemma bad : C.
+Proof.
+  let x := open_constr:(_:C) in exact x.
+  Fail Qed.
+Unshelve.
+exact _.
+Qed.
+
+Lemma foo : C.
+Proof.
+  let x := open_constr:(_:C) in resolve_tc x; exact x.
+Qed.
+
+(* resolve_tc doesn't focus *)
+Lemma bar : C.
+Proof.
+  let x := open_constr:(_:C) in exact x; resolve_tc x.
+Qed.