On Thu, 14 Dec 2017 at 3:19 PM, David Feuer <redirect@vodafone.co.nz> wrote:
I still haven't really digested what you've written, but I wish to pick a nit (below)

Thanks David. Heh, heh. I think we might be agreeing about the phenomenon, but picking different nits to 'blame'.


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.

Hmm. I wonder what you think "closed" amounts to? 

Equation 1    `'False && b    = 'False` is consistent with `[b ~ Foo]`
   (unless GHC were to reason about closed kinds)

Equation 2    `'True  && b     = b   ` is consistent with `[b ~ Foo]`

And so on.

The last equation `a      && a    = a` is consistent with `[a ~ Foo]`.
Furthermore it's *inconsistent* with a putative backwards FunDep ` r a -> b` on `'False && 'True ~ 'False`.
I think it would be better to omit that equation all together.

Then when your o.p. reasons:

>>> ... we can calculate (Not a || Not b) as 'True for each of these LHSes.

What will it calculate for (Not Foo)?

Asking GHC to reason like this about open type families smells much harder, but maybe my sense of smell is off.
Hmm. Your o.p. said

>>> In order for the constraint (a && b) ~ 'True to hold, the type family application *must have reduced* using one of its equations.
I think that's smelly logic: if you want to reason backwards, then you can't make assumptions about what "must" have reduced if GHC were reasoning forward. That is, unless you're expecting GHC to behave like an SMT solver over closed kinds.

Remember that the logic for selecting Closed Type Family equations works from top to bottom *ignoring anything known about the result*. So not only must it have reduced using one of the equations; it must have rejected equations above the one it selected; and it must have seen evidence for rejecting them. (It's more complicated than that in practice: if there's coincident overlap, GHC will pick some equation eagerly. And your `&&` equations exhibit coincident overlap, apart from the last.)

If you want it to benefit from something known about the result, you won't (in general) find the same top-to-bottom sequence helps with type improvement. With the FunDep inconsistency in your last equation for `&&`, I suspect that equation-selection will get 'stuck' looking for evidence to reject earlier equations.

If we do expect GHC to behave like an SMT solver over closed kinds, then it can reason just as well for an open type family; on the proviso that it can see all the equations.

For a bit of history: during discussions around Injective Type Families, one suggestion was to infer injectivity by examining the equations given -- along the lines you're positing. That was rejected on grounds the equations might exhibit injectivity 'by accident'. Also that the programmer might intend injectivity, but their equations be inconsistent. So it was decided there must be explicit declaration; and the equations must be consistent with that declaration. No equations for `&&` could be consistent that way.

AntC