[Agda] strange mismatch

[Sergei Meshveliani]

Please, what is wrong here?

test1  is type-checked, and  test2  is not
(in Agda 2.6.0-207bde6) :


-----------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

module _ {α} (A : Set α) (zr a : A)
  where
  data Expression : Set α where
                          con  : A → Expression
                          _:+_ : Expression → Expression → Expression

  f : Expression → Expression → Expression
  f (con zr) y        =  y
  f x        (con zr) =  x
  f x        y        =  x :+ y

  test1 :  f (con zr) (con a) ≡ con a
  test1 =  PE.refl

  test2 :  f (con a) (con zr) ≡ con a
  test2 =  PE.refl
------------------------------------------------------------------------

How to fix?

Thanks,

------
Sergei