fix: unnecessary unfolding

src/Lean/Elab/App.lean

@@ -311,7 +311,6 @@ private def addEtaArg (k : M Expr) : M Expr := do
 private def finalize : M Expr := do
   let s ← get
   let mut e     := s.f
-  let mut eType := s.fType
   -- all user explicit arguments have been consumed
   trace[Elab.app.finalize]! e
   let ref ← getRef
@@ -320,7 +319,11 @@ private def finalize : M Expr := do
     registerMVarErrorImplicitArgInfo mvarId ref e
   if !s.etaArgs.isEmpty then
     e ← mkLambdaFVars s.etaArgs e
-    eType ← inferType e
+  /-
+    Remark: we should not use `s.fType` as `eType` even when
+    `s.etaArgs.isEmpty`. Reason: it may have been unfolded.
+  -/
+  let eType ← inferType e
   trace[Elab.app.finalize]! "after etaArgs, {e} : {eType}"
   match s.expectedType? with
   | none              => pure ()

tests/lean/unnecessaryUnfolding.lean

@@ -0,0 +1,11 @@
+import Lean
+open Lean
+
+abbrev M := StateRefT Nat IO
+
+def M.run (x : M α) (s := 0) : IO α :=
+  x.run' s
+
+variable (x : M Unit)
+
+#check id x.run

tests/lean/unnecessaryUnfolding.lean.expected.out

@@ -0,0 +1 @@
+id (M.run x 0) : IO Unit