[Agda] question on parametric modules

[Sergei Meshveliani]

Dear Agda developers,

  http://www.botik.ru/pub/local/Mechveliani/agdaNotes/rep-nov9-2014.zip 

contains a program (a full code of  23K byte archive, not so large). 
It which uses parametric modules and records in them.
It produces the following strange effect.


unzip,   emacs Subclasses1.agda,  Ctrl-C Ctrl-l


Agda 2.4.2  reports that the last occurrence of  subDSet
            has a wrong type.

Then,  comment out the line  (1)  in Subclasses1.agda
       and  un-comment the two lines  (2).

This way it is type-checked.


Why is there such a difference between

    open SubmonPack-inst.Submonoid submonoid using (subDSet)
and
    subDSet : SubDSet upDSet
    subDSet = SubmonPack-inst.Submonoid.subDSet submonoid
?

These two ways to obtain  subDSet  need to be equivalent.

(I rather need `open', because there are several values to take from
there).

See  Subclasses1.agda  for the parametric modules and records involved.

Is this a bug in Adga ?

Thanks,

------
Sergei