Pourquoi ce bloc 'with' gâche-t-il la totalité de cette fonction?

Question

Je suis en train de calculer la parité avec le plancher de la moitié, sur des nombres naturels:

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

J'ai essayé d'aller avec la mise en œuvre évidente de 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) 

Ce typable et fonctionne comme attendu. Cependant, si je tente de marquer parity comme total, Idris commence à se plaindre:

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

Le seul with bloc que je vois dans parity est celui avec l'appel récursif de parity (S (S n)) à parity n, mais il est clair que bien-fondé, puisque n est structurellement plus petit que S (S n).

Comment puis-je convaincre Idris que parity est total?

Answer 1

Il ressemble à un bug pour moi, parce que la solution suivante basée sur case passe le vérificateur de la totalité:

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)