Re: [Haskell-cafe] Promoted data types

Hi David, My workaround is to use:

data K a where

   K0 :: forall a b. b -> K a

The kind `K Bool` contains things like:

:kind! K0 'True

(K0 'True) :: K Bool

:kind! K0 'False

(K0 'True) :: K Bool But also

:kind! (K0 Int :: K Bool)

(K0 Int :: K Bool) :: K Bool and I'd like to have a way to not allow to construct such a type. Oh!, what I just realised is that I can actually achieve what I want by simply declaring:

data K a where

   K0 :: forall a. a -> K a

Now the type constructor of a type of kind `K Bool`, must is `K0 'True`, `K0 'False`, or `K0` of some exotic type of kind `Bool`. Thanks for making me realise that! Regards, Marcin ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, May 3rd, 2021 at 22:44, David Feuer wrote:

On Mon, May 3, 2021, 8:04 AM 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.