[Agda] possible unifier bug / explain error messages?

[Andreas Abel]

One question here is of course when we should freeze the module 
telescope.  Alternatively, it could be frozen only after the module has 
been checked entirely.

The current behavior is not very nice: Agda should at least emit a 
warning that the frozen metas will never be instantiated in cases like

   module _ x y where

where no interaction metas are involved.

On 17.05.2017 09:36, Ulf Norell wrote:
> 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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> 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://www.cse.chalmers.se/~abela/