[Haskell-cafe] Promoted data types

Hello, Currently with `DataKind` extension, Haskell allows to promote terms / types to types / kinds. Currently, one cannot write: ``` data K a where K0 :: forall (x :: a). x -> K a ``` Because `K0` is both a term and a type constructor, and as a term and one cannot represent `x` of kind `a`. Is there a proposal or an issue to allow such declaration and error at use sites of `K0` as a term, rather than at declaration site? Best regards, Marcin Szamotulski