"Not a constructor application or primitive" when using `with`

I'm using views where I want to be able to match on the last n elements of a Vect.

data SplitLast : (n : Nat) -> (xs : Vect r a)
                 -> {auto prf : n `LTE` r} -> Type where
  Append : forall m, n . (init : Vect m a) -> (tail : Vect n a)
  -> SplitLast {prf=rewrite plusCommutative m n in lteAddRight n} n (init ++ tail)

splitLast : (n : Nat) -> (xs : Vect r a)
            -> {auto prf : n `LTE` r} -> SplitLast n xs

That compiles, but in the with part of a function which uses this,

flipLast : Vect (S (S r)) Nat -> Vect (S (S r)) Nat
flipLast xs with (splitLast 2 xs)
  flipLast (leading ++ [m, n]) | (Append leading [m, n]) = leading ++ [n, m]

I'm seeing

While processing left hand side of with block in flipLast. Can't match
on ?postpone [no locals in scope] (Not a constructor application or primitive).

...
 187 |   flipLast (leading ++ [m, n]) | (Append leading [m, n]) = leading ++ [n, m]
                           ^^

I don't get why - I thought this is exactly what the view + with would allow. Using Fin instead of the prf doesn't help.