#12522: GHC 8.0.1 hangs, looping forever in type-checker -------------------------------------+------------------------------------- Reporter: clinton | 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): OK I had a look. What is happening is this. We have a wanted constraint {{{ [W] TF (x_aDY, a_aJn) ~ s_aF4 FunEq }}} where `s_aF4` is a flatten-unification-variable; and in our mdel we have {{{ [D] s_aF4 ~ Maybe Char }}} We can't reduce the wanted constraint so we try irmpvoement. Now rightly or wrongly, "improvement" kicks in, by matching the constraint with the axiom {{{ type instance TF (D1 x, a) = Maybe (TF (x, a)) }}} In improvement we seem to use "pre-unification" from the paper, so that matching `Maybe Char` against `Maybe (TF (x,a))` succeeds. So we emit two new derived constraint {{{ [D] a_aJn ~ a_fresh1 [D] x_aDY ~ D1 x_fresh2 }}} The match on RHS is incomplete so we just get a "shape", with fresh unification variables. But that is bad. Now we take `[D] a_aJn ~ a_fresh1` as our next work item, unify `a_a7n := a_fresh`, kick out the TF FunEq, and now we are in an infinite loop. Question: why do we use pre-unification when matching the RHS in the injectivity-improvement step. That's what is causing the trouble. Richard? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12522#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler