fix: tryPureCoe?

src/Lean/Elab/Term.lean

@@ -620,11 +620,14 @@ def synthesizeInst (type : Expr) : TermElabM Expr := do
   | LOption.undef    => throwError! "failed to synthesize instance{indentExpr type}"
   | LOption.none     => throwError! "failed to synthesize instance{indentExpr type}"
 
+def isMonadApp (type : Expr) : TermElabM Bool := do
+  let some (m, _) ← isTypeApp? type | pure false
+  return (← isMonad? m) |>.isSome
+
 /--
   Try to coerce `a : α` into `m β` by first coercing `a : α` into ‵β`, and then using `pure`.
-  The method is only applied if one of the following cases hold:
-  - Head of `α` and head of ‵β` are not metavariables.
-  - Head of `α` is not a metavariable, and it is not a Monad.
+  The method is only applied if `α` is not monadic (e.g., `Nat → IO Unit`), and the head symbol
+  of the resulting type is not a metavariable (e.g., `?m Unit` or `Bool → ?m Nat`).
 
   The main limitation of the approach above is polymorphic code. As usual, coercions and polymorphism
   do not interact well. In the example above, the lift is successfully applied to `true`, `false` and `!y`
@@ -649,13 +652,11 @@ private def tryPureCoe? (errorMsgHeader? : Option String) (m β α a : Expr) : T
       pure (some aNew)
     catch _ =>
       pure none
-  let αHead := α.getAppFn
-  if !β.getAppFn.isMVar && !αHead.isMVar then
-    doIt -- case 1
-  else
-    let αIsMonad? ← isMonad? α
-    if !αHead.isMVar && αIsMonad?.isNone then
-      doIt -- case 2
+  forallTelescope α fun _ α => do
+    if (← isMonadApp α) then
+      pure none
+    else if !α.getAppFn.isMVar  then
+      doIt
     else
       pure none
 

tests/lean/pureCoeIssue.lean

@@ -0,0 +1,15 @@
+def f1 (x : Nat) : IO Unit := do
+  IO.println x
+  return ()
+
+def g1 : IO Unit := do
+  f1 -- Error
+  pure ()
+
+def f2 (x : Nat) (y : Nat) : IO Unit := do
+  IO.println s!"{x} {y}"
+  return ()
+
+def g2 : IO Unit := do
+  f2 10 -- Error
+  pure ()

tests/lean/pureCoeIssue.lean.expected.out

@@ -0,0 +1,16 @@
+pureCoeIssue.lean:6:2: error: application type mismatch
+  bind f1
+argument
+  f1
+has type
+  Nat → IO Unit
+but is expected to have type
+  IO ?m
+pureCoeIssue.lean:14:2: error: application type mismatch
+  bind (f2 10)
+argument
+  f2 10
+has type
+  Nat → IO Unit
+but is expected to have type
+  IO ?m

tests/lean/run/coeIssues4.lean

@@ -1,4 +1,4 @@
-
+--
 
 def f : List Int → Bool := fun _ => true
 
@@ -27,8 +27,7 @@ def ex4 :=
 def ex5 (xs : List String) :=
 xs.foldl (fun r x => r.push x) Array.empty
 
-set_option pp.all true
-
+set_option pp.all true in
 #check foo 1
 
 def ex6 :=