This is a known problem. Originally, one could not even split if the rhs was more than a single hole. Now, you can split, but in some cases you get garbage. I still consider this an improvement.

The problem is mostly on the side of the emacs mode (see #2340), but in your case, there is also the substitution into the rhs missing. However, at this point we cannot reify internal syntax to concrete syntax in a way that fulfills the roundtrip-property, thus, a perfect implementation of case splitting is impossible.

@UlfNorell : refering to our discussion yesterday, here is a situation where you want the round-trip property, which is currently impossible (e.g. because of the desugaring of lets), and it will not get better with more things that are desugared early.

Maybe a possible solution here would be to put the content of rhss into holes. However, emacs does not know where the rhs of a clause ends.

What about using an @ alias to keep the name we are case-splitting on if it shows up on the right hand side?

bar : Nat → Nat
bar x = foo x {!x!}

would lead to:

bar : Nat → Nat
bar x@zero = foo x ?
bar x@(suc x') = foo x ?

Ah, yes, this would fix the present issue!

The other issues in the family: #1146 and #2628.