#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): Here's what is happening * The given `b ~ f b` has an occurs check, so it's insoluble. It's a bit like saying {{{ f :: (Int ~ Bool) => blah }}} * In the long discussion on #12466 (see `Note [Given errors]` in `TcErrors` we decided not to complain about insoluble givens. * So the given `b ~ f b` is just parked. * Now we try to solve `b ~ f b`. Lo, it has an occurs-check error. Which we report. Seems reasonable to me, except for the lack of a complaint about the insoluble given; better ideas welcome (but look at #12466). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14323#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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

#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 RyanGlScott): Given that the incompleteness of the representational equality solver has spawned at least a couple of Track tickets (this one and #14247, off the top of my head), it would be nice to document all of this somewhere. (Perhaps `Data.Coerce`?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14323#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): comment:8 done in {{{ commit f20cf982f126aea968ed6a482551550ffb6650cf Author: Simon Peyton Jones Date: Mon Oct 9 13:16:59 2017 +0100 Remove wc_insol from WantedConstraints This patch is a pure refactoring, which I've wanted to do for some time. The main payload is * Remove the wc_insol field from WantedConstraints; instead put all the insolubles in wc_simple * Remove inert_insols from InertCans Instead put all the insolubles in inert_irreds * Add a cc_insol flag to CIrredCan, to record that the constraint is definitely insoluble Reasons * Quite a bit of code gets slightly simpler * Fewer concepts to keep separate * Insolubles don't happen at all in production code that is just being recompiled, so previously there was a lot of moving-about of empty sets A couple of error messages acutally improved. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14323#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler