[Agda] Decidable _\~~_ of Semiring

[Serge D. Mechveliani]

Please, what is wrong in the following program? 

(for  Agda-2.3.0.1, MAlonzo, lib-0.6,  lib-0.6 used heavily)

------------------------------------------------------------------------
...
open import Relation.Unary using ( Decidable )
open import Algebra using ( Semiring; module Semiring; ... 
                          )
open import Relation.Binary using
                           ( IsDecEquivalence; module IsDecEquivalence )  

test : {c l : Level} -> {R : Semiring c l} ->
       let open Semiring {{...}}
           C  = Carrier
       in
       C -> 
       IsDecEquivalence {A = C} _~~_ ->    -- (1)                   
       -- Decidable {A = C} _~~_ ->        -- (2)                     
       C

test x 
       isDE =   -- (1)                               
       -- eq =  -- (2)                                                    

               case eq x 0# of н╩ { (yes _) -> 0# ;  _ -> 1# }
               where
	       open Semiring {{...}}
               eq = IsDecEquivalence._?=_ isDE   -- (1)                   
------------------------------------------------------------------------

-- here I replace the math symbols as  \~~  ->  ~~,  \?=  ->  ?=

Now I need to simplify this varant (1) to variant (2).
Because  
1) IsDecEquivalence {A : Set A} _~~_  
   has the fields               isEquivalence : IsEquivalence _~~_
                                _?=_          : Decidable _~~_,

2) `test'  uses only the  field  ?=,
   it does not need checking   isEquivalence,  because it takes  _~~_  
   from  R : Semiring _ _,  
   and there  _~~_  is declared as an equivalence,
3) so, instead of  isDE,  `test'  needs only  
   eq : Decidable {A = C} _~~_,  where _~~_ is of R.  

Right?
So I comment out the three lines marked by  (1) 
and un-comment the two lines marked by      (2).
The checker reports

  (Semiring.Carrier R -> Set l) !=< (Set _540) of type
  (Set (L-suc l L-max c))
  when checking that the expression _~~_ has type (Carrier -> Set _540)

for the line of   " Decidable {A = C} _~~_ ->  " 

Skipping here {A = C} does not change this.

So, for  _~~_  taken from  R  we have that
1) _?=_ : Decidable _~~_   is accepted in  IsDecEquivalence 
2) Decidable _~~_          is rejected in the signature of `test'.

This looks like a contradiction. How to fix the variant (2) ?
Thank you in advance for explanation,

------
Sergei