[GHC] #12444: Regression: panic! on inaccessible code with constraint

[GHC]

#12444: Regression: panic! on inaccessible code with constraint
-------------------------------------+-------------------------------------
        Reporter:  zilinc            |                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):

 Here’s a slightly simpler example
 {{{
 type instance F (Succ x) = Succ (F x)

 [W] alpha ~ Succ (F alpha)
 }}}
 Solving the constraint goes like this:
 {{{
 Flatten:
 [W] alpha ~ Succ fuv  (CTyVarEq)
 [W] F alpha ~ fuv     (CFunEqCan)

 Unify alpha := Succ fuv; there’s no occurs check here;
 and substitute in the other constraint
 [W] F (Succ fuv) ~ fuv    (CFunEqCan)

 Now we can fire the rule (hooray?)
 [W] Succ (F fuv) ~ fuv
 }}}
 Normally we’d declare at this point that we have figured out what `fuv`
 is, so we call `dischargeFmv` to update it in place.   But we don’t want
 to unify `fuv := Succ (F fuv)` because that’s makes an infinite type.

 So instead we turn the fuv into an ordinary unification variable beta,
 thus `fuv := beta`.  So now we have
 {{{
 [W] Succ (F beta) ~ beta
 }}}
 And lo, that’s exactly what we started with, so the whole process
 iterates.

 This is terrible.  It’s a kind of occurs-check loop, but it goes via
 function call.  If we didn’t do flattening we’d have   `[W] alpha ~ Succ
 (F alpha)`, which is an occurs check, so we would not substitute for
 alpha.  Instead we put such occurs-check equalities aside in the
 “insoluble”.  But we do flatten!

 Of course this example isn’t soluble, but this variant is:
 {{{
 type instance F (Succ a) = Zero
 [W] alpha ~ Succ (F alpha)
 }}}
 Now if we flatten, unify alpha we get
 {{{
 [W] F (Succ fuv) ~ fuv
 }}}
 Now fire the rule, and we get
 {{{
 Zero ~ fuv
 }}}
 Which is a fine solution.  However I would not be too bothered if we
 didn’t find it.

 So what should we do?  Its bad bad bad for the solver to diverge: note
 that the type family instance for `F` is perfectly nice.

 I wasted an entire evening thinking about and trying several ideas, none
 of which worked.  One possibility I didn’t try is to beef up the “occurs
 check” so that when seeing if `a ~ ty` has an occurs check, we unflatten
 on-the-fly to see if `a` occurs.

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