diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index ea646b6181..54349a16f1 100644
--- a/src/Lean/Elab/Do.lean
+++ b/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
 
diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out
index 2005434ee7..4c1a36742d 100644
--- a/tests/lean/doErrorMsg.lean.expected.out
+++ b/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
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
index 17e7fdff93..d59f9e7ddb 100644
--- a/tests/lean/doIssue.lean.expected.out
+++ b/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
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 2f4c492518..32b6253ca4 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/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
diff --git a/tests/lean/eagerUnfoldingIssue.lean b/tests/lean/eagerUnfoldingIssue.lean
new file mode 100644
index 0000000000..a109ab33f3
--- /dev/null
+++ b/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
diff --git a/tests/lean/eagerUnfoldingIssue.lean.expected.out b/tests/lean/eagerUnfoldingIssue.lean.expected.out
new file mode 100644
index 0000000000..ebfdd36f89
--- /dev/null
+++ b/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
diff --git a/tests/lean/pureCoeIssue.lean.expected.out b/tests/lean/pureCoeIssue.lean.expected.out
index 76c9f0630d..65337b027a 100644
--- a/tests/lean/pureCoeIssue.lean.expected.out
+++ b/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