[Agda] shared record parts

[Sergei Meshveliani]

People,
I am trying to find the main sources of type checking inefficiency in
the system of
(my library for algebra + Agda implementation).

Th investigation with  no-eta-equality + copatterns  has given nothing,
because the most interesting module is not type-checked, it is difficult
to understand, why. The module in close to end, the program is complex.

  
Another suspect is as follows.
My library has many parts like this:

 -----------------------------------------------------------
 module (commutativeRing : CommutativeRing _ _) 
   where
   open CommutativeRing commutativeRing using
                        (Carrier; *semigroup; *upSemigroup; 
                         *monoid; upRingoid; ring; upRing)
  
   f x =  g *semigroup

   f1 x = g1 *monoid

   f2 x = g2 ring
   ... 
 ------------------------------------------------------------

And the imported record instances  *semigroup; *upSemigroup; 
*monoid; upRingoid; ring; upRing
present a tower, some of the tower levels include some others as record
field values. 
These record types also carry some implementation in them.
Then,  (f x), (f1 x), (f2 x) ...  take as arguments the parts of this
tower.  
Thus,  f2 analyzes  ring (to some depth),  f analyzes *semigroup (to
some depth), and *semigroup is a considerable part of this  ring.  
There appears the question of how sharing and laziness work in such
examples: how eagerly the structure of *semigroup will be copied, 
what happens when this data becomes un-referenced, and so on.
Is it like in GHC ?
   
I program such modules in Agda as I did it in Haskell + GHC for symbolic
computation and for a term rewriting library. And with GHC, I am sure
that it this example it will unwind the parts of  ring and *semigroup
in the lazy style, and with sharing. So that in computation, the term
data will not blow up to surprise me much. And if it does, then I am
able to find the source and to fix my program. 
The Agda type checker may evaluate in another way, not similarly to how
it evaluates a GHC-compiled program. 
So, I wonder.

Regards,

------
Sergei