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_clay...@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.
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
