a0f2a8bf60
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
27 lines
651 B
Text
27 lines
651 B
Text
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
|