[Agda] possible unifier bug / explain error messages?

[Ulf Norell]

The problem is that _1 is frozen. After checking each set of mutually
recursive
definitions, any left-over metavariables are frozen, preventing them from
being
solved. In this case that means you can't solve metas in the module
telescope
using information from the module definitions.

It would indeed be nice if this was explained in the error message in some
way.

/ Ulf

On Wed, May 17, 2017 at 1:02 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> This looks like an Agda bug to me. If it's not, would someone please
> explain the error message? I'm confused especially (but not only) by the
> last line, "_1 = .Agda.Primitive.lzero". That should be pretty easy to
> solve uniquely, no?
>
> The code:
>
> postulate
>   set : Set
>   prop  : set → Set
>
> module _ x y where
>   postulate
>     _ : prop x
>     _ : prop y
>
> The error:
>
> Sort _1  [ at *.agda:5,10-11 ]
>> _2 : Set _1  [ at *.agda:5,10-11 ]
>> _7 : set  [ at *.agda:8,14-15 ]
>> _8 : set  [ at *.agda:8,14-15 ]
>>
>> ———— Errors ————————————————————————————————————————————————
>> Failed to solve the following constraints:
>>   _7 := (λ x y → x) [blocked on problem 4]
>>   [4] _2 =< set : (Set _1)
>>   _1 = .Agda.Primitive.lzero
>>
>>
>> _______________________________________________
> 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/20170517/76e99181/attachment.html>