Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

A do block that only consists of pure ()s take a time exponential in the amount pure ()s. This is due to mkBindUnlessPure running the continuation twice, even if it is non-duplicable.

Context

Observing a non-duplicable continuation get run twice.

Steps to Reproduce

set_option backward.do.legacy false

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

Expected behavior:
The time it takes to elaborate test is roughly twice as much as if there were 7 pure ()s (i.e. negligible).

Actual behavior:
test takes multiple seconds to elaborate, roughly twice as much as if there were 13 pure ()s.

Versions

Lean 4.31.0, commit 2cd9863

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.