Why can an existential type be poly-kinded?

Question

When I wrote

data Y1 f a where
  Y1 :: (b -> a) -> f b -> Y1 f a

GHC 9.12.1 infered its kind as Y1 :: (Type -> Type) -> Type -> Type. But when I gave a kind signature to make f poly-kinded, GHC accepted it.

type Y1 :: (k -> Type) -> Type -> Type
data Y1 f a where
  Y1 :: (b -> a) -> f b -> Y1 f a

But I'm not sure how I can use a kind other than Type as k. I need to make either a or b not Type, but a kind of (->) is Type -> Type -> Type, and a and b have to be Type.

Can I ask why it can be poly-kinded, and how I can use it?

Also, I found that GHC didn't allow me to make it poly-kinded with ExistentialQuantification.

data Y2 f a = forall k (b :: k). Y2 (b -> a) (f b)

GHC made this an error.

<interactive>:50:38: error: [GHC-25897]
    • Expected a type, but ‘b’ has kind ‘k’
    • In the type ‘(b -> a)’
      In the definition of data constructor ‘Y2’
      In the data declaration for ‘Y2’

This kind of makes sense, but I'm not sure why GHC allowed it with GADT-syntax, but didn't allow it with ExistentialQuantification.

Answer 1

If you enable -fprint-explicit-foralls and -fprint-explicit-kinds, you see that the Y1 type constructor has the following kind:

> :k Y1
Y1 :: forall k. (k -> Type) -> Type -> Type

While the Y1 data constructor has the following type:

> :t Y1
Y1 :: forall b a (f :: Type -> Type). (b -> a) -> f b -> Y1 @Type f a

In other words, while the type of the Y1 data constructor forces b to have kind Type, nothing prevents you from adding another constructor that returns a Y1 @k f a for some other kind k.

Answer 2

One of the things you can do with GADT syntax is to implicitly specialize type variables. For example, you can write

data T a where T :: T Bool

and although the kind of T makes it look like it can accept any type, in reality you can only ever build T Bools. Alternately, you could think of this as having a constraint on the type argument:

data T a where T :: a ~ Bool => T a

This is what's happening to you: the k from your kind declaration is getting implicitly constrained:

type Y1 :: (k -> Type) -> Type -> Type
data Y1 f a where
  Y1 :: {k ~ Type =>} (b -> a) -> f b -> Y1 f a

So you can have any kind k you want, as long as you want Type.