[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 simonpj):

 > Thus, I'd argue that hm2 and hm3 are not wrong programs.

 Hmm.  That's a good point.  But we solve constraints, both `~#` and `~R#`
 by normalising and then rewriteing.  So if we have
 {{{
 [G] b ~R# f b
 [W] b ~R# blah
 }}}
 then we can use the given to rewrite the wanted to
 {{{
 [W] b ~R# blah
 ==> [W] f b ~R# blah
 ==> [W] f (f b) ~R# blah
 ..etc...
 }}}
 We don't want to do that.  So we park the given and don't use it for
 rewriting.

 So maybe the point is not that the code is inaccessible, but rather that
 we don't have a complete solver.  Hmm.

 I wonder what Richard and Stephanie think?

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