Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information