[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):

 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