[Agda] strange "Unreachable clause"

[Sergei Meshveliani]

Please, what is wrong in f' below? 
Why Agda-2.5.3 type-checks f and does not type-check f' ? 

---------------------------------------------------------
open import Level    using () renaming (zero to 0ℓ)
open import Algebra  using (Semiring)
open import Data.Nat using (ℕ)

data Expr : Set  where c1 : ℕ → Expr
                       c2 : Expr → Expr → Expr
f : Expr → ℕ
f (c1 _)        =  0
f (c2 (c1 0) _) =  0
f (c2 (c1 1) _) =  0
f (c2 _      _) =  0

postulate R : Semiring 0ℓ 0ℓ
open Semiring R using (Carrier; 0#; 1#)

data Expr' : Set  where d1 : Carrier → Expr'
                        d2 : Expr' → Expr' → Expr'
f' : Expr' → ℕ
f' (d1 _)         =  0
f' (d2 (d1 0#) _) =  0
f' (d2 (d1 1#) _) =  0
f' (d2 _       _) =  0
----------------------------------------------------------

Agda reports  Unreachable clause  for the third pattern in  f',  as if
it was shadowed by previous pattern. But it is not shadowed.

Is this a bug in Agda-2.5.3 ?

------
Sergei