[SOLVED] Why does this 'with' block spoil the totality of this function?

Why does this 'with' block spoil the totality of this function?

I'm trying to compute parity together with the floor of the half, over natural numbers:

data IsEven : Nat -> Nat -> Type where
    Times2 : (n : Nat) -> IsEven (n + n) n

data IsOdd : Nat -> Nat -> Type where
    Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n

parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))

I tried going with the obvious implementation of parity:

parity Z = Left $ Evidence _ $ Times2 0
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0
parity (S (S n)) with (parity n)
  parity (S (S (k + k))) | Left (Evidence _ (Times2 k)) =
      Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k)
  parity (S (S (S ((k + k))))) | Right (Evidence _ (Times2Plus1 k)) =
      Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k)

This typechecks and works as expected. However, if I try to mark parity as total, Idris starts complaining:

 parity is possibly not total due to: with block in parity

The only with block I see in parity is the one with the recursive call from parity (S (S n)) to parity n, but clearly that is well-founded, since n is structurally smaller than S (S n).

How do I convince Idris that parity is total?

Solution

It looks like a bug to me, because the following solution based on case passes the totality checker:

total
parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))
parity Z = Left $ Evidence _ $ Times2 0
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0
parity (S (S k)) =
  case (parity k) of
    Left (Evidence k (Times2 k)) =>
      Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k)
    Right (Evidence k (Times2Plus1 k)) =>
      Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k)