[Haskell-cafe] Promoted data types

[Kai-Oliver Prott]

Hi,

I think I don't quite understand the question.

The code you propose seems wrong to me for a different reason:
The type constructor (->) for function values has Kind: * -> * -> *

In fact, GHC will print this error when compiling the snippet with the 
corresponding extensions.

Promoting a data type is done differently.

Can you elaborate on what exactly it is you are proposing?

Sincerely
Kai Prott

On 03.05.21 14:04, coot at coot.me wrote:
> 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
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/af4c2a3f/attachment.html>