Thanks for the explanation. I realized I had a few gaps in understanding. Here are some additional notes I made while reasoning through whatâ€™s going on in case anyone else is similarly confused.

An arrow `->`

in a type signature is the `Function`

data constructor, which has a â€śkindâ€ť signature of `Type -> Type -> Type`

. Note that these *kind signature arrows* are different than *type signature arrows*. Only the former means `Function`

.

So then if we look at `V2`

's `bar :: forall a. c a -> a`

, we can fill-in the following:

```
Type -> Type -> Type
(c a) a Function (c a) a
```

Looking at the second `Type`

, we see that `a`

has kind `Type`

.

Looking at the first `Type`

, we see that `c a`

has kind `Type`

, and since `a`

was earlier determined to have kind `Type`

, then `c`

must have kind `Type -> Type`

. This kind signature is straightforward (no *kind polymorphism*), and so the compiler doesnâ€™t nag us for annotation. But we could still include the kind annotation if we wanted to: `type V2 :: (Type -> Type) -> Type`

.

In `V1`

or `V3`

, we canâ€™t nail down the kinds of any `a`

to simply `Type`

. These `a`

s could be a variety of things, such as `Type -> Type`

, `Type -> Type -> ... -> Type`

, `Row Type`

, etc.

Since `c`

must accept any of these kinds of `a`

, we use a kind variable `k`

to indicate this â€śkind polymorphismâ€ť and describe the kind of `c`

as `forall k. (k -> Type)`

. The compiler wants us to annotate declarations involving polymorphic kinds.