Exponential time growth when repeating `pure ()`

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 2cd98639c40d2d2a026dd599093b70f55f55ffaf

Impact

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

Start by reproducing the minimal test definition with backward.do.legacy false, then inspect mkBindUnlessPure, which the issue identifies as running the continuation twice. Done means elaboration time no longer grows exponentially with repeated pure () expressions while the affected do block still elaborates correctly.