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

user_4779636 0
Viewed 96

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])'
haskell
1 Answers

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.

user_32349590
Related