The Importance of Equality in GHC

The inversion of maybe is a good one, yes. Does it even exist? Sure it does. So that's a type family. And it turns out that that equality is sometimes useful. We'd like to be able to do something with it, but we can't do the normal thing with it. It turned out that these two things are really quite similar. And there's a third one involving type checker levels, which I won't even explain. But we identified that there were three different stories and could sort of unify all of these into a common structure. This was a nice little bit of refactoring that is more expressive than any of the individual pieces.