fix: avoid unnecessary unfolding at do

src/Lean/Elab/Do.lean

@@ -93,21 +93,36 @@ private def mkIdBindFor (type : Expr) : TermElabM ExtractMonadResult := do
   let idBindVal := Lean.mkConst `Id.hasBind [u]
   pure { m := id, hasBindInst := idBindVal, α := type, expectedType := mkApp id type }
 
-private def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
+private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
   match expectedType? with
   | none => throwError "invalid 'do' notation, expected type is not available"
   | some expectedType =>
-    let type ← withReducible $ whnf expectedType
-    if  type.getAppFn.isMVar then throwError "invalid 'do' notation, expected type is not available"
-    match type with
-    | Expr.app m α _ =>
-      try
-        let bindInstType ← mkAppM `Bind #[m]
-        let bindInstVal  ← synthesizeInst bindInstType
-        pure { m := m, hasBindInst := bindInstVal, α := α, expectedType := expectedType }
-      catch _ =>
-        mkIdBindFor type
-    | _ => mkIdBindFor type
+    let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
+      match type with
+      | Expr.app m α _ =>
+        try
+          let bindInstType ← mkAppM `Bind #[m]
+          let bindInstVal  ← Meta.synthInstance bindInstType
+          return some { m := m, hasBindInst := bindInstVal, α := α, expectedType := expectedType }
+        catch _ =>
+          return none
+      | _ =>
+        return none
+    let rec extract? (type : Expr) : MetaM (Option ExtractMonadResult) := do
+      match (← extractStep? type) with
+      | some r => return r
+      | none =>
+        let typeNew ← whnfCore type
+        if typeNew != type then
+          extract? typeNew
+        else
+          if typeNew.getAppFn.isMVar then throwError "invalid 'do' notation, expected type is not available"
+          match (← unfoldDefinition? typeNew) with
+          | some typeNew => extract? typeNew
+          | none => return none
+    match (← extract? expectedType) with
+    | some r => return r
+    | none   => mkIdBindFor expectedType
 
 namespace Do
 

tests/lean/doErrorMsg.lean.expected.out

@@ -3,7 +3,7 @@ doErrorMsg.lean:3:2-3:13: error: type mismatch
 has type
   EIO IO.Error IO.FS.Stream : Type
 but is expected to have type
-  EIO IO.Error PUnit : Type
+  IO PUnit : Type
 doErrorMsg.lean:15:19-15:21: error: type mismatch
   f1
 has type

tests/lean/doIssue.lean.expected.out

@@ -3,13 +3,13 @@ doIssue.lean:2:2-2:3: error: type mismatch
 has type
   Nat : Type
 but is expected to have type
-  EIO IO.Error PUnit : Type
+  IO PUnit : Type
 doIssue.lean:10:2-10:13: error: type mismatch
   Array.set! xs 0 1
 has type
   Array Nat : Type
 but is expected to have type
-  EIO IO.Error PUnit : Type
+  IO PUnit : Type
 doIssue.lean:18:2-18:20: error: application type mismatch
   pure (Array.set! xs 0 1)
 argument

tests/lean/doNotation1.lean.expected.out

@@ -27,7 +27,7 @@ doNotation1.lean:51:0-51:13: error: type mismatch
 has type
   EIO IO.Error (IO.Ref Bool) : Type
 but is expected to have type
-  EIO IO.Error Unit : Type
+  IO Unit : Type
 doNotation1.lean:58:2-58:20: error: type mismatch, result value has type
   Unit : Type
 but is expected to have type

tests/lean/eagerUnfoldingIssue.lean

@@ -0,0 +1,15 @@
+import Lean
+
+namespace Lean.Elab
+
+def f1 (x : Nat) : MetaM Unit := do
+  logInfo m!"{x}"
+  pure ()
+
+abbrev M := MetaM Unit
+
+def f2 (x : Nat) : M := do
+  logInfo m!"{x}"
+  pure ()
+
+end Lean.Meta

tests/lean/eagerUnfoldingIssue.lean.expected.out

@@ -0,0 +1,5 @@
+eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize instance
+  MonadLog MetaM
+eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize instance
+  MonadLog MetaM
+eagerUnfoldingIssue.lean:15:0-15:13: error: invalid 'end', name mismatch

tests/lean/pureCoeIssue.lean.expected.out

@@ -3,10 +3,10 @@ pureCoeIssue.lean:6:2-6:4: error: type mismatch
 has type
   Nat → IO Unit : Type
 but is expected to have type
-  EIO IO.Error PUnit : Type
+  IO PUnit : Type
 pureCoeIssue.lean:14:2-14:7: error: type mismatch
   f2 10
 has type
   Nat → IO Unit : Type
 but is expected to have type
-  EIO IO.Error PUnit : Type
+  IO PUnit : Type