[Agda] a strange function type report

[mechvel at scico.botik.ru]

Sorry, here is attached a much smaller program, which is also zipped.
The effect is the same as reported below.


On 2020-04-24 22:21, mechvel at scico.botik.ru wrote:
> Please, what is wrong in the attached program?
> 
> In one module it is declared
> 
>   Prime∣split :  Set _
>   Prime∣split =  {p a b : Carrier} → IsPrime p → p ∣ (a * b) → p ∣ a ⊎ 
> p ∣ b
> 
> and in the last module it is implemented
> 
>   test : (p x y : Carrier) → IsPrime p → p ∣ (x * y) → (p ∣ x) ⊎ (p ∣ 
> y)
>   test p x y p-prime p∣xy =  Prime∣split p-prime p∣xy
> 
> And Agda 2.6.1 reports
> "
> Set (α ⊔ α=) should be a function type, but it isn't
> when checking that p-prime p∣xy are valid arguments to a function
> of type Set (α ⊔ α=)
> ".
> 
> Am I missing something, or it is a bug in the type checker?
> 
> Regards,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.agda.zip
Type: application/zip
Size: 738 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/4f5b6b0b/attachment.zip>