Несоответствие типов с участием трех типов, которые должны быть идентичными

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.