<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>&quot;<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 -&gt; Nat<br><br>data A : Nat → Set where<br>  MkA : {n : Nat} -&gt; A n<br><br><br>macro<br>  myMacro : Term -&gt; Term -&gt; 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>&quot;<br><br><br></div>When typechecking this module, I obtain the following errors related to &quot;exampleDoesntWork&quot;:<br><br>&quot;<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>&quot;<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 &lt;<a href="mailto:j.p.pizaniflor@uu.nl" target="_blank">j.p.pizaniflor@uu.nl</a>&gt;<br></div>Promovendus - Departement Informatica<br></div>Faculteit Bètawetenschappen - Universiteit Utrecht<br></div></div></div>
</div></div></div></div></div>