Agda: Case splitting generates invalid syntax when there's a `rewrite`

[ice1000]

Like, if I have:

  a-b=a+-b : ∀ a b → a ⊖ b ≡ + a - + b
  a-b=a+-b zero  zero    = refl
  a-b=a+-b zero (nsuc _) = refl
  a-b=a+-b (nsuc a) b
    rewrite nat-add-comm a 0 = {!!}

And I type C-c C-c b RET in the hole, then I get:

  a-b=a+-b : ∀ a b → a ⊖ b ≡ + a - + b
  a-b=a+-b zero  zero    = refl
  a-b=a+-b zero (nsuc _) = refl
  a-b=a+-b (nsuc a) b
    a-b=a+-b (nsuc a) zero | .a | refl = ?
    a-b=a+-b (nsuc a) (nsuc b) | .a | refl = ?

Which is invalid.

is this a bug?

[andreasabel]

This is a combination of bugs #2340 and and #2087.

Thanks for reporting, I close this as duplicate.

[ice1000]

Glad to hear that!

I really appreciate your quick reply! :+1: :smiley:

[andreasabel]

Unfortunately, the bugs require some extra work to fix, thus, I am a bit pessimistic that they will be attacked soon.

I hope you can work around them!