`withDuplicableCont` leaves continuation metavariable unassigned if `checkAssign` fails

[Rob23oba]

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

In withDuplicableCont, the result of checkedAssign is silently discarded, causing the continuation metavariable to stay unassigned in case of failure. This causes "declaration has metavariables" errors that are hard to debug.

Context

I encountered this while writing and debugging a doElem elaborator.

Steps to Reproduce

import Lean

syntax (name := testElem) "test" : doElem

open Lean Elab Do
@[doElem_elab testElem]
def elabTestElem : DoElab := fun _stx _dec => do
  return .fvar ⟨`bad_fvar⟩

@[doElem_control_info testElem]
def controlInfoTestElem : ControlInfoHandler := fun _stx => do
  return .pure

set_option backward.do.legacy false

/-- error: (kernel) declaration has metavariables 'testFn' -/
#guard_msgs in
def testFn : IO Unit := do
  if true then pure () else pure () -- uses `withDuplicableCont`
  test -- produces a term that `checkedAssign` will reject

set_option pp.mvars false

/--
info: def testFn : IO Unit :=
have __do_jp := ?_;
if true = true then __do_jp () else __do_jp ()
-/
#guard_msgs in
#print testFn

Expected behavior:
Either it gives some indication that something went wrong or assigns the metavariable unconditionally (such that you can see the problem, that is, the unknown free variable, when printing the declaration).

Actual behavior:
The metavariable is left in the body, discarding the entire elaborated term of test, making it hard to understand where the issue came from.

Versions

Lean 4.30.0-nightly-2026-03-05

Impact

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