Hi devs, I've recently made a design decision for GHC 8.0 that I may wish to revisit, and I'd love some feedback. GHC 7.x has but one user-visible type equality relation, ~. The constraint (ty1 ~ ty2) is well-kinded only when ty1 and ty2 have the same kinds. And the solver works in terms of this very same equality, so error messages simply talk about ~. GHC 8.0, on the other hand, has three equality relations that might potentially appear to users. It retains ~. But it also has ~~, which is heterogeneous type equality, meaning that (ty1 ~~ ty2) is well-kinded even when ty1 and ty2 have different kinds. And it has ~#, which is the unlifted equality used in the solver. It turns out that ~~ and ~ are just wrappers around ~#. Because of all of this, GHC sometimes ends up thinking about ~~ or ~# even when the user has said ~. (See the definition of ~ in Data.Type.Equality, for example.) And it naively would print ~# a bunch in error messages. So, I put a little pretty-printing magic in that prints ~, ~~, and ~# all as ~ in user-facing output, unless the user writes -fprint-equality-relations. This design decision has kept error messages pretty. But it will be awfully confusing when someone intentionally uses ~~ and sees ~ in their output. And there's nothing to suggest -fprint-equality-relations. These sorts "hide the scary plumbing!" decisions irk me to no end when I find them in my operating system. But now I've done the same thing in GHC... which is why I want to re-examine this. What do you think? Do you see a better way to handle this? Thanks! Richard