[Agda] possible unifier bug / explain error messages?

[Martin Stone Davis]

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
>
>