From 33cbd99bcdc4d45d8fc939f69d5ad3ec8ddcae4b Mon Sep 17 00:00:00 2001
From: Rob23oba <robin.arnez@web.de>
Date: Tue, 9 Jun 2026 16:09:20 +0200
Subject: [PATCH 1/2] fix mkBindUnlessPure calling continuation twice

---
 src/Lean/Elab/Do/Basic.lean |  4 ++--
 tests/elab/13858.lean       | 31 +++++++++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/elab/13858.lean

diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 29330123cc41..e4faf5de9edd 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -562,9 +562,9 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         return (isPure, isDuplicable)
       if isPure then
         if isDuplicable then
-          return ← mapLetDeclZeta (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k
+          return ← body.replaceFVarsM #[xFVar] #[eRes]
         -- else -- would be too aggressive
-        --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
+        --   return ← body.replaceFVarsM #[xFVar] #[eRes]
 
     let body ← Term.ensureHasType (← mkMonadApp kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
diff --git a/tests/elab/13858.lean b/tests/elab/13858.lean
new file mode 100644
index 000000000000..ef6681afd833
--- /dev/null
+++ b/tests/elab/13858.lean
@@ -0,0 +1,31 @@
+/-!
+Test for https://github.com/leanprover/lean4/issues/13858
+
+Repeating `pure ()`s should scale linearly.
+-/
+
+set_option backward.do.legacy false
+
+set_option maxHeartbeats 1000
+
+def test : IO Unit := do
+  pure () -- 1
+  pure () -- 2
+  pure () -- 3
+  pure () -- 4
+  pure () -- 5
+  pure () -- 6
+  pure () -- 7
+  pure () -- 8
+  pure () -- 9
+  pure () -- 10
+  pure () -- 11
+  pure () -- 12
+  pure () -- 13
+  pure () -- 14
+  pure () -- 15
+  pure () -- 16
+  pure () -- 17
+  pure () -- 18
+  pure () -- 19
+  pure () -- 20

From f65bf273997cce3806d5f2f630497ec86c1e74f1 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 14 Oct 2026 07:53:50 +0000
Subject: [PATCH 2/2] chore: remove stale commented-out code in
 mkBindUnlessPure

---
 src/Lean/Elab/Do/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index e4faf5de9edd..ae2bf2d971a0 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -563,8 +563,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
       if isPure then
         if isDuplicable then
           return ← body.replaceFVarsM #[xFVar] #[eRes]
-        -- else -- would be too aggressive
-        --   return ← body.replaceFVarsM #[xFVar] #[eRes]
 
     let body ← Term.ensureHasType (← mkMonadApp kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body