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.
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.