<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/playground/ExampleExpectedUnification.agda:23,21-32 ]<br>_n_31 : Nat [ at /data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]<br>_33 : Term [ at /data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]<br>_35 : A Zero [ at /data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]<br><br>———— Errors ————————————————————————————————————————————————<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="gmail_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>