<div dir="auto"><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Mon, May 3, 2021, 8:04 AM  <<a href="mailto:coot@coot.me">coot@coot.me</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 class="gmail_quote" dir="auto"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div></div>