[Agda] How to obtain the reflected goal?

[Liang-Ting Chen]

Hi all,

Based on Language Reference, I expect that the following fragment

macro
  showGoal : Term → TC ⊤
  showGoal hole =
    (inferType hole) >>= λ goal → typeError [ termErr goal ]


binds the reflected goal to `goal`, but I always get a meta-variable
instead even if the goal is simply ℕ. Is this the expected behaviour?

-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190420/cad93fa9/attachment.html>