[Agda] inferType yields a metavariable

[Martin Stone Davis]

Is there some way to infer-the-goal as 'Set' in foo (below)? I mean to do
this within the tactic, not by providing implicits to id. Currently,
infer-the-goal reports the goal as _n (some metavariable).

  open import Prelude
  open import Builtin.Reflection

  macro
    infer-the-goal : Tactic
    infer-the-goal hole = inferType hole >>= λ goal → typeError (termErr
goal ∷ [])

  foo : Set
  foo = id infer-the-goal

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160225/8c0ab49f/attachment.html