<div>Hi David,<br><br>My workaround is to use:<br>> data K a where<br>>   K0 :: forall a b. b -> K a<br><br>The kind `K Bool` contains things like:<br>> :kind! K0 'True<br>(K0 'True) :: K Bool<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>> :kind! K0 'False<br>(K0 'True) :: K Bool<br><br>But also<br>> :kind! (K0 Int :: K Bool)<br>(K0 Int :: K Bool) :: K Bool<br><br>and I'd like to have a way to not allow to construct such a type.<br><br>Oh!, what I just realised is that I can actually achieve what I want by simply declaring:<br>> data K a where<br>>   K0 :: forall a. a -> K a<br>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`.<br><br>Thanks for making me realise that!<br><br>Regards,<br>Marcin<br><br></div><div class="protonmail_quote"><div>‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐<br></div><div> On Monday, May 3rd, 2021 at 22:44, David Feuer <david.feuer@gmail.com> wrote:<br></div></div><div><br></div><blockquote class="protonmail_quote" type="cite">
            <div dir="auto"><div dir="auto" class="gmail_quote"><div dir="ltr">On Mon, May 3, 2021, 8:04 AM  <<a href="mailto:coot@coot.me" rel="noreferrer nofollow noopener">coot@coot.me</a>> wrote:<br></div><blockquote style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex" class="gmail_quote">Currently with `DataKind` extension, Haskell allows to promote terms / types to types / kinds.  Currently, one cannot write:<br>
<br>
```<br>
data K a where<br>
  K0 :: forall (x :: a). x -> K a<br>
```<br></blockquote></div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto" class="gmail_quote"><blockquote style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex" class="gmail_quote"></blockquote></div></div>

        </blockquote>