[GHC] #12522: GHC 8.0.1 hangs, looping forever in type-checker

[GHC]

#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.

 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.

 > * 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.

 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