<div dir="auto">I still haven't really digested what you've written, but I wish to pick a nit (below)<br><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Nov 20, 2017 3:44 AM, "Anthony Clayden" <<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>> wrote:<br type="attribution"><blockquote class="m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:<br>
<br>...<br>
<br>
> For (&&), the obvious things you'd want are ...<br>
><br>
> There's nothing inherently impossible about this sort of<br>
reasoning.<br>
<br>
No-ish but. It relies on knowing kind `Bool` is closed.<br>
And GHC doesn't pay attention to that.<br>
So you need to bring type family `Not`<br>
into the reasoning; hence a SMT solver.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I don't think this is entirely correct. The fact that Bool is closed does not seem relevant.  The key fact, I believe, is that (&&) is closed. Asking GHC to reason like this about open type families smells much harder, but maybe my sense of smell is off.</div><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="m_6484221779925235617quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div></div></div>