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