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

 Replying to [comment:15 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.

 This seems to be precisely my {-# UNSAFE_STRONGER_APARTNESS_CHECK #-}`
 pragma. Declaring this property of a type function seems orthogonal to
 whether or not evaluating the function terminates -- I could see both `{-#
 UNDECIDABLE #-}` and `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` as separate
 pragmas, where neither implies the other. The first means that GHC might
 not terminate; the second means your program might not be type-safe.

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

 See #8162. That example uses open type families, and will compile and seg-
 fault with 7.6.3. The improved checking in 7.8.x stops compilation.
 However, an open type family with all of its instances in one module (such
 as `F` in #8162) is fully equivalent to a closed type family (with
 equations in any order). Why? Because all open type family instances must
 be ''compatible'', and a closed type family where all the equations are
 compatible skips the apartness check during reduction. (See the closed
 type families paper for details.) Thus, if we did the wrong apartness
 check (that is, ignored the possibility of infinite types) in 7.8.x, then
 an example along the lines of #8162 would cause a seg-fault.

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

 I tried and failed at this, and I've decided it's impossible. Without
 using type families, classes introduce no new type axioms -- even with
 equality superclasses. Without any axioms, the proof of progress of FC is
 quite straightforward and has no surprises. Thus, any program with an
 implementation of `unsafeCoerce` must fail to be well-typed in FC. So,
 barring Core Lint errors, this trick shouldn't be possible.

 So, I maintain my earlier position: what we have now is sound, but perhaps
 unpredictable in extreme cases. I ''do'' think we should make the class
 overlap check echo the type family overlap check, but I don't think
 there's a soundness issue here.

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