`case`, das Argumente verfeinert

Question

In this answer on a question about the totality checker wurde eine Problemumgehung mit case anstelle von with empfohlen.

In Situationen jedoch, in denen das Ergebnis der Übereinstimmung den Typ der anderen Argumente verfeinert, ist diese Umwandlung nicht einfach zu machen.

beispielsweise angesichts der folgenden Definitionen:

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

folgende Definition typechecks, ist aber nicht als insgesamt akzeptiert:

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

während die folgenden man nicht typecheck:

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

aufgrund

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

Ich habe auch versucht 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) 

aber hier wird foo1' auch nicht als insgesamt akzeptiert:

foo1' is not total as there are missing cases 

Answer 1

Eine wirksame Abhilfe, die ich für diese gefunden haben, ist neu binden n in jedem Zweig, dh zum Schreiben foo2 als

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

Leider, während dies für dieses vereinfachte Problem von meiner ursprünglichen Frage funktioniert, funktioniert es nicht, wenn sich die Typen der verschiedenen Zweige unterscheiden; zum Beispiel in

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 

, die nicht mit

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)