[GHC] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

[GHC]

#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      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:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Some reactions to all this:

 * comment:3 talks about parking `Coercible` constraints in the insolubles.
 I hope we don't -- they're not insoluble. I imagine you mean that they're
 parked in the "irreducibles", which is more sensible.

 * The representational equality solver is known to be incomplete. I
 believe the problem is simply undecidable. Perhaps this could be better
 documented, but its incompleteness is precisely in recursive situations.

 * I agree that the reason for occurs-checks isn't about solubility, but
 rather about keeping the solver from going into gratuitous loops.

 Bottom line: I don't have any better ideas. I doubt we can make the
 `Coercible` solver more complete without gross hacks. And, absent a Real
 Use Case, I'm not keen on trying.

 I have not digested all of #12466 about nominal equalities, which I tend
 to think are more worrisome.

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