I still haven't really digested what you've written, but I wish to pick a nit (below)

On Nov 20, 2017 3:44 AM, "Anthony Clayden" <anthony_clayden@clear.net.nz> wrote:

> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:

...

> For (&&), the obvious things you'd want are ...
>
> There's nothing inherently impossible about this sort of
reasoning.

No-ish but. It relies on knowing kind `Bool` is closed.
And GHC doesn't pay attention to that.
So you need to bring type family `Not`
into the reasoning; hence a SMT solver.

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.