[Agda] matching against _::_ ?

[Sergei Meshveliani]

On Wed, 2017-06-07 at 23:01 +0200, Andreas Abel wrote:
> You can use vectors:
> 
> open import Data.Nat.Base
> open import Data.Vec
> open import Function
> 
> test : ℕ
> test = case 1 ∷ 2 ∷ 3 ∷ [] of λ where
>    (a ∷ b ∷ c ∷ _) → a + b + c


Thank you. This example works with it.

But my real example does not.
The two lemmas below differ only in the way in which  a' and b'  are
bound to their values. The former uses the assignment `=', the latter
uses matching against a vector. 
Below  []' and _∷'_  are the Vec constructors.
lemma  is type-checked, and  lemma'  is not.

  open Ring R 
  ...
  lemma :  a + b ≈ b + a
  lemma =  let
             a' =  gen 0
             b' =  gen 1
             e  =  a' :+ b'
             e' =  b' :+ a'

             en≡e'n :  nf e ≡ nf e'
             en≡e'n =  PE.refl
           in
           value≈byNF gens e e' en≡e'n

  lemma' : a + b ≈ b + a
  lemma' =
         case  gen 0 ∷' gen 1 ∷' []'
         of \
         { (a' ∷' b' ∷' []') →
                         let e  =  a' :+ b'
                             e' =  b' :+ a'

                             en≡e'n :  nf e ≡ nf e'
                             en≡e'n =  PE.refl
                         in
                         value≈byNF gens e e' en≡e'n
         }

The report is 
" 
a' != b' of type Expression
when checking that the expression PE.refl has type
nf-comm (a' :+ b') ≡ nf-comm (b' :+ a')
"

In lemma', the values for a' and b' occur somehow confused. 

Can anyone tell, please, what is happening there?

Thanks,
 
------
Sergei