13 Dec
2017
13 Dec
'17
9:06 p.m.
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"
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.