Track skolemization rather than avoiding it for error messages
Motivation
In https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs#L688-696 we have
{- Note [Don't skolemise unnecessarily]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are trying to solve
(Char->Char) <= (forall a. a->a)
We could skolemise the 'forall a', and then complain
that (Char ~ a) is insoluble; but that's a pretty obscure
error. It's better to say that
(Char->Char) ~ (forall a. a->a)
fails.
What if we could track the skolemization and requantiy everything for the error message? Then could instead say something like:
forall a. (Char ~ a)
is insoluble
Proposal
I don't have an exact proposal. I'm especially unclear how much this generalizes to other messages from the compiler.