[GHC] #15846: Re-examine mkResidualConstraints

[GHC]

#15846: Re-examine mkResidualConstraints
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> Simon and I spent some time debating `TcSimplify.mkResidualConstraints`.
> 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 in `simplifyInfer`.
>
> *  The `promoteTyVarSet` call in `mkResidualConstraints` appears to be
> entirely redundant, because anything that gets caught there should also
> have been caught in `decideMonoTyVars`.
>
> * 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.

New description:

 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 in `simplifyInfer`.

 *  The `promoteTyVarSet` call in `mkResidualConstraints` appears to be
 entirely redundant, because anything that gets caught there should also
 have been caught in `decideMonoTyVars`.

 * 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.

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15846#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler