From a0f2a8bf60e83938ad16b8e6479bde9705fa899b Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Mon, 13 Apr 2026 21:32:43 +0200
Subject: [PATCH] fix: improve error for join point assignment failure in do
 elaborator (#13397)

This PR improves error reporting when the `do` elaborator produces an
ill-formed expression that fails `checkedAssign` in
`withDuplicableCont`. Previously the failure was silently discarded,
making it hard to diagnose bugs in the `do` elaborator. Now a
descriptive error is thrown showing the join point RHS and the
metavariable it failed to assign to.

Closes #12826
---
 src/Lean/Elab/Do/Basic.lean |  5 ++++-
 tests/elab/issue12826.lean  | 27 +++++++++++++++++++++++++++
 2 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 tests/elab/issue12826.lean

diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 891217489b..1d2bb025fa 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -545,7 +545,10 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
-  discard <| joinRhsMVar.mvarId!.checkedAssign joinRhs
+  unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
+    joinRhsMVar.mvarId!.withContext do
+      throwError "Bug in a `do` elaborator. Failed to assign join point RHS{indentExpr joinRhs}\n\
+        to metavariable\n{joinRhsMVar.mvarId!}"
 
   let body ← body?.getDM do
     -- Here we unconditionally add a pending MVar.
diff --git a/tests/elab/issue12826.lean b/tests/elab/issue12826.lean
new file mode 100644
index 0000000000..ca2a5bfd29
--- /dev/null
+++ b/tests/elab/issue12826.lean
@@ -0,0 +1,27 @@
+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: Bug in a `do` elaborator. Failed to assign join point RHS
+  fun __r => bad_fvar
+to metavariable
+⊢ Unit → IO Unit
+-/
+#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