#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