Re-examine mkResidualConstraints
Simon and I spent some time debating TcSimplify.mkResidualConstraints
and the accompanying Note [Emitting the residual implication in simplifyInfer]
.
Here is what we learned:
- The current code handles covars at the top level only. At one point, we were worried about covars in nested implications. But I conjecture this can't happen, because these would necessarily be instances of skolem-escape, prevented elsewhere. (Why skolem-escape? Because the covar would mention local skolems, and yet appears in the type of the variable(s) we're trying to infer.)
- We think that any covars that come through
mkResidualConstraints
will never be solved. That's because there can't be given equality from an outer context -- if there were, we'd be in the "let should not be generalized" case and wouldn't be insimplifyInfer
. - The
promoteTyVarSet
call inmkResidualConstraints
appears to be entirely redundant, because anything that gets caught there should also have been caught indecideMonoTyVars
. - So the only time that we should do work in
mkResidualConstraints
is when we have deferred type errors. Perhaps with that insight, it can be simplified.
This ticket is to track our understanding of this function, settle on a way to improve it, and then execute that change. At the minimum, we should figure out whether that promoteTyVarSet
is necessary.