[SOLVED] How to define a data type with an explicit kind quantification?

How to define a data type with an explicit kind quantification?

When I define

data Foo a = Foo [a]

then the type is of kind Foo :: * -> *.

Having enabled PolyKinds and RankNTypes I'd like to explicitly quantify it with a more general kind signature Foo :: forall k . k -> k.

However none of my attempts worked:

--    Malformed head of type or class declaration: (Foo :: forall k.
--                                                         k -> k) a
32 | data (Foo :: forall k . k -> k) a = Foo [a]

-- error: parse error on input ‘::’
32 | data Foo a = Foo [a] :: forall k . k -> k

-- error:
--     Multiple declarations of ‘Foo’

data Foo :: forall k . k -> k
data Foo a = Foo [a]

Solution

You can use a standalone kind signature:

type Foo :: forall k. k -> k
data Foo a = Foo [a]

But do note that the kind forall k. k -> k is not valid for Foo, because Foo a, being a data type, must have kind Type, furthermore the kind of [] is Type -> Type. So the kind signature Foo :: Type -> Type is forced.

An example that does compile without errors is:

type Foo :: forall k. k -> Type
data Foo a = Foo