[Haskell-cafe] Promoted data types

[coot at coot.me]

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.

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.

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:

```

type K0 :: a -> K a

data K a where
  K0 :: forall a (x :: a) -> K a
```
Now this is refused with `The standalone kind signature for 'K0' lacks an accompynying binding`.

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:
https://gist.github.com/coot/b568ebc7bac2e4e31cb54bf3939419d8#file-pipelined-hs-L94

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

Maybe this is in scope of the dependent type Haskell workstream that you're doing?

Best regards,

Marcin

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Monday, May 3rd, 2021 at 16:11, Richard Eisenberg <rae at richarde.dev> wrote:

> Perhaps Marcin is looking for 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 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
> > > 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/e3b71901/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 509 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/e3b71901/attachment.sig>