From ca0e6b0522e2948e8d819886be1e8fc106354947 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 9 Oct 2023 22:04:33 +1100
Subject: [PATCH] chore: fix MVarId.getType' (#2595)

* chore: fix MVarId.getType'

* add test
---
 src/Lean/Meta/Tactic/Util.lean    |  5 ++++-
 tests/lean/2505.lean              | 27 +++++++++++++++++++++++++++
 tests/lean/2505.lean.expected.out |  3 +++
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/2505.lean
 create mode 100644 tests/lean/2505.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index cc2e010278..e6fb759249 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -63,8 +63,11 @@ def getMVarType (mvarId : MVarId) : MetaM Expr :=
 
 /-- Get the type the given metavariable after instantiating metavariables and reducing to
 weak head normal form. -/
+-- The `instantiateMVars` needs to be on the outside,
+-- since `whnf` can unfold local definitions which may introduce metavariables.
+-- We don't need an `instantiateMVars` before the `whnf`, since it instantiates as necessary.
 def _root_.Lean.MVarId.getType' (mvarId : MVarId) : MetaM Expr := do
-  whnf (← instantiateMVars (← mvarId.getType))
+  instantiateMVars (← whnf (← mvarId.getType))
 
 @[deprecated MVarId.getType']
 def getMVarType' (mvarId : MVarId) : MetaM Expr := do
diff --git a/tests/lean/2505.lean b/tests/lean/2505.lean
new file mode 100644
index 0000000000..1121a06237
--- /dev/null
+++ b/tests/lean/2505.lean
@@ -0,0 +1,27 @@
+import Lean
+
+open Lean Elab Tactic Meta
+
+inductive A : Nat → Prop
+
+def Lean.MVarId.getType'' (mvarId : MVarId) : MetaM Expr := do
+  instantiateMVars (← whnf (← mvarId.getType))
+
+elab "the_target" : tactic => Tactic.withMainContext do
+  dbg_trace "target : {← (← getMainGoal).getType'}"
+  dbg_trace "target' : {← (← getMainGoal).getType''}"
+
+example : True := by
+  let p := A ?n
+  case n => exact 1
+  have : p := ?h
+  case h =>
+    the_target
+    sorry
+  sorry
+/-
+Prior to #2595, this gave:
+
+target : A ?_uniq.3033
+target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
+-/
diff --git a/tests/lean/2505.lean.expected.out b/tests/lean/2505.lean.expected.out
new file mode 100644
index 0000000000..6610d40a35
--- /dev/null
+++ b/tests/lean/2505.lean.expected.out
@@ -0,0 +1,3 @@
+target : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
+target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
+2505.lean:14:0-14:7: warning: declaration uses 'sorry'