<div>Thanks Richard, indeed that proposal would not help. The snippet I posted is a valid GADT syntax. When it is compiled with `DataKinds`, `PolyKinds` and `KindSignatures` ghc is is quite explicit why it refuses it: Expected a type, but `x` has a kind `a`, which is exactly what you said.<br><br>However, I think it would be quite reasonable to accept it. In general ghc would only need to generate code for the case `a ~ Type`, all other use cases at term level must be refused. It might be enough to add a type inference rule which injects `a ~ Type` for any such term. <br><br>Another missing puzzle is that there's no way to specify that one only wants the promoted types / kinds without the term level part. This could be done by specifying an explicit kind signature:<br>```<br>type K0 :: a -> K a<br></div><div class="protonmail_signature_block protonmail_signature_block-empty"><div class="protonmail_signature_block-user protonmail_signature_block-empty"></div><div class="protonmail_signature_block-proton protonmail_signature_block-empty"></div></div><div><div>data K a where<br></div><div> K0 :: forall a (x :: a) -> K a<br></div><div>```<br></div><div>Now this is refused with `The standalone kind signature for 'K0' lacks an accompynying binding`.<br><br></div><div>It's not the first time I stumbled upon this. The latest incarnation is a gist in which I worked out how to encode pipelining using a type level queue / list in a session type framework which we use at work for developing protocols: <br></div><a href="https://gist.github.com/coot/b568ebc7bac2e4e31cb54bf3939419d8#file-pipelined-hs-L94">https://gist.github.com/coot/b568ebc7bac2e4e31cb54bf3939419d8#file-pipelined-hs-L94</a></div><div class="protonmail_quote"><div><br>Richard, does it sound reasonable to you? If so, what would be the right process to propose / implement such a feature? I don't think it would require a new extension, rather modify how `DataKind` works in presence of `PolyKinds` and `StandaloneKindSignatures`.<br><br>Maybe this is in scope of the dependent type Haskell workstream that you're doing?<br><br>Best regards,<br>Marcin<br><br>‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐<br></div><div> On Monday, May 3rd, 2021 at 16:11, Richard Eisenberg <rae@richarde.dev> wrote:<br></div></div><div><br></div><blockquote class="protonmail_quote" type="cite">
Perhaps Marcin is looking for <a class="" href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst" target="_blank" rel="noreferrer nofollow noopener">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 class="" type="cite"><div class="">On May 3, 2021, at 9:10 AM, Kai-Oliver Prott <<a class="" href="mailto:kai.prott@hotmail.de" rel="noreferrer nofollow noopener">kai.prott@hotmail.de</a>> wrote:</div><br><div 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 href="mailto:coot@coot.me" rel="noreferrer nofollow noopener">coot@coot.me</a> wrote:<br class="">
</div>
<blockquote class="" type="cite">
<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></fieldset>
<pre wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank" rel="noreferrer nofollow noopener">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 class="" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank" rel="noreferrer nofollow noopener">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>
</blockquote>