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

 Well, this is annoying.  The definition of `Coercible` is roughly this
 {{{
 class (a ~R# b) => Coercible a b
 }}}
 So then

 * When we have `[G] Coercible b (f b)` we put that into the inert set, and
 add its superclasses `[G] b ~R# f b`.

 * The given `[G] b ~R# f b`  has an occurs check, so we "park" it in the
 insolubles.

 * Now we try `[W] Coercible b (f b)`.  Aha!  We have precisely that inert
 in the inert set, so we solve it.

 If we switch te type sig to `Coercible (f b) b` then something slightly
 different happens:

 * `[G] Coercible (f b) b` is put into the inert set; then add its
 superclasses `[G] f b ~R# b`.

 * The given `[G] f b ~R# b` normalised to `b ~R# f b` but has an occurs
 check, so we "park" it in the insolubles.

 * Now we try `[W] Coercible b (f b)`.  Alas!  No matching dictionary
 exists, so is reported as "can't solve".

 The inconsistency here is that when the givens are insoluble we may not
 (indeed cannot) fully normalise them and use them to solve the wanteds.
 But it's hard to spot that the `Coercible` dictionary (just another class
 to the solver) is insoluble because its superclass is.

 I'm not sure what to do here.  Since it's all to do with a wrong program
 anyhow, maybe it does not matter too much.

 Incidentally the same thing can happen with nominal equality:
 {{{
 class (a~b) => C a b

 foo :: C a b => a -> b
 foo x = x

 hm2 :: C b (f b) => b -> f b
 hm2 x = foo x

 hm3 :: C (f b) b => b -> f b
 hm3 x = foo x
 }}}
 Here `hm2` typechecks because of the exactly-matching given `C b (f b)`
 dictionary, but `hm3` does not.

 (Actually `hm3` fails to typecheck but regrettably does not emit an error
 message. That's a separate bug which I'm fixing.)

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