[Agda] boundings in data-where

[Serge D. Mechveliani]

People,
there is a strange syntax difference between the `record' and `data'
declarations with respect to bounding and `open' after `where'.
Consider the example: 

------------------------------------------------------------------------
record LeftQuotient {c l : Level} (H : Semigroup c l)
                    (a b : Semigroup.Carrier H) :  Set (max c l)
  where
  open Semigroup {{...}}     -- (1)
  _~_ = Semigroup._\~~_ H    -- (2)
  field 
    quot : Semigroup.Carrier H
    ...

data MbDivideLeft {c l : Level} (H : Semigroup c l)
     (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) : Set (max c l)
  where
  open Semigroup {{...}}     -- (1')
  _~_ = Semigroup._\~~_ H    -- (2')
  ...
  unsolvable :
             (x : Carrier H) -> \neg ((x * b) ~ a) -> MbDivideLeft H a b
  ...
------------------------------------------------------------------------

The lines (1) and (2) do work,  while (1') and (2') do not parse.
Has it sense to make this feature in `data' similar as in 'record' ? 

Thanks,
Sergei.