feat(library/tactic/exact_tactic): generate error if 'exact' tactic produces a term containing metavariables

src/library/tactic/exact_tactic.cpp

@@ -4,14 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/constants.h"
 #include "kernel/type_checker.h"
+#include "kernel/error_msgs.h"
+#include "library/util.h"
+#include "library/constants.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration) {
+tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration, bool allow_metavars) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
@@ -19,13 +21,22 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
                 throw_no_goal_if_enabled(s);
                 return none_proof_state();
             }
-            expr t            = head(gs).get_type();
+            expr t                 = head(gs).get_type();
             bool report_unassigned = false;
             if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
                                                        report_unassigned, enforce_type_during_elaboration)) {
                 goals const & gs   = new_s.get_goals();
                 if (gs) {
                     goal const & g     = head(gs);
+                    if (!allow_metavars && has_expr_metavar_relaxed(*new_e)) {
+                        throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
+                                format r = format("invalid 'exact' tactic, term still contains metavariables "
+                                                  "after elaboration");
+                                r       += pp_indent_expr(fmt, *new_e);
+                                return r;
+                            });
+                        return none_proof_state();
+                    }
                     substitution subst = new_s.get_subst();
                     assign(subst, g, *new_e);
                     return some(proof_state(new_s, tail(gs), subst));
@@ -53,12 +64,17 @@ void initialize_exact_tactic() {
     register_tac(exact_tac_name,
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
-                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true);
+                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, false);
                  });
     register_tac(rexact_tac_name,
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'rexact' tactic, invalid argument");
-                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false);
+                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false, false);
+                 });
+    register_tac(refine_tac_name,
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'refine' tactic, invalid argument");
+                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, true);
                  });
 }
 void finalize_exact_tactic() {

tests/lean/exact_partial.lean

@@ -0,0 +1,5 @@
+example (a b : Prop) : a → b → a ∧ b :=
+begin
+  intros,
+  exact (and.intro _ _),
+end

tests/lean/exact_partial.lean.expected.out

@@ -0,0 +1,14 @@
+exact_partial.lean:4:2: error:invalid 'exact' tactic, term still contains metavariables after elaboration
+  and.intro ?M_1 ?M_2
+proof state:
+a b : Prop,
+a_1 : a,
+a_2 : b
+⊢ a ∧ b
+exact_partial.lean:5:0: error: don't know how to synthesize placeholder
+a b : Prop
+⊢ a → b → a ∧ b
+exact_partial.lean:5:0: error: failed to add declaration '14.0' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop),
+    ?M_1