[Agda] a strange function type report

[mechvel at scico.botik.ru]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.agda
Type: text/x-pascal
Size: 2902 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/bc71600d/attachment.bin>