为什么我无法构造单例符号列表？

Question

我从 GHCI 收到一个令人费解的错误，知道这意味着什么吗？一对符号可以正常工作，但单例列表会失败。

$ ghci
> :m +GHC.Types
> :set -XDataKinds -XKindSignatures
GHC.Types> :kind! (["A", "B"] :: [Symbol])
(["A", "B"] :: [Symbol]) :: [Symbol]
= '["A", "B"]
GHC.Types> :kind! (["A"] :: [Symbol])
<interactive>:1:2: error:
    * Expected kind `[Symbol]', but `["A"]' has kind `*'
    * In the type `(["A"] :: [Symbol])'
<interactive>:1:3: error:
    * Expected a type, but `"A"' has kind `Symbol'
    * In the type `(["A"] :: [Symbol])'

Answer 1

一般来说，当使用“类型级别的术语语法”时，我们会发现术语符号在某些情况下是不明确的。因此，在使用DataKindsGHC时需要我们使用引号'来消除歧义。

例如，(x, y)是一对的术语语法。但是，唉，(Bool, Int)即使它具有相同的语法，它也是一种类型。事实上，我们很可能有：

(x,y) :: (Bool, Int)       -- term::type
(Bool, Int) :: Type        -- type::kind

现在...如果我们想将一对类型写为“类型级别的术语”怎么办？我们想要

(Bool, Int) :: (Type, Type)  -- term-at-type::kind
-- This is a kind error!

但这与上面的第二种情况冲突。

为了消除歧义，我们需要引用。

'(Bool, Int) :: (Type, Type)  -- term-at-type::kind
-- Now it kind-checks

列表的语法也有类似的问题：

[x] :: [Bool]      -- term::type
[Bool] :: Type     -- type::kind

但是如果我们想要一个单例类型列表怎么办？语法是：

[Bool] :: [Type]   -- term-at-type::kind
-- This is a kind error!

但这又发生冲突了。我们再次需要报价：

'[Bool] :: [Type]   -- term-at-type::kind
-- Now this kind-checks

在其他一些情况下，我们确实遇到了其他歧义：

[] :: Type -> Type
[] :: [Type]   -- wanted, but clashes
'[] :: [Type]  -- OK

data T :: T
T :: Type
T :: T     -- clashes
'T :: T    -- OK

最好总是添加引号。