[Agda] `where' scope

[Serge D. Mechveliani]

People,	
how does this occur that `where' does not protect its local scope?
Thus, for
  f : Nat -> Nat
  f = suc
  g : Nat -> Nat
  g x =  f $ suc x  where
                    f : Nat -> Nat
                    f y = y

Agda-2.3.0.1 MAlonzo  reports a  multiple definition of  f.
It is natural to put that a value defined under `where' is local and
overrides the outer value of the synonym (like in Haskell).

What is a profound reason to change this nice rule?

May be `private' will help, but why does one need to put an extra 
`private' ?

Thanks,

------
Sergei