使用数据索引-类型不匹配错误

Question

data Z
data S n

type One = S Z
type Two = S (S Z)

type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

ghci> :t undefined :: Plus One Two
undefined :: Plus One Two :: S * (S * (S * Z))

data Nat = Z | S Nat

type family Plus m n :: Nat

Kind mis-match
Expected kind `OpenKind', but `Plus One Two' has kind `Nat'
In an expression type signature: Plus One Two
In the expression: undefined :: Plus One Two

Answer 1

我认为你测试的方法是不正确的。undefined可以是任何类型的*（我可能错了）。

在ghci中尝试此操作

ghci>:t (undefined :: 'Z)

<interactive>:1:15:
    Kind mis-match
    Expected kind `OpenKind', but `Z' has kind `Nat'
    In an expression type signature: Z
    In the expression: (undefined :: Z)

在ghci中使用:kind！仍然可以获得加1 2的类型

ghci>:kind! Plus One Two
Plus One Two :: Nat
= S (S (S 'Z))