From 3f720d778cf9b267a6545c661e26ee77afdb5f83 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Nov 2020 13:08:18 -0800
Subject: [PATCH] fix: unnecessary unfolding

---
 src/Lean/Elab/App.lean                            |  7 +++++--
 tests/lean/unnecessaryUnfolding.lean              | 11 +++++++++++
 tests/lean/unnecessaryUnfolding.lean.expected.out |  1 +
 3 files changed, 17 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/unnecessaryUnfolding.lean
 create mode 100644 tests/lean/unnecessaryUnfolding.lean.expected.out

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