Reasoning backwards with type families

[David Feuer]

Sometimes it woulld be useful to be able to reason backwards about type families.
For example, we have

type family a && b where
  'False && b      = 'False
  'True  && b      = b
  a      && 'False = 'False
  a      && 'True  = a
  a      && a      = a

If we know something about either of the arguments, we can choose an equation and
learn something about the result. But if we know something about the *result*, GHC doesn't
give us any way to learn anything about the arguments. For (&&), the obvious things you'd
want are

    prj1 :: (a && b) ~ 'True => a :~: 'True
    prj2 :: (a && b) ~ 'True => b :~: 'True
    flop :: (a && b) ~ 'False => (Not a || Not B) :~: 'True

There's nothing inherently impossible about this sort of reasoning. In order for the
constraint  (a && b) ~ 'True to hold, the type family application *must have reduced*
using one of its equations. The only possibilities are

    'True && b = b
    a && 'True = a
    a && a = a

Substituting 'True for each RHS gives

    'True && 'True = 'True
    'True && 'True = 'True
    'True && 'True = 'True

So in each case, the first argument is forced to 'True.

Similarly, if (a && b) ~ 'False, we look at all the possibilities:

  'False && a      = 'False
  'True  && a      = a
  a      && 'False = 'False
  a      && 'True  = a
  a      && a      = a

Substituting 'False for each RHS,

  'False && a      = 'False
  'True  && 'False  = 'False
  a      && 'False = 'False
  'False  && 'True  = 'False
  'False  && 'False      = 'False

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

Now consider (==), which is recursive:

    type family (a :: k) == (b :: k) :: Bool where
      f a == g b = f == g && a == b
      a == a = 'True
      _ == _ = 'False

We'd really like to know that

    eqEqual :: (a == b) ~ 'True => a :~: b
 ::
For eqEqual, we can reason thus: if  (a == b) ~ 'True, then we obtained that
result from one of the equations

    f a == g b = f == g && a == b
    a == a = 'True

In the base case, a ~ a on the LHS. In the recursive case, the RHS being 'True
tells us (using the reasoning for (&&)) that  (f == g) ~ True and that
(a == b) ~ True. Inductively, we conclude that f :~: g and a :~: b. Shifting
to the LHS, we conclude that f a ~ g b.


I wouldn't necessarily expect GHC to be able to work something like this out on
its own. But it seems like there should be some way to allow the user to guide
it to a proof. A tantalizing feature is that we're essentially reasoning about
execution traces, which are necessarily finite. It at least *seems* that this
should mean that the induction is well-founded. Now why should anyone
care about this sort of business? Because the runtime representation of, say,
(a == b && c /= d) :~: 'True is smaller than the runtime representation of
(a :~: b, c :~: d -> Void). So it would be nice to be able to recover the latter
from the former. Can we do it?

David