I was playing around in the REPL trying to understand `Data.NonEmpty`

’s definition, so I came up with the following types and wanted to check their kind(?) when this error popped up:

```
> import Data.List (List(..), (:))
>
> data T f a = T f a -- ≈ Data.Tuple
> data T' f a = T' (f a)
> data T'' f a = T'' a (f a)
>
> x = T 1 "a" :: T Int String
> y = T' (1 : Nil) :: T' List Int
> z = T'' 27 (1 : Nil) :: T'' List Int
>
> :kind T
Type -> Type -> Type
> :kind T''
(Type -> Type) -> Type -> Type
> :kind T'
Error found:
at <internal>:0:0 - 0:0 (line 0, column 0 - line 0, column 0)
Type variable k is undefined.
while inferring the kind of k
while checking that type k
has kind Type
while inferring the kind of T' @k
See https://github.com/purescript/documentation/blob/master/errors/UndefinedTypeVariable.md
for more information, or to contribute content related to this error.
```

Went to link in the error description, but it does not seem to be related to this one (or I failed to make the connection). As far as I understand, `f`

in `data T' f a`

has to be a functor, so why is `:kind`

unable to infer this, yet it has no problem with `T''`

(or `NonEmpty`

)?

I can kinda help with this. The issue being bumped into here is called “polymorphic kinds” or “polykinds.” Here’s some references on the matter:

If you add a kind annotation to `T'`

:

```
data T' :: (Type -> Type) -> Type -> Type
data T' f a = T' (f a)
```

then it’ll work (of course that kinda defeats the purpose of asking the REPL to print the kind information).

I think it otherwise could have kind

```
data T' :: forall k. (k -> Type) -> k -> Type
```

I can’t do a good job of explaining why `T'`

needs the annotation and others don’t, and I can’t do a good job of explaining what other `k`

’s you could use to do something useful besides `Type`

.

1 Like

No worries and thank you! You already did plenty as it would have taken me quite a while to stumble upon “polymorphic kinds”… and I didn’t even know about kind signatures…

`T'`

needs an annotation because the kind of `a`

cannot be unambiguously inferred. It depends on what `f`

is. Which itself depends on what `a`

is.

For example:

```
> data F a = F a
> :kind T' F
Type -> Type
> data G a = G (a Int)
> :kind T' G
(Type -> Type) -> Type
```

In these two examples the kinds of `a`

are different. In the first example `a :: Type`

and in the second - `a :: Type -> Type`

. This means that the kind of `a`

has to be polymorphic.

In `T`

this doesn’t happen, because both `f`

and `a`

are used in a position where there would be a datum (e.g. `T "foo" 42`

), and therefore both `f`

and `a`

must be `Type`

. No polymorphism.

In `T''`

this doesn’t happen, because `a`

is used in a data position, and therefore `a :: Type`

, and then `f a`

is used in a data position, and therefore `f a :: Type`

, and therefore `f :: Type -> Type`

. No polymorphism here either.

What fascinates me is why REPL can’t show the polymorphic kind. This works fine at the type level:

```
> f x = x + zero
> :t f
forall (a25 :: Type). Semiring a25 => a25 -> a25
```

And the compiler itself is even able to figure this out when in IDE support mode:

(and, of course, when compiling)

So why not in REPL?

3 Likes