diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 75b1c49044..d264d9e778 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1290,6 +1290,8 @@ fun stx expectedType? =>
     refTermType ← inferType refTerm;
     e ← elabTerm (stx.getArg 3) expectedType?;
     eType ← inferType e;
+    -- TODO: try coercions. We cannot simply use `ensureHasType` at this point because it has no support for the custom error message.
+    -- a `catch` would also not work since `ensureHasType` may postpone the coercion resolution.
     unlessM (isDefEq eType refTermType) $ throwError $ mkTypeMismatchError e eType refTermType msg;
     pure e
 
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index f098312ae5..854e625536 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -78,7 +78,7 @@ def find? (xs : List Nat) (p : Nat → Bool) : Option Nat := Id.run do
 let result := none
 for x in xs do
   if p x then
-    result := x
+    result := some x
     break
 return result