[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:10 simonpj]:
 > I conclude from this thread that
 >  * `OverlappingInstances` should probably obey the same rules as closed
 type families, for consistency.

 Generally agreed here, with the same reservations that Simon writes.

 >
 > I suppose that we could lift the restriction (ie strengthen the "surely-
 apart" check) if some flag is set:
 >  * I believe that the unpredictability only strikes if you have infinite
 types, via a looping type family.  And a programmer might well be willing
 to guaranteed that will not occur.
 >  * In that sense, it's a bit like `-XUndecidableInstances`: the
 programmer takes responsibility.
 >  * And, as such it should probably be a per-type-family (or per-closed-
 type-family) pragma, rather than a global flag.  Maybe even `{-#
 UNDECIDABLE #-}`.

 I'm not sure exactly what you mean here (mostly). The `{-# UNDECIDABLE
 #-}` route is almost surely a good idea, independent of anything else, as
 it follows the new pattern started by `{-# OVERLAPPABLE #-}` and friends.

 But, critically, a dangerous use of a strengthened apartness check would
 happen on a family '''without''' this pragma. For example:

 {{{
 type family Equals a b where
   Equals a a = True
   Equals a b = False
 }}}

 This clearly has no loops and should compile without `{-# UNDECIDABLE
 #-}`. Yet, if we use the strengthened apartness check when choosing to
 reduce by the second equation, we can get into trouble. Specifically,
 should `Equals x [x]` reduce to `False`, for some skolem `x`? If, in some
 future module, we introduce `type family Loop where Loop = [Loop]`, then
 it would be terrible to have reduced `Equals x [x]` to `False`. But, of
 course, we have no way of knowing if `Loop` will come into being in the
 future.

 The nub of the problem, as I see it, is that the safety (for closed type
 families) or predictability (for class instances) of the system depends on
 some '''global''' no-looping property.

 I could see some `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma that
 could be put on `Equals` that would enable the stronger check and let the
 programmer bear the safety burden. However, this is a significant
 departure from other "let the programmer beware" issues in that, for
 closed type families, you can abuse this ability to implement
 `unsafeCoerce`. (This would not be the case for class instances.)

 So, getting back to Simon's proposal: what's your suggested behavior? I
 see what you want with `{-# UNDECIDABLE #-}`, but I don't see precisely
 how it would influence the apartness check.

 If we are going to start treating undecidable instances as different than
 regular ones, it would be worthwhile to make the termination checker
 smarter. Right now, a standard Peano multiplication type family requires
 `-XUndecidableInstances`. I think the assumed safety of that extension (I
 think folks are OK with a perhaps-looping compiler, as long as the
 produced binary, if any, is type-safe) allows people to use it without
 much hesitation, so there has been little (no?) pressure to improve the
 termination checker.

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