Thank you Richard, everything clear now.


Sent from ProtonMail mobile



-------- Original Message --------
On 3 May 2021, 23:57, Richard Eisenberg < rae@richarde.dev> wrote:

Sounds like you've figured this out, so I won't write a long response to your previous email -- but let me know if there are still outstanding questions there.

Thanks,
Richard

On May 3, 2021, at 5:26 PM, coot@coot.me wrote:

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!