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

@@ -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)

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)

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