[Agda] strange mismatch

[Sergei Meshveliani]

On Wed, 2017-05-24 at 19:41 -0500, Andrés Sicard-Ramírez wrote:
> On 24 May 2017 at 14:35, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > 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.
> 
> Note that the `zr` in equations
> 
>   f (con zr) y        =  y
>   f x        (con zr) =  x
> 
> is *different* from the `zr` in the parameters.
> 


For example, for the equation 

    f (con zr) _ = con zr

in the above context we have that
zr  in the pattern is a variable to be matched, 
and  zr  on the right-hand side is the one in the parameters.
Right? 

Thanks to people for explanations,

------
Sergei