Fix "no skolem info" bugs
There are a lot of tickets for No skolem info. This ticket is about fixing them.
The goal
When reporting typechecker error messages, it helps to explain the provenance of a type variable. For skolems, that means where it is bound. For example
f :: forall a. [a] -> [a]
f x = blah
In error messages arising from blah
, if they mention the type variable a
, it helps to
say that it's the (rigid, skolem) type variable bound by the type signature f :: forall a. [a] -> [a]
.
The current mechanism
A typical error arises from a failure to solve some typing constraint, leading to a residual implication constraint (see Modular type inference with local assumptions) like
[W] forall a. (a ~ Int)
arising from a failed attempt to make a
equal to Int
. (Failed because a
is a skolem;
a type constant equal only to itself.)
An implication constraint is represented in GHC by an Implication
in GHC.Tc.Types.Constraint:
data Implication
= Implic {
ic_skols :: [TcTyVar],
ic_info :: SkolemInfo,
ic_wanted :: WantedConstraints,
...lots more fields...
}
The ic_skols
list the skolems (in our example, just [a]
); the ic_wanted
gives constraints inside the implication to be solved (in our example, a ~ Int
). Finally the ic_info
field describes the binding site, via the data type SkolemInfo
(defined in GHC.Tc.Types.Origin):
data SkolemInfo
= SigSkol UserTypeCtxt TcType [(Name,TcTyVar)]
| SigTypeSkol UserTypeCtxt
| ForAllSkol SDoc
...etc...
GHC's error reporting machinery uses the SkolemInfo
in enclosing Implications
to describe the free skolems mentioned an error message.
What goes wrong
The difficulty is that we sometimes generate constraints that mentions
a skolem that is not bound by the enclosing Implication
. That leads to the Dreaded "no skolem info" error.
I have tried repeatedly to solve this, but it just turns out to be tricky to do so.
One reason is that GHC's typechecker sometimes gets to the point where it cannot proceed, and so throws an exception in the monad. This is caught, and the typechecker recovers and tries to typecheck other bits of the program. But
- we don't want to discard the already-generated constraints -- they might express the very error that led to the exception
- yet the exception might bubble out past the code that would usually wrap these gathered constraints in an implication.
You might think that the implication-wrapping code could catch the exception, wrap, and re-throw. But it turns out to be extremely tricky to do this. It makes the code more complicated; and we have no guarantee that we have found all the bad places.
Generating entirely well-scoped constraints seems like the Right Thing, but we are convinced that it is not easy to achieve, starting from where we are. (Maybe we should elminate all exceptions?)
A slightly hacky solution
An alterantive plan is to put the SkolemInfo
in the type variable itself. We have
data TcTyVarDetails
= SkolemTv TcLevel Bool
| RuntimeUnk
| MetaTv { ...blah... }
Add SkolemInfo
to SkolemTv
.
A slight downside that I recall is that "tidying" a type variable should properly
involve tidying the SkolemInfo
, since the latter includes free type variables.
But that seems overkill for general tidying since when we are printing a type we
won't print the SkolemInfo for every type variable.
But that's fine: we can simply not tidy the SkolemInfo
; instead we can tidy it
when we print it in Tc.Errors.
Of course, we then need to plumb the right SkolemInfo
to the places we make
those skolems. And I have a feeling that a very few of them may be TyVars
not
TcTyVars
, as a short-cut; that short-cut then becomes no longer available.