<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Perhaps Marcin is looking for <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst" class="">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst</a>, 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.<div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On May 3, 2021, at 9:10 AM, Kai-Oliver Prott <<a href="mailto:kai.prott@hotmail.de" class="">kai.prott@hotmail.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" class="">
<div class=""><p class="">Hi,</p><p class="">I think I don't quite understand the question. <br class="">
</p><p class="">The code you propose seems wrong to me for a different reason: <br class="">
The type constructor (->) for function values has Kind: * ->
* -> *</p><p class="">In fact, GHC will print this error when compiling the snippet
with the corresponding extensions.</p><p class="">Promoting a data type is done differently. <br class="">
</p><p class="">Can you elaborate on what exactly it is you are proposing?</p><p class="">Sincerely<br class="">
Kai Prott<br class="">
</p>
<div class="moz-cite-prefix">On 03.05.21 14:04, <a class="moz-txt-link-abbreviated" href="mailto:coot@coot.me">coot@coot.me</a> wrote:<br class="">
</div>
<blockquote type="cite" cite="mid:U1A64IhqoeqlOTMYetw-yGGKOKwX0wJcc7ewU-TdHgUD_8VPZYMFFz3JUceGFTSRnpntnwooweKSbXECFfN71w5fHGWBWguMkW1SvuL7W14=@coot.me" class="">
<pre class="moz-quote-pre" wrap="">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
</pre>
<br class="">
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
</blockquote>
</div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></body></html>