[Agda] missing double definition

[Sergei Meshveliani]

People,
in the program of  

------------------
f : ℕ
f = let m : ℕ
        m = 0

        m : ℕ
        m = 1
    in
    m
------------------

the value  m  is doubly defined.
Need the type checker report an error?

(Development Agda of January 9, 2016, ghc-7.10.2  
type-checks this).

Thanks,

------
Sergei