[Agda] Macro not resolving implicit arguments as wished

[João Paulo Pizani Flor]

Hi everyone,

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.

The minimal example which I have come up with is:

"
module ExampleExpectedUnification where

open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.Reflection using (Term; TC; inferType; bindTC;
checkType; unify)

data Nat : Set where
  Zero : Nat
  Succ : Nat -> Nat

data A : Nat → Set where
  MkA : {n : Nat} -> A n


macro
  myMacro : Term -> Term -> TC ⊤
  myMacro a qhole =
    bindTC (inferType qhole) (\ tyH → bindTC (checkType a tyH) (\ aChk →
unify qhole aChk))

exampleWorks : A Zero
exampleWorks = myMacro (MkA {Zero})

exampleDoesntWork : A Zero
exampleDoesntWork = myMacro MkA
"


When typechecking this module, I obtain the following errors related to
"exampleDoesntWork":

"
_28 : A Zero  [ at
/data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,21-32 ]
_n_31 : Nat  [ at
/data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]
_33 : Term  [ at
/data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]
_35 : A Zero  [ at
/data/data/priv/phd/playground/ExampleExpectedUnification.agda:23,29-32 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  [0] _34 := unquote (myMacro _33)
  [0] _32 := quoteTerm MkA :? Term
"


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?

Thanks,

João Pizani, M.Sc <j.p.pizaniflor at uu.nl>
Promovendus - Departement Informatica
Faculteit Bètawetenschappen - Universiteit Utrecht
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161108/8a4da680/attachment.html