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

@@ -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.

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