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
?
As Conor states, this is not directly possible. You can, however, define
Then this promotes to
If you then use
K *
, you can achieve what you want.