#13674: GHC doesn't discharge heterogeneous equality constraint when it ought to -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:8 is essentially correct. Consider two scenarios: 1. We have a Given proving `blah` and a Wanted `blah`. We use the Given to solve the Wanted. Later, we learn that `blah` is `Lcm m m ~ m`, but nothing above changes. 2. We have a Given proving `blah`. We learn that `blah` is `Lcm m m ~ m`, so we mark it as insoluble. Then, we get a Wanted `blah`, which we see is `Lcm m m ~ m`. This, too, is marked as insoluble. In case 1, we'll succeed; in case 2, we'll fail. The problem is that the only difference in these cases is the order in which constraints are treated and/or solved, something notoriously difficult to control. The "fix" for this problem is not to error on occurs-checks, which would then allow us to succeed in case 2. That seems unsatisfactory, though, because even if occurs-checks don't immediately error, we'll have a hard time solving `m ~ Lcm m m` from `Lcm m m ~ m`. I'm inclined to say that we let this behavior stand. Note that when we accept the program, nothing goes wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13674#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler