diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 79d3948b1a..9b17490e48 100644
--- a/src/Lean/Elab/App.lean
+++ b/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 ()
diff --git a/tests/lean/unnecessaryUnfolding.lean b/tests/lean/unnecessaryUnfolding.lean
new file mode 100644
index 0000000000..b18a1575e9
--- /dev/null
+++ b/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
diff --git a/tests/lean/unnecessaryUnfolding.lean.expected.out b/tests/lean/unnecessaryUnfolding.lean.expected.out
new file mode 100644
index 0000000000..d275926ae9
--- /dev/null
+++ b/tests/lean/unnecessaryUnfolding.lean.expected.out
@@ -0,0 +1 @@
+id (M.run x 0) : IO Unit