Why does :k [False] result in an error in GHCI?

Question

I'm confused about the error that I received at the end of the session below:

$ ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
Ok, modules loaded: Main.
*Main> :set -XDataKinds

*Main> :t [False, True]
[False, True] :: [Bool]

*Main> :t [False]
[False] :: [Bool]

*Main> :k [False, True]
[False, True] :: [Bool]

*Main> :k [False]

<interactive>:1:2:
    Expected kind ‘*’, but ‘False’ has kind ‘Bool’
    In a type in a GHCi command: [False]

Why the error?

---

Future experimenting reveals:

*Main> :k [Int]
[Int] :: *

*Main> :k [Int, Int]
[Int, Int] :: [*]

[Int] can have inhabited values so it is of kind *, but it also makes sense that it is of kind [*].

---

A bit more data points:

*Main> :k []
[] :: * -> *

*Main> :k [Bool]
[Bool] :: *

Dropsonde

I'm just learning about this so I don't have confidence in my answers yet but with -XDataKinds wouldn't the type [False, True] be of kind [Bool] ? – Dropsonde

Answer 1

If you have type level lists with only a single element, GHC thinks that it's not a lifted list but a regular list type constructor applied to some type of kind *.

You should prefix the list with an apostrophe to explicitly select for lifted lists:

> :k '[False]
'[False] :: [Bool]

Similarly with empty lists:

> :k '[]
'[] :: [k]

Williwaw

Specifically [False] is parsed as the type [] :: * -> * applied to the type False :: Bool, there is a kind mismatch - [] expects a * which gives the observed "kind error". – Decameter

Answer 2

As you note:

[Int] can have inhabited values so it is of kind *, but it also makes sense that it is of kind [*]

What you've spotted is that DataKinds there is ambiguity in some type expressions if you simply allow value expressions to be lifted to the type level. It very often comes up with lists this because of the use of square brackets for both list literals and list types, but it's not wholly specific to lists.

Basically, the source code text [False] could refer to three different things:

1. List literal syntax for a value level list, containing a single element which is the value False
2. The list type constructor applied to the type False
3. List literal syntax for a type level list, containing a single element which is the type False

Without DataKinds the third meaning doesn't exist, so the compiler could always use its contextual knowledge of whether the source code text [False] was occurring in a type expression or a value expression. But both case 2 and 3 occur in type expressions, so this doesn't help.

In this case we can see that [False] as the type "list of things of type False" doesn't make any sense, because the [] type constructor can only be applied to things of kind *. But the compiler has to know what you're trying to say before it can type/kind check things to see whether it's consistent; we don't really want it to try several possible interpretations and type/kind check them all, silently accepting if one of them works. And anyway with a little effort (along the lines of defining suitable type names and/or using PolyKinds to make type constructors that accept things of multiple kinds) you can come up with a situation where a piece of source text has all 3 of the sorts of meaning I outlined above, and all 3 could compile without error.

So, to resolve the ambiguity (without disrupting existing syntax like [Int] for "list of things of type Int") GHC adopts the rule that the ordinary non-lifted type constructors take precedence. So [False] actually does not mean a type level singleton list; it only means the (nonsense) "list of things of type False" type, which is results in the kind error you see.

But DataKinds also introduces syntax to explicitly request the other meaning; if you precede any type constructor with an apostrophe then GHC knows you're referring to the lifted version of the value constructor, not any non-lifted type constructor of the same name. For example:

Prelude> :k 'False
'False :: Bool

And similarly, tacking an apostrophe on the front of list literal syntax explicitly says you're writing a type-level list literal, not writing a list type even if the list only has one item. So:

Prelude> :k '[False]
'[False] :: [Bool]

Prelude> :k '[Int]
'[Int] :: [*]

You can similarly use it to distinguish between the list type constructor of kind * -> * and the empty type-level list:

Prelude> :k []
[] :: * -> *
Prelude> :k '[]
'[] :: [k]

Aguila