Constructor that lifts (via DataKinds) to * -> A

Question

Given an ADT like

data K = A | B Bool

the DataKinds extension allows us to lift it into kinds and types/type constructors

K :: BOX
'A :: K
'B :: 'Bool -> K

Is there a way to add a constructor to K that lifts to the type constructor

'C :: * -> K

?

Mood

Answer 1

As Conor states, this is not directly possible. You can, however, define

data K a = ... | C a

Then this promotes to

C :: a -> K a

If you then use K *, you can achieve what you want.

Aroma

Answer 2

At the moment, I'm afraid not. I haven't spotted an obvious workaround, either.

This ticket documents the prospects for the declaration of data kinds, born kind, rather than being data types with kindness thrust upon them. It would be entirely reasonable for the constructors of such things to pack up types as you propose. We're not there yet, but it doesn't look all that problematic.

My eyes are on a greater prize. I would like * to be perfectly sensible type of runtime values, so that the kind you want could exist by promotion as we have it today. Combine that with the mooted notion of pi-type (non-parametric abstraction over the portion of the language that's effectively shared by types and values) and we might get a more direct way to make ad hoc type abstractions than we have with Data.Typeable. The usual forall would remain parametric.

Horseweed

Would Rich Eisen's stated goals with his dependent GHC project also meet your goals? – Hassi