[Agda] Macro not resolving implicit arguments as wished

[Ulf Norell]

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:

  myMacro : {X : Set} -> X -> Term -> TC ⊤
  myMacro a qhole =
    bindTC (inferType qhole) \ tyH →
    bindTC (quoteTC a) \ `a →
    unify qhole `a

(Aside: you don't need the checkType, unify does type checking before
unification)

/ Ulf

On Tue, Nov 8, 2016 at 4:17 PM, João Paulo Pizani Flor <J.P.PizaniFlor at uu.nl
> wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161109/139311ca/attachment.html