#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 goldfire): Replying to [comment:13 simonpj]:
I've re-read our Haskell Symposium '15 paper "Injective type families". It's rather good!
Glad you like it. :)
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.
* 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
But I wonder if we need to. The existing machinery for dealing with type functions should add that equality in short order once we do the partial improvement. Perhaps that's why we left this out of the paper. 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. I trust your judgment here, but it all looks rather fragile. What termination property does setting `a_aJn := a_fresh1` violate? Or, said differently, ''why'' does this fix the problem. You might say "you won't kick out the `FunEqCan`" and you'd be right, but that doesn't seem like a fundamental enough reason. But perhaps this is a battle for another day.
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 the Derived constraints) live off in its own world with minimal interaction with Wanteds?
Every Wanted effectively has a "shadow Derived" behind it.
Yes, I suppose I knew that. But I thought these Deriveds only come into play when working with other Deriveds. Put another way: should we try improvement only when working with Deriveds? Given your statement above about shadow Deriveds, my new plan would seem to cover all cases where we try improvement now, but we would seemingly be saved from this loop. Am I missing anything? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12522#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler