feat: add MVarId.ensureNoMVar

src/Lean/Meta/Tactic/Grind.lean

@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
+import Lean.Meta.Tactic.Grind.EnsureNoMVar

src/Lean/Meta/Tactic/Grind/EnsureNoMVar.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Util
+
+namespace Lean.Meta.Grind
+
+/--
+Throws an exception if target of the given goal contains metavariables.
+-/
+def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
+  let type ← instantiateMVars (← mvarId.getType)
+  if type.hasExprMVar then
+    throwTacticEx `grind mvarId "goal contains metavariables"
+
+end Lean.Meta.Grind

tests/lean/run/grind_revertAll.lean

@@ -4,8 +4,15 @@ open Lean Elab Tactic in
 elab "revert_all" : tactic => do
   liftMetaTactic1 (·.revertAll)
 
+open Lean Elab Tactic in
+elab "ensure_no_mvar" : tactic => do
+  liftMetaTactic1 fun mvarId => do
+    mvarId.ensureNoMVar
+    return mvarId
+
 example {α : Type u} [Inhabited α] (a : α) (f : α → α) (h : f a = default) : default = f a := by
   revert_all
+  ensure_no_mvar
   guard_target =ₛ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a
   intro α inst a f h
   exact h.symm
@@ -13,6 +20,7 @@ example {α : Type u} [Inhabited α] (a : α) (f : α → α) (h : f a = default
 example (a b : α) (h₁ : a = b) (f g : α → α) (h₂ : ∀ x, f x = x) (h₃ : ∀ x, g x = f x) : ∃ x : α, f x = a ∧ g x = b := by
   apply Exists.intro
   revert_all
+  fail_if_success ensure_no_mvar
   intro β a₁ a₂ h f₁ f₂ h' h''
   constructor
   · exact h' a₁