From e729b32b2b77800da2a93ad6eb3d794bee099705 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 May 2022 06:41:17 -0700
Subject: [PATCH] feat: `unfold` should fail if it didn't unfold anything

---
 src/Lean/Meta/Tactic/Unfold.lean           | 2 ++
 tests/lean/unfoldFailure.lean              | 5 +++++
 tests/lean/unfoldFailure.lean.expected.out | 4 ++++
 3 files changed, 11 insertions(+)
 create mode 100644 tests/lean/unfoldFailure.lean
 create mode 100644 tests/lean/unfoldFailure.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index 2587a0f442..d84c8873e4 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -33,11 +33,13 @@ where
 def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
   let target ← instantiateMVars (← getMVarType mvarId)
   let r ← unfold target declName
+  if r.expr == target then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr target}"
   applySimpResultToTarget mvarId target r
 
 def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
   let localDecl ← getLocalDecl fvarId
   let r ← unfold (← instantiateMVars localDecl.type) declName
+  if r.expr == localDecl.type then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr localDecl.type}"
   let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
   return mvarId
 
diff --git a/tests/lean/unfoldFailure.lean b/tests/lean/unfoldFailure.lean
new file mode 100644
index 0000000000..a844f6dc66
--- /dev/null
+++ b/tests/lean/unfoldFailure.lean
@@ -0,0 +1,5 @@
+example : True := by
+  unfold Nat.add
+
+example (h : x = 2 * y) : True := by
+  unfold Nat.add at h
diff --git a/tests/lean/unfoldFailure.lean.expected.out b/tests/lean/unfoldFailure.lean.expected.out
new file mode 100644
index 0000000000..cc62a9ba57
--- /dev/null
+++ b/tests/lean/unfoldFailure.lean.expected.out
@@ -0,0 +1,4 @@
+unfoldFailure.lean:2:2-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
+  True
+unfoldFailure.lean:5:2-5:21: error: tactic 'unfold' failed to unfold 'Nat.add' at
+  x = 2 * y