[Agda] case ((a , b) , (c , d))

[Sergei Meshveliani]

Please, what is wrong here?

open import Function using (case_of_)                           
open import Data.Nat  using (ℕ; suc; zero)
open import Data.Product using (_×_; _,_)

f : ℕ → ℕ
f n = case (  (n , suc n)  ,  (suc n , suc (suc n))  )
      of \
      { ( (zero , zero) , _             ) →  zero
      ; ( _             , (zero , zero) ) →  zero
      }


The first `case' pattern is type checked, and the second is not:
"
Type mismatch
when checking that the pattern zero has type _25 n proj₁ 0
"

This is  Agda 2.3.2.2 MAlonzo.

Thanks,

------
Sergei