[Haskell-cafe] Promoted data types

coot at coot.me coot at coot.me
Mon May 3 12:04:04 UTC 2021


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>

More information about the Haskell-Cafe mailing list