diff --git a/Qq/Macro.lean b/Qq/Macro.lean index 5e3a250..1ba58de 100644 --- a/Qq/Macro.lean +++ b/Qq/Macro.lean @@ -463,6 +463,7 @@ def Impl.macro (t : Syntax) (expectedType : Expr) : TermElabM Expr := do if ← synth.isAssigned then let t ← synth.synth s unless ← isDefEq mvar t do + tryPostpone throwError "cannot assign metavariable ({mvar} : {← inferType mvar}) with {t}" instantiateMVars mainMVar