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
mkResidualConstraintswill 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 in
mkResidualConstraintsappears to be entirely redundant, because anything that gets caught there should also have been caught in
- So the only time that we should do work in
mkResidualConstraintsis 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.