# GHC/Type system/PolyKinds

# Kind polymorphism

GHC 7.6 introduced kind polymorphism and data kinds for the first time. This page contains notes (currently rather random) about how to use these features.

- User manual sections about kind polymorphism and data type promotion
- Giving Haskell a promotion, the paper about it.

## Syntactic ambiguity for lists

Suppose `Proxy :: forall k. k -> *`

, and consider

```
Proxy [Int]
Proxy [Int,Bool]
```

The former must mean what it always means in Haskell, namely

```
Proxy * (List Int)
```

where I'm writing the kind argument explicitly. To be fully clear, I'm writing `List`

for the type constructor for lists (written `[]`

in Haskell), so `(List Int)`

is a type of kind *.

But `Proxy [Int,Bool]`

can only mean `Proxy`

applied to a list of types, thus:

```
Proxy [*] (Cons * Int (Cont * Bool (Nil *)))
```

Now we can see that `Proxy [Int]`

is ambiguous. It could also mean

```
Proxy [*] (Cons * Int (Nil *))
```

but we choose the normal meaning to avoid screwing up Haskell programs. To get the above form we have to quote the "[", thus

```
Proxy '[ Int ]
```

In short, singleton lists (and indeed the empty list) must be explicitly promoted with a quote, whereas for type-level lists of two or more elements you don't need an explicit promotion quote.