What I find strange is that we're using the model when triggering improvement as we're looking at a Wanted. Doesn't the model (that is, all
#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): I've re-read our Haskell Symposium '15 paper "Injective type families". It's rather good! Section 5.2 covers exactly the point at issue here. * You point out above that we can really also produce `[D] Char ~ TF (x_fresh2, a_fresh1)`. Very true! WE don't currently do that. Moreover, this idea is missing from Section 5.2 in the paper. In the example here we should add `[D] G beta ~ Int`, shouldn't we? Doing so could lead to more progress. Would you like to cook up an example that will only work if we do this? * How to avoid the loop? Well we basically emit `[D] (x_aDY, a_aJn) ~ (D x_fresh2, a_fresh1)`. When we boil this down to `a_aJn ~ a_fresh1` we really really want to unify `a_fresh1 := a_aJn`. If we do it the other way round we get the infinite loop. Or to put it another way, we don't want to invent more fresh variables than we need to. In this case, let's no invent `a_fresh1` at all; just re-use `a_aJn`. You might think of it as an optimisation, but acutally it's essential to avoid the loop. the Derived constraints) live off in its own world with minimal interaction with Wanteds? Every Wanted effectively has a "shadow Derived" behind it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12522#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler