[Haskell-cafe] Promoted data types

[coot at coot.me]

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 509 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/df9b1c8f/attachment.sig>