[GHC] #12660: singletons doesn't compile with GHC 8.0.2 snapshot

[GHC]

#12660: singletons doesn't compile with GHC 8.0.2 snapshot
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.2
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I now know what is happening.

 * At some point we have a Given
 {{{
 [G] Tuple3Sym3 x1 x2 y ~ Tuple3Sym3 n0 n1 n2
 }}}

 * Currently we make derived constraints from injectivity from Givens, so
 we get
 {{{
 [D] n1 ~ x2
 }}}
   This becomes part of the "model".

 * Inside a further nest of implication constraints we are processing the
 Givens, and end up adding this to the inert set:
 {{{
 [G] (n1 - n0) ~ fsk    (CFunEqCan)
 }}}

 * But since that can be rewritten by the model, we emit a derived "shadow"
 of the Given:
 {{{
 [D] (n1 - n0) ~ fsk    (CNonCanonical)
 }}}

 * When processing that Derived constraint, we add
 {{{
 [D] (n1 - n0) ~ fuv   (CFunEqCan)
 }}}
   to the flat-cache

 * Now we finish processing the Givens and start doing the Wanteds.  We get
 a hit in the flat-cache, so 'fuv' nwo shows up in the residual wanteds.
 Then during un-flattening we unify that fuv.  At this point the assumption
 is that CFunEqCan can't reappear. But it's still there in the flat-cache,
 and when we re-solve the Wanteds we find hit again.  But this time fuv is
 unified and chaos results.

 What to do?  I can think of a number of alternatives.

 1. For now the simple thing to do is to start processing the Wanteds with
 an empty flat-cache. This is easily done in `nestTcS`.  But it's
 unsatisfactory because it discards useful Given entries in the flat-cache.

   Still, it's a 2-line quick-and-dirty fix that does solve the problem (I
 tried it).

 2. We could address the unsatisfactory aspect of (1) by selectively
 purging the flat-cache, but I dislike that.  Seems like a lot of work
 (both code and execution time) for an edge case.

 3. We could simply not generate derived shadows for Given constraints.
 This is clean, simple, and will generate fewer deriveds.  I have been
 unable to construct an example where we need to rewrite a Given with a
 (derived) model constraints to make useful progress.  Can anyone else
 construct one?

 4. We could still emit derived shadows from Givens, but in a less
 aggressive way, so that they don't pollute the flat-cache

 I'm going to try (3).

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