diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 2bf15f5001..1c8e813172 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1216,7 +1216,8 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : withNestedTraces do let env ← getEnv match (← liftMacroM (expandMacroImpl? env stx)) with - | some (decl, Except.ok stxNew) => + | some (decl, stxNew?) => + let stxNew ← liftMacroM <| liftExcept stxNew? withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <| withMacroExpansion stx stxNew <| withRef stxNew <| diff --git a/tests/lean/macroError.lean b/tests/lean/macroError.lean new file mode 100644 index 0000000000..d81ed4b1bc --- /dev/null +++ b/tests/lean/macroError.lean @@ -0,0 +1,3 @@ +macro "foo" : term => Lean.Macro.throwError "Test Error" + +#check foo diff --git a/tests/lean/macroError.lean.expected.out b/tests/lean/macroError.lean.expected.out new file mode 100644 index 0000000000..c6ebf13697 --- /dev/null +++ b/tests/lean/macroError.lean.expected.out @@ -0,0 +1 @@ +macroError.lean:3:7-3:10: error: Test Error