Warum zerstört dieser "mit" -Block die Gesamtheit dieser Funktion?

Question

Ich versuche Parität zusammen mit dem Boden der Hälfte zu berechnen, über die natürlichen Zahlen:

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)) 

ich mit der offensichtlichen Umsetzung parity gehen versucht:

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) 

Diese typechecks und arbeitet als erwartet. Allerdings, wenn ich versuchen parity als total zu markieren, beginnt Idris klagen:

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

Der einzige with Block I in parity sehen, ist das mit dem rekursiven Aufruf von parity (S (S n)) zu parity n, aber klar ist, dass eine fundierte, seit n ist strukturell kleiner als S (S n).

Wie überzeuge ich Idris, dass parity insgesamt ist?

Answer 1

Es sieht aus wie ein Bug zu mir, weil die folgenden Lösung basierend auf case die Gesamtheit checker passiert:

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)