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