diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index fb73ae1550..4e6adaed0f 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 0000000000..b36b52d008
--- /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 0000000000..d00b3a0716
--- /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