`case` qui affine les arguments

Question

Dans this answer on a question about the totality checker, une solution de contournement impliquant l'utilisation de case au lieu de with a été recommandée. Cependant, dans les situations où le résultat de la correspondance affine le type d'autres arguments, cette transformation n'est pas simple à faire.

Par exemple, étant donné les définitions suivantes:

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 

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

les typable définition suivants, mais ne sont pas acceptés comme total:

foo1 : Nat -> Nat 
foo1 n with (parity n) 
    foo1 n@(k + k) | Left (Evidence _ (Times2 k)) = (n * n) 
    foo1 n@(S (k + k)) | Right (Evidence _ (Times2Plus1 k)) = (2 * (k * n + k)) 

alors que le suivant ne Typecheck pas:

foo2 : Nat -> Nat 
foo2 n = case parity n of 
    Left (Evidence k (Times2 k)) => n * n 
    Right (Evidence k (Times2Plus1 k)) => (2 * (k * n + k)) 

en raison de

Type mismatch between 
     IsEven (k + k) k (Type of Times2 k) 
and 
     IsEven n k (Expected type) 

J'ai aussi essayé expanding the with in foo1:

foo1' : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n)) -> Nat 
foo1' n@(k + k) (Left (Evidence k (Times2 k))) = (n * n) 
foo1' n@(S (k + k)) (Right (Evidence k (Times2Plus1 k))) = 2 * (k * n + k) 

foo1 : Nat -> Nat 
foo1 n = foo1' n (parity n) 

mais ici, foo1' est pas non plus accepté comme total:

foo1' is not total as there are missing cases 

Answer 1

Une solution efficace que je l'ai trouvé pour cela est de re-lier n dans chaque branche, c.-à-d. écrire foo2 comme

foo2 : Nat -> Nat 
foo2 n = case parity n of 
    Left (Evidence k (Times2 k)) => let n = k + k in n * n 
    Right (Evidence k (Times2Plus1 k)) => let n = S (k + k) in (2 * (k * n + k)) 

Malheureusement, bien que cela fonctionne pour ce problème simplifié à partir de ma question initiale, cela ne fonctionne pas lorsque les types des différentes branches diffèrent; par exemple dans

total Foo : Nat -> Type 
Foo n = case parity n of 
    Left (Evidence k (Times2 k)) =>() 
    Right (Evidence k (Times2Plus1 k)) => Bool 

foo : (n : Nat) -> Foo n 
foo n = case parity n of 
    Left (Evidence k (Times2 k)) =>() 
    Right (Evidence k (Times2Plus1 k)) => True 

qui échoue avec

Type mismatch between 
     () (Type of()) 
and 
     case parity (plus k k) of 
      Left (Evidence k (Times2 k)) =>() 
      Right (Evidence k (Times2Plus1 k)) => Bool (Expected type)