[Haskell-cafe] Promoted data types

[Richard Eisenberg]

Perhaps Marcin is looking for https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst>, but that proposal would not accept the code in the original post, for the reasons Kai describes -- you just cannot have (x :: a) on one side of an arrow.

Richard

> On May 3, 2021, at 9:10 AM, Kai-Oliver Prott <kai.prott at hotmail.de> wrote:
> 
> 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 <mailto: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 <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
>> Only members subscribed via the mailman list are allowed to post.
> _______________________________________________
> 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/f49e7932/attachment.html>