[Agda] inferType yields a metavariable

[Martin Stone Davis]

Thanks, that worked. But how about this slightly-more-complicated example?
If I remove "id", the goal gets reported as _n → Set, which is fine for me,
since I just care about seeing that it's 'Set'. However, with "id", it's _n
→ _m. I'm not finding that blockOnMeta helps here.

    open import Prelude
    open import Tactic.Reflection

    macro
      infer-the-goal₂ : Tactic
      infer-the-goal₂ hole = do
        goal ← forceFun =<< inferType hole -|
        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

On Thu, Feb 25, 2016 at 9:41 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> Try blockOnMeta if it comes back a meta.
>
> / Ulf
> On Fri, 26 Feb 2016 at 06:38, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> 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
>> _______________________________________________
>> 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/20160225/db804b51/attachment.html