Re: [Haskell-cafe] Promoted data types

Perhaps Marcin is looking for https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-ga... https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-ga..., 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 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@coot.me mailto:coot@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.