From 321ef5b9563154a35a85d3f4510490652bd5b0a5 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 27 Feb 2024 14:17:46 -0800
Subject: [PATCH] fix: make `Lean.Internal.liftCoeM` and `Lean.Internal.coeM`
 unfold (#3404)

The elaboration function `Lean.Meta.coerceMonadLift?` inserts these
coercion helper functions into a term and tries to unfolded them with
`expandCoe`, but because that function only unfolds up to
reducible-and-instance transparency, these functions were not being
unfolded. The fix here is to give them the `@[reducible]` attribute.
---
 src/Init/Coe.lean                 |  4 ++--
 tests/lean/coeM.lean              | 17 +++++++++++++++++
 tests/lean/coeM.lean.expected.out |  6 ++++++
 3 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/coeM.lean
 create mode 100644 tests/lean/coeM.lean.expected.out

diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index fb73ae1550b2..4e6adaed0faa 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -321,7 +321,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 This is used for coercions between monads, in the case where we want to apply
 a monad lift and a coercion on the result type at the same time.
 -/
-@[inline, coe_decl] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
+@[coe_decl] abbrev Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
     [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
   let a ← liftM x
   pure (CoeT.coe a)
@@ -331,7 +331,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 
 This is used for coercing the result type under a monad.
 -/
-@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
+@[coe_decl] abbrev Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
     [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
   let a ← x
   pure (CoeT.coe a)
diff --git a/tests/lean/coeM.lean b/tests/lean/coeM.lean
new file mode 100644
index 000000000000..b36b52d008e8
--- /dev/null
+++ b/tests/lean/coeM.lean
@@ -0,0 +1,17 @@
+/-
+# Testing monad lift coercion elaborator
+
+The functions inserted for the coercions are supposed to be inlined immediately during elaboration.
+-/
+
+variable (p : Nat → Prop) (m : IO (Subtype p))
+
+/-!
+`Lean.Internal.liftCoeM`
+-/
+#check (m : (ReaderT Int IO) Nat)
+
+/-!
+`Lean.Internal.coeM`
+-/
+#check (m : IO Nat)
diff --git a/tests/lean/coeM.lean.expected.out b/tests/lean/coeM.lean.expected.out
new file mode 100644
index 000000000000..d00b3a0716ba
--- /dev/null
+++ b/tests/lean/coeM.lean.expected.out
@@ -0,0 +1,6 @@
+do
+  let a ← liftM m
+  pure a.val : ReaderT Int IO Nat
+do
+  let a ← m
+  pure a.val : EIO IO.Error Nat