# DataKinds Are Not What You Think

The `DataKinds`

language extension doesn’t work the way you think it does… probably. Of course I can’t possibly know what mental model you have for `DataKinds`

. Perhaps you are one of the few who understand its true nature. But I’ve seen experts – yes, type-level Haskell wizards – fall into the trap that I’m about to expose.

## How DataKinds are commonly explained

To set the stage, let’s take a look at how `DataKinds`

are commonly explained.

Matt Parsons in his article “Basic Type Level Programming in Haskell” (2017) writes:

`data Nat = Zero | Succ Nat`

In plain Haskell, this definition introduces a new type

`Nat`

with two value constructors,`Zero`

and`Succ`

(which takes a value of type`Nat`

). With the`DataKinds`

extension, this also defines some extra new tidbits. We get a new kind`Nat`

, which exists in a separate namespace. And we get two new types: a type constant`'Zero`

, which has the kind`Nat`

, and a type constructor`'Succ`

, which accepts a type of kind`Nat`

.

Sandy Maguire in his book “Thinking with Types” (2018) writes:

`data Bool = False | True`

… the

`data Bool`

definition above introduces the following things into scope (as usual):

- A type constructor
`Bool`

of kindType- A data constructor
`True`

of type`Bool`

- A data constructor
`False`

of type`Bool`

However, when

`-XDataKinds`

is enabled, our definition of`Bool`

also introduces the following into scope:

- A new kind:
Bool- A promoted data constructor
`'True`

of kindBool- A promoted data constructor
`'False`

of kindBool

Rebecca Skinner in her article “An Introduction to Type Level Programming” (2021) writes:

`data ExampleColor = Red | Green | Blue`

Here we’re creating a sum type with constructors

`Red`

,`Green`

and`Blue`

, but thanks to`DataKinds`

we’re also creating a new Kind with types`Red`

,`Green`

and`Blue`

.

The common theme in those explanations is that kinds are *created* from types, as if there was some duplication happening behind the scenes:

## What’s wrong with this explanation?

Prior to GHC 8.0 (2016), this model used to work just fine because types and kinds were indeed entirely separate. But with the introduction of the type-in-type axiom, this picture became outdated and misleading. Here are a few lines of code that do not quite fit within this framework:

```
type family Sing :: k -> Type
class FromSing k where
fromSing :: Sing (a :: k) -> k
```

At first glance, this does not even seem related to the picture above. And yet it reveals a fatal flaw in it. In the type signature for `fromSing`

, is `k`

a type or a kind?

```
fromSing :: Sing (a :: k) -> k
-- ↑ ↑
-- kind type
```

Well, the first occurrence is a kind, and the second occurrence is a type! How can one variable be a type and a kind simultaneously? This paradox is resolved by the following mental shift: there are no kinds. You heard that right.

**Pre-8.0:**terms have types, types have kinds.**Post-8.0:**terms have types, types have types.

We used to have terms, types, and kinds. Now we’re down to terms and types. Occasionally, however, the old terminology is still convenient. Saying “type of a type” every time is a bit awkward, so we may say “kind” instead. The important thing to keep in mind is that a kind isn’t a thing in itself; a type can be used as a kind.

So in the example above, `k`

is a *type* variable. It’s used as a kind in `Sing (a :: k)`

, so we might also call it a *kind* variable. However, this is a statement about how it’s used, not about what it is.

This suggests the following modification to our understanding of `DataKinds`

:

Compared to the previous model, we now have the type level and the term level, whereas kinds don’t get their own level and are merged into types. This is definitely an improvement, but it’s still incorrect in a subtle way. Since this interpretation of `DataKinds`

is based on duplication, we end up with two separate `Bool`

s. But are they really distinct?

Building upon our definitions of `Sing`

and `FromSing`

, here are some instances for them:

```
data SBool (a :: Bool) where
STrue :: SBool True
SFalse :: SBool False
type instance Sing @Bool = SBool
instance FromSing Bool where
fromSing :: Sing (a :: Bool) -> Bool
fromSing STrue = True
fromSing SFalse = False
```

Haskell is no stranger to puns. I could declare `data Proxy a = Proxy`

and have two proxies in scope: one is a data constructor and the other is a type constructor. So it wouldn’t be unreasonable to assume that the same thing is happening with `Bool`

: perhaps one is a type and the other one is a kind, yet they are internally distinct. Let me mark type and kind occurrences with different numbers:

```
data SBool (a :: Bool1) where
STrue :: SBool True
SFalse :: SBool False
type instance Sing @Bool1 = SBool
instance FromSing Bool2 where
fromSing :: Sing (a :: Bool1) -> Bool2
fromSing STrue = True
fromSing SFalse = False
```

The hypothesis we need to test now is whether GHC thinks that `Bool1`

and `Bool2`

are actually distinct entities. The answer shall reveal itself if we compare the type signature of `fromSing`

in the class declaration and in the instance:

```
fromSing :: Sing (a :: k) -> k
fromSing :: Sing (a :: Bool1) -> Bool2
```

We seem to instantiate `k`

to `Bool1`

in one position and to `Bool2`

in another. So if we had `Bool`

the type and `Bool`

the kind, we would expect a type error of the following form:

```
• Couldn't match type 'Bool' with kind 'Bool'
```

… because GHC couldn’t decide what `k`

stands for. And yet the code above compiles just fine, which leads us to the only possible conclusion: there’s just one `Bool`

.

One might wonder: are `True`

and `False`

actually duplicated if `Bool`

isn’t? As long as terms and types are separated, we can’t really tell. A term-level variable can’t occur in a type-level context or vice versa, so we can’t ask the compiler if the term-level `True`

and the type-level `True`

are equal. There is currently no way to test this hypothesis. One could indeed argue that promoted data constructors are a mirror image of their term-level counterparts.

Dependent types, however, lead us to a more elegant model:

For now this simplification is out of reach, but, personally, I find it to be a very attractive direction.

## Conclusion

Enabling the `DataKinds`

extension does not create new kinds. Instead, it allows existing types to be used as kinds. This objection isn’t based on vague philosophical grounds but has practical implications, as illustrated by a fairly basic use of singleton types that we covered.