涉及必须相同的三种类型的类型不匹配

Question

这样编译：

data ThreeEq : a -> b -> c -> Type where
    Same3 : (x : a)  -> ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS k k k (Same3 k) = Same3 (S k)

但是 Same3 的一个小改动，它不再编译。谁能解释一下为什么？

data ThreeEq : a -> b -> c -> Type where
    Same3 : x -> ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS k k k (Same3 k) = Same3 (S k)

错误信息如下：

- + Errors (1)
 `-- Amy2.idr line 5 col 0:
     When checking left hand side of allSameS:
     When checking an application of Main.allSameS:
             Type mismatch between
                     ThreeEq x x x (Type of Same3 _)
             and
                     ThreeEq k y z (Expected type)

             Specifically:
                     Type mismatch between
                             Type
                     and
                             Nat

Answer 1

这是不同之处

data ThreeEq : a -> b -> c -> Type where
    Same3 : (x : a)  -> ThreeEq x x x
             ^   ^
             |   |
             |    Type
             Value

此处，Same3 Z 构建了一个 Three Z Z Z 类型的值。

data ThreeEq : a -> b -> c -> Type where
    Same3 : x -> ThreeEq x x x
            ^
            |
            Type

现在，Same3 Z 构建了一个类型为 Three Nat Nat Nat 的值。

涉及必须相同的三种类型的类型不匹配

Type mismatch involving three types that must be identical

idris