[Haskell-cafe] Promoted data types

[David Feuer]

On Mon, May 3, 2021, 8:04 AM <coot at coot.me> wrote:

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

I feel like I'm missing something. Suppose `a` is not Type but rather, say,
Bool. Then `x` has kind Bool. That is, x is 'True, 'False, or something
exotic. K0 @Bool is then a function that takes anything of type 'True or
type 'False and gives you something of type K Bool. What I think Richard is
getting at is that there isn't anything of type 'True or type 'False,
whether at the term level or the type level. These things only exist when
`a` is Type (or TYPE rep for some rep :: RuntimeRep). So it's pretty hard
to see what you're trying to do.

>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/959d83ff/attachment.html>