pattern-matching - `case` 细化参数

Question

在this answer on a question about the totality checker ，建议使用 case 而不是 with 的解决方法。

但是，在匹配结果细化其他参数类型的情况下，这种转换并不容易进行。

例如，给定以下定义:

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

以下定义进行了类型检查，但不被接受为全部:

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

而下面的代码不进行类型检查:

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

由于

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

我也试过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)

但在这里，foo1' 也不被接受为总数:

 foo1' is not total as there are missing cases

Answer 1

我发现的一个有效的解决方法是在每个分支中重新绑定(bind) n，即将 foo2 写为

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

不幸的是，虽然这适用于我最初问题中的这个简化问题，但当各个分支的类型不同时它不起作用；例如在

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

失败了

 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)