You're absolutely right that improvement doesn't solve your problem. But what I didn't say is that there is no real reason (I think) that we can't improve improvement to produce givens. This would likely require a change to the coercion language in Core (and thus not to be taken lightly), but if we can identify a class of programs that clearly benefits from that work, it is more likely to happen. The thoughts about improvement were just a very basic proof-of-concept. Sadly, the proof-of-concept failed, so I think a first step in this direction would be to somehow encode these partial improvements, and then work on changing Core. That road seems too long, though, so in the end, I think constrained type families (with superclass constraints) might be a more fruitful direction.

Could closed type families move beyond injectivity and functional dependencies by applying closed-world reasoning that derives solutions of arbitrary equalities, provided a unique solution exists? Consider this example:

type family J a where

  J Int = Char

  J Bool = Char

  J Double = Float

One might reasonably expect that if we wish to prove (J a ∼ Float), we will simplify to (a ∼ Double). Yet GHC does not do this as neither injectivity nor functional dependencies can discover this solution.