[Agda] record syntax error

[Serge D. Mechveliani]

Please, what is wrong in the attached program?

123 lines code in  Main.agda.zip  is attached to this letter.

This is for  Agda-2.3.2 made from source, MAlonzo, ghc-7.4.1.

It looks like the responsible fragment is 
(with a couple of math symbols changed)

---------------------------------------------------------------
record DMonoid (c l : Level) : Set (setoidLevel c l) where
  field
    semigroup : DSemigroup c l

  private  M     = DSemigroup.magma semigroup
           dS    = DSetoid.decSetoid $ Magma.setoid M
           S     = DecSetoid.setoid dS
           _*_   = Magma._*_ M
           mbU   = Magma.mbLeftUnity M
           justU = justLeftUnity mbU
  field
    hasUnity : justU === true

  unity : LeftUnity S _*_ 
  unity  with mbU | hasUnity
  ...  | leftUnity u | _ = u
  ...  | unknown     | ()

  e : Setoid.Carrier S
  e = LeftUnity.e unity 

  _~~_ = Setoid._~~_ S

  field  foo : e ~~ (e * e) 
---------------------------------------------------------------
 
`field' is intermingled 3 times with defining values,
the  foo  field uses  e,  and  e  is extracted from `unity',
`unity'  is defined ealier in this record.

The report is
-----------------------------
...
lation/Binary/InducedPreorders.agdai).
   Skipping Data.Colist (/home/mechvel/agda/lib-0.6/src/Data/Colist.agdai).
  Skipping Data.String (/home/mechvel/agda/lib-0.6/src/Data/String.agdai).
 Skipping IO.Primitive (/home/mechvel/agda/lib-0.6/src/IO/Primitive.agdai).

Missing definition for unity
-----------------------------

If we remove the line of  foo,  then the type checker becomes satisfied 
with the definition for `unity' (which, I think, is valid in both cases).

I wonder of whether I am stuck by this effect.

The code in  Main.agda  is contrived, obtained from the real one by 
removing its parts, as possible.

Regards,

------
Sergei

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 1339 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130102/0dda36c6/Main.agda.zip