[Agda] strange mismatch

[Sergei Meshveliani]

On Wed, 2017-05-24 at 22:13 +0300, Sergei Meshveliani wrote:
> 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?


May be, listing  "zr a"  in parameters does not imply that  a  does not
match against zr.  
I am not sure.

May be, I have instead to add to  Expression  the constructors  
    zr : Expression
    a  : Expression,

and this will imply that  a  does not match against zr.

Can anybody comment, please?

Thanks,

------
Sergei