[Agda] "Hiding of record parameters leads ..."

[Sergei Meshveliani]

Hello,

This is on the bug fix for  
"Hiding of record parameters leads to hiding mismatch in
checkInternal" (#1759).

The effect for my DoCon-A application is that I need to write
   
    module MgIsoPair = MagmaIsomorphismPair {upMagma = upMagma}
                                            {upMagma' = upMagma'}
instead of
    module MgIsoPair = MagmaIsomorphismPair upMagma upMagma' 

for  record MagmaIsomorphismPair : Set _ where ...

defined in
   module _ {α α= β β=} (upMagma : UpMagma α α=) 
                        (upMagma' : UpMagma β β=)  where
     ...

There are the two similar places in the current program, where one needs
to write   {foo = <foo-inst>}  instead of  <foo-inst>.

Probably, fixing the bug costs this minor complication.

Regards,

------
Sergei