Okay, I mistakenly copied idris1's example code. Parity's definition should be:
data Parity : Nat -> Type where
Even : {n : _} -> Parity (n + n)
Odd : {n : _} -> Parity (S (n + n))
In Idris 2, we need to state explicitly that n is needed at run time
When I leave that parameter out, Idris inserts {0 n : _} for me, which is has quantity 0.
In this case, the erased value j is being passed as the first argument to helpEven, which is not quantity 0.
However,
So helpEven doesn't need (j : Nat) at all. This could work too.
helpEven : Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven p = rewrite plusSuccRightSucc j j in p
...
parity (S (S (j + j))) | Even = helpEven (Even {n = S j})
...