<html><head>

<meta http-equiv="Content-Type" content="text/html; charset=utf-8">

  </head>

  <body>

    <p>Hi,</p>

    <p>I think I don't quite understand the question. <br>

    </p>

    <p>The code you propose seems wrong to me for a different reason: <br>

      The type constructor (->) for function values has Kind: * ->

      * -> *</p>

    <p>In fact, GHC will print this error when compiling the snippet

      with the corresponding extensions.</p>

    <p>Promoting a data type is done differently. <br>

    </p>

    <p>Can you elaborate on what exactly it is you are proposing?</p>

    <p>Sincerely<br>

      Kai Prott<br>

    </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>

    </div>

    <blockquote type="cite" cite="mid:U1A64IhqoeqlOTMYetw-yGGKOKwX0wJcc7ewU-TdHgUD_8VPZYMFFz3JUceGFTSRnpntnwooweKSbXECFfN71w5fHGWBWguMkW1SvuL7W14=@coot.me">

      <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>

      <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>

  </body>

</html>