Why Can't I Construct a Singleton List of Symbol?

Question

I'm getting a puzzling error from GHCI, any idea what it means? A pair of symbols works just fine, but a singleton list fails.

$ 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

In general, when using "term syntax at the type level" we can find the term notation to be ambiguous in some cases. Hence, when using DataKinds GHC requires us to use quotes ' to disambiguate.

For instance, (x, y) is term syntax for a pair. But, alas, (Bool, Int) is a type even if it has the same syntax. Indeed, we might well have:

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

Now... what if we want to write a pair of types as a "term at the type level"? We want

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

but that clashes with the second case above.

To disambiguate, we need a quote.

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

The syntax for lists has similar issues:

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

But what if we want a singleton list of types? The syntax would be:

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

but that clashes again. We need a quote, again:

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

We do get other ambiguities in a few other cases:

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

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

It is best if we always add quotes.