chore: fix MVarId.getType' (#2595)

* chore: fix MVarId.getType'

* add test

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

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))
+-/

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'