[Agda] `where' in type

[Serge D. Mechveliani]

People,
I have a question about the code

  record CommutativeRing2 c l : Set (suc (max c l))
    where
    open CommutativeRing
    field
      commutativeRing : CommutativeRing c l
      fromInt         : Integer -> Carrier commutativeRing
      divMb           : (Carr -> Carr -> Carr) 
                        where
                        Carr = Carrier commutativeRing   

(the math symbols are replaced, in order to make this e-mail
readable:   max := \lub,  Integer := \bz).

This is under  Agda-2.3.0.1 + lib-0.6,
and it relies on the Algebra part of Standard library:  uses 
CommutativeRing.

The Doc sais that a  record field type  my depend on other field values,
and I use this in the declarations for  fromInt, divMb.
Hence, one has a hope that `let' and `where' are allowed in such a 
dependency.  
But this declaration for  divMb  causes  Parse error  -- at `where'.

Replacing it with 
                  divMb : (let Carr = Carrier commutativeRing   
                           in  Carr -> Carr -> Carr)  
makes it compiled.

Why 'where' is not so lucky here as `let' ?

Apart of the `where' question:
currently I think that the best is the following approach with multiple
`field' parts.

  record CommutativeRing2 c l : Set ...  where
    field
      commutativeRing : CommutativeRing c l

    Carr : Set _
    Carr = CommutativeRing.Carrier commutativeRing

    field
      fromInt : Integer -> Carr
      divMb   : Carr -> Carr -> Maybe Carr
      isCommutativeRing2 : ...

It is compiled, and I hope that this code is reliable
(its idea is to avoid copying operation names from a superclass). 

Thanks,

------
Sergei