From e21ea536617a912f746dd0b79c6e70e9f167d6fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Dec 2020 09:42:27 -0800
Subject: [PATCH] fix: position of `failed to synthesize toStream ...` error

---
 src/Lean/Elab/Do.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index c2ae7cd465..0528fe1fc3 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1340,8 +1340,10 @@ mutual
       let doForDecls := doForDecls.eraseIdx 1
       let body := doFor[3]
       withFreshMacroScope do
+        let toStreamFn ← `(toStream)
+        let toStreamFn := toStreamFn.copyInfo ys
         let auxDo ←
-          `(do let mut s := toStream $ys
+          `(do let mut s := $toStreamFn:ident $ys
                for $doForDecls:doForDecl,* do
                  match Stream.next? s with
                  | none => break