[Agda] stuck with "unsolved metas"

[Roman]

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.