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

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

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12522#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler