[Agda] stuck with "unsolved metas"

[Andreas Abel]

I see, you are referring to

   https://github.com/agda/agda/issues/1079

In this instance, Agda inserts _too many_ hidden arguments, which it 
cannot solve then.  Sergei has run into this problem before, see

   https://github.com/agda/agda/issues/1092

This issue can only be finally settled by drastically restricting the 
use of hidden quantification, which would rule out many Agda programs 
which are legal at this point.  So we don't.

On 19.05.2016 04:34, Roman wrote:
> 2016-05-18 16:33 GMT+03:00, Andreas Abel <abela at chalmers.se>:
>> On 18.05.2016 13:30, Roman wrote:
>>> Sergei, try also
>>>
>>>       debug = \ {_ _ _} -> implic prime∣split
>>
>> Why should that help?
>
> I thought it could be an instance of the hidden lambda bug, but I now
> realize that such instance can only have form `h f` for some `h` and
> `f` that receives an implicit argument (right?). Then it type checks
> as `h (\ {_} -> f)`, but just `h f` results in an error, not in
> unsolved metas.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/