[Agda] inferType yields a metavariable

[Ulf Norell]

Hmm, that's trickier. It's the forceFun that makes it possible to solve the
target type, but when you blockOnMeta you lose that work. Not sure what's
needed to make this work.

/ Ulf

On Fri, Feb 26, 2016 at 8:40 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> 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/20160226/87bfe5a4/attachment-0001.html