[was ghc-devs] Reasoning backwards with type families

[David Feuer]

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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171213/a2598bd6/attachment.html>