[GHC] #9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family

[GHC]

#9918: GHC chooses an instance between two overlapping, but cannot resolve a
clause within the similar closed type family
-------------------------------------+-------------------------------------
        Reporter:  qnikst            |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.8.3
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by simonpj):

 The straw-man proposal is that with `{-# UNDECIDABLE #-}` (or some other
 pragma name) on a closed type family, the surely-apart check is
 strengthened, allowing more reductions to fire.

 Richard, you rightly point out that if you put that on `Equal`, then
 `Equal x [x]` would return `False`, as you'd expect if all types were
 finite.  But you also claim that if you can define an infinite type, then
 you can get `unsafeCoerce`.  I believe you (c.f Section 6 of the
 [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
 Closed Type Families paper]).  But can you exhibit an example?

 And if you can, can you translate it back into an example using
 overlapping classes, probably with equality superclasses?  If so, perhaps
 our existing compiler is unsound!

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