[Agda] lost fixity of ≈

[mechvel at scico.botik.ru]

Dear Agda team,

This is on  Development Agda of December, 2018,  ghc-8.02.

In the below program, the priority of the _≈_ operator is lost,
so that  "0# + 0# ≈ 0#"  is not parsed.

---------------------------------------------------
open import Relation.Binary using (Decidable)
open import Algebra         using (Ring)

module _ {α α=} (R : Ring α α=)
                 (let _≈_ = Ring._≈_ R)      -- I
                 (_≟_ : Decidable _≈_)       -- II
   where
   open Ring R using (0#; _+_)

   postulate  test :  0# + 0# ≈ 0#
---------------------------------------------------

Is this a bug in Agda ?

If we replace (I) with  "(open Ring R using (_≈_))",
then it improves.

Regards,

------
Sergei