<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Can you find the error in this code :</div><div><br></div><div>```agda</div><div><br></div><div>module test where<br><br>open import Agda.Builtin.Reflection<br>open import Reflection<br>open import Prelude.Nat<br>open import Prelude.Bool<br>open import Prelude.Unit<br>open import Prelude.List<br><br>pat : Term<br>pat = pat-lam [ clause [ arg (arg-info visible relevant) (var "ii") ] (def (quote Bool) []) ] [ arg (arg-info visible relevant) (var 0 []) ]<br><br>macro<br>  mm : Term → TC ⊤<br>  mm hole<br>    = do<br>         inContext (arg (arg-info visible relevant) (def (quote Nat) []) ∷ [])<br>           (do<br>               t ← reduce pat<br>               typeError (termErr t ∷ termErr pat ∷ [])<br>                    )<br><br>test : ⊤<br>test = mm</div><div>```</div><div><br></div><div>Why do I get a meta instead of actually reducing :</div><div>```</div><div>.../test.agda:27,8-10<br>_22 _ (λ { ii → Bool }) _<br>when checking that the expression unquote mm has type ⊤</div><div>```<br></div></div></div></div>