AgdaQuestion

As a learning experience, I'm trying to implement a verified regular-expression matcher using continuation-passing style in Agda, based on the one proposed in [this paper](http://www.cs.cmu.edu/~rwh/papers/regexp/jfp.pdf).

I've got a type for regular expressions defined like this:

<!-- language: lang-agda -->

    data RE :  Set where
      ε : RE 
      ∅ : RE 
      Lit : Char -> RE 
      _+_ : RE -> RE -> RE
      _·_ :  RE -> RE -> RE
      _* : RE -> RE

And a type for a proof that a string matches an RE like this:

<!-- language: lang-agda -->

    data REMatch : List Char -> RE -> Set where
      EmptyMatch : REMatch [] ε
      LitMatch : (c : Char) -> REMatch (c ∷ []) (Lit c)
      ...
      ConcatMatch : 
	    (s1 : List Char) (s2 : List Char ) (r1 : RE) (r2 : RE)
	    -> REMatch s1 r1
	    -> REMatch s2 r2
	    -> REMatch (s1 ++ s2) (r1 · r2)


I'm trying to write a correctness proof for my matcher, but I'm getting type errors on my pattern matches, before I even try to have a proof:     

<!-- language: lang-agda -->

    accCorrect : 
      (r : RE) (s : List Char) (s1 : List Char) (s2 : List Char) (k : (List Char -> Bool)) 
      -> ( (s1 ++ s2) ≡ s)
      -> (REMatch s1 r)
      -> (k s2 ≡ true)
      -> (acc r s k ≡ true )
    accCorrect ε [] [] [] k _ EmptyMatch kproof = kproof
    accCorrect (r1 · r2) s s1 s2 k splitProof (ConcatMatch _ _ _ _ subMatch1 subMatch2 ) kproof = ?

However, this gives the following error:

    r4 != r2 of type RE
    when checking that the pattern
    ConcatMatch _ _ _ _ subMatch1 subMatch2 has type
    REMatch s1 (r1 · r2)

However, if I replace the underscores by `s1`,