[Agda] class inheritance

[Serge D. Mechveliani]

People,
this is on inheritance of `classes' (records), in Agda and in 
Standarad library (lib-0.6).

I am trying to use  Standarad library of lib-0.6.
One of its branch in the algebraic `class' (record) hierarchy ends with  
CommutativeRing.
And I am trying to define  GCDRing :
the extension of   CommutativeRing  with the operations (fields)

  canonicAssociate : Carrier -> Carrier
  gcd              : Carrier -> Carrier -> Carrier
  noZeroDivisors   : NoZeroDivisors _~_ _*_        -- property

(_~_  is the underlying equality, where I replace the math symbol with 
_~_).
I expected for this a syntax like the following 
(ignore the type levels, so far):

  record GCDRing : Set where
    inherit CommutativeRing    -- reexport operations from CommutativeRing
    field
      commutativeRing  : CommutativeRing
      canonicAssociate : Carrier -> Carrier
      gcd              : Carrier -> Carrier -> Carrier
      noZeroDivisors   : NoZeroDivisors _~_ _*_       -- property

Here  _~_  and  _*_  are operations (fields) taken from  CommutativeRing.
Is it possible to model this in Agda ?
If so, what could be a drawback?

If the user needs to extract from this data item  r,  for example,  
additiveGroup,  one writes
                    ((r.commutativeRing).ring).additiveGroup,

(is a record field extracted by `.' ?)
or may be, even writes  `r.additiveGroup',  
and some sugar extends this to  (r.commutativeRing).ring).additiveGroup  
-- assuming that the `path' from  GCDRing  to  additiveGroup  is unique.
     

But following the approach of                       module Algebra, 
I am forced to write it like this (ignore levels):

------------------------------------------------------------
record GCDRing : Set where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _~_
  field
    Carrier           : Set c
    _~_               : Rel Carrier 
    _+_               : Op2 Carrier
    _*_               : Op2 Carrier
    -_                : Op2 Carrier
    0#                : Carrier
    1#                : Carrier
    isCommutativeRing : IsCommutativeRing _~_ _+_ _*_ -_ 0# 1#

    -- proper part of GCDRing  ----------------
    commutativeRing  : CommutativeRing
    canonicAssociate : Carrier -> Carrier
    gcd              : Carrier -> Carrier -> Carrier
    noZeroDivisors   : NoZeroDivisors _~_ _*_
    -------------------------------------------

  open IsCommutativeRing isCommutativeRing public

  ring : Ring _ _
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open Ring ring public using (rawRing; +-group; +-abelianGroup)
  open CommutativeSemiring commutativeSemiring public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
  ...
  ...
----------------------------------------------------------------

To add  4 lines of a signature,  one needs to repeat  40 lines  of the 
lower level signatures.

If we take this approach of _copying and joining_ the signature at 
each class level, the definition for many higher classes in algebra 
will be too large:
  Ring  included  CommutativeRing  included  SyzygySolvableRing   
  included  GCDRing  included  FactorizationRing  included  Field 
  included  AbsoluteValueField ...

-- the source code size will grow exponentially in the class level.

Am I missing something?

Thank you in advance for explanation,

-------
Sergei