<div dir="ltr">The problem is that Term arguments to macros are not allowed to have unsolved metavariables, so you never even get to run the macro. It's waiting for the implicit argument to MkA to be resolved before quoting it. You can fix this by doing the quoting yourself in the macro:<div><br></div><div><div> myMacro : {X : Set} -> X -> Term -> TC ⊤</div><div> myMacro a qhole =</div><div> bindTC (inferType qhole) \ tyH →</div><div> bindTC (quoteTC a) \ `a →</div><div> unify qhole `a</div></div><div><br></div><div>(Aside: you don't need the checkType, unify does type checking before unification)</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Nov 8, 2016 at 4:17 PM, João Paulo Pizani Flor <span dir="ltr"><<a href="mailto:J.P.PizaniFlor@uu.nl" target="_blank">J.P.PizaniFlor@uu.nl</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hi everyone,<br><br></div>I have an issue currently when trying to use reflection-based macros: I want to pass as argument to a macro a constructor of an indexed datatype, with the index as implicit argument. Given the specified type signature, I was expecting that applying the macro would resolve the implicit argument, but this does not seem to be the case.<br><br></div>The minimal example which I have come up with is:<br><br>"<br>module ExampleExpectedUnification where<br><br>open import Agda.Builtin.Unit using (⊤)<br>open import Agda.Builtin.Reflection using (Term; TC; inferType; bindTC; checkType; unify)<br><br>data Nat : Set where<br> Zero : Nat<br> Succ : Nat -> Nat<br><br>data A : Nat → Set where<br> MkA : {n : Nat} -> A n<br><br><br>macro<br> myMacro : Term -> Term -> TC ⊤<br> myMacro a qhole =<br> bindTC (inferType qhole) (\ tyH → bindTC (checkType a tyH) (\ aChk → unify qhole aChk))<br><br>exampleWorks : A Zero<br>exampleWorks = myMacro (MkA {Zero})<br><br>exampleDoesntWork : A Zero<br>exampleDoesntWork = myMacro MkA<br>"<br><br><br></div>When typechecking this module, I obtain the following errors related to "exampleDoesntWork":<br><br>"<br>_28 : A Zero [ at /data/data/priv/phd/<wbr>playground/<wbr>ExampleExpectedUnification.<wbr>agda:23,21-32 ]<br>_n_31 : Nat [ at /data/data/priv/phd/<wbr>playground/<wbr>ExampleExpectedUnification.<wbr>agda:23,29-32 ]<br>_33 : Term [ at /data/data/priv/phd/<wbr>playground/<wbr>ExampleExpectedUnification.<wbr>agda:23,29-32 ]<br>_35 : A Zero [ at /data/data/priv/phd/<wbr>playground/<wbr>ExampleExpectedUnification.<wbr>agda:23,29-32 ]<br><br>———— Errors ——————————————————————————————<wbr>——————————————————<br>Failed to solve the following constraints:<br> [0] _34 := unquote (myMacro _33)<br> [0] _32 := quoteTerm MkA :? Term<br>"<br><div><br><br></div><div>Can anyone understand what is happening is this situation, and if I can somehow make this implicit argument of MkA be resolved in the macro?<br><br></div><div>Thanks,<br></div><div><div><div><div><br clear="all"><div><div class="m_-5549828878288999858gmail_signature"><div dir="ltr"><div><div>João Pizani, M.Sc <<a href="mailto:j.p.pizaniflor@uu.nl" target="_blank">j.p.pizaniflor@uu.nl</a>><br></div>Promovendus - Departement Informatica<br></div>Faculteit Bètawetenschappen - Universiteit Utrecht<br></div></div></div>
</div></div></div></div></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>