#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here’s a slightly simpler example {{{ type instance F (Succ x) = Succ (F x) [W] alpha ~ Succ (F alpha) }}} Solving the constraint goes like this: {{{ Flatten: [W] alpha ~ Succ fuv (CTyVarEq) [W] F alpha ~ fuv (CFunEqCan) Unify alpha := Succ fuv; there’s no occurs check here; and substitute in the other constraint [W] F (Succ fuv) ~ fuv (CFunEqCan) Now we can fire the rule (hooray?) [W] Succ (F fuv) ~ fuv }}} Normally we’d declare at this point that we have figured out what `fuv` is, so we call `dischargeFmv` to update it in place. But we don’t want to unify `fuv := Succ (F fuv)` because that’s makes an infinite type. So instead we turn the fuv into an ordinary unification variable beta, thus `fuv := beta`. So now we have {{{ [W] Succ (F beta) ~ beta }}} And lo, that’s exactly what we started with, so the whole process iterates. This is terrible. It’s a kind of occurs-check loop, but it goes via function call. If we didn’t do flattening we’d have `[W] alpha ~ Succ (F alpha)`, which is an occurs check, so we would not substitute for alpha. Instead we put such occurs-check equalities aside in the “insoluble”. But we do flatten! Of course this example isn’t soluble, but this variant is: {{{ type instance F (Succ a) = Zero [W] alpha ~ Succ (F alpha) }}} Now if we flatten, unify alpha we get {{{ [W] F (Succ fuv) ~ fuv }}} Now fire the rule, and we get {{{ Zero ~ fuv }}} Which is a fine solution. However I would not be too bothered if we didn’t find it. So what should we do? Its bad bad bad for the solver to diverge: note that the type family instance for `F` is perfectly nice. I wasted an entire evening thinking about and trying several ideas, none of which worked. One possibility I didn’t try is to beef up the “occurs check” so that when seeing if `a ~ ty` has an occurs check, we unflatten on-the-fly to see if `a` occurs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12444#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler