[Agda] no-field record

[Serge D. Mechveliani]

People,
I have a beginner question about a  record with no `field':

  record Foo (foo1 : Bool) : Set _ where  
                                   foo2 : Bool
                                   foo2 = not foo1
                                   foo3 : Foo3 
                                   foo3 = ...
                                   ...
                                   foo9 : Foo9
                                   foo9 = ...

I use it like this:  let r : Foo true
                         r = _
                     in  Foo.foo9 r

1. One of this style records is type-checked but not compiled 
   -- of which I have recently reported on Agda-2.3.2 MAlonzo.

2. Are parameterized modules better to use than such records?
   (as I recall, modules are not first class data).

Thanks,

------
Sergei