[Agda] "not in scope" without "does not export"

[mechvel at scico.botik.ru]

Dear Agda developers,

For the below program
(not self-contained, non-standard records for algebra)

Agda 2.6.1 reports
"Not in scope:
   Foo
".

May be, it rather needs to report
"The module OfCommutativeMonoid  does not export commutativeSemigroup"
?
(the word `public' is missed in the code).


module OfCommutativeMonoid (CM : CommutativeMonoid) where
   open CommutativeMonoid CM using (commutativeSemigroup)

module OfSemiring (R : Semiring) where
   open Semiring R using (+-commutativeMonoid)

module OfCommutativeSemiring (R : CommutativeSemiring)
   where
   open CommutativeSemiring R using (*-commutativeMonoid)
   open OfCommutativeMonoid *-commutativeMonoid using ()
                            renaming (commutativeSemigroup to Foo)

   debug : CommutativeSemigroup
   debug = Foo


Regards,

------
Sergei