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

 I conclude from this thread that
  * `OverlappingInstances` should probably obey the same rules as closed
 type families, for consistency.

  * But then both Oleg's versions would be rejected

  * "A foolish consistency is the hobgoblin of little minds".  But there is
 a reason for the consistency, namely that we know that type inference
 might become unpredictable (i.e. succeed on Tuesday but fail on Friday,
 because of some difference in the order in which the solver solves
 constraints) if we allowed the more flexible form.

  * We don't yet know if there is any way to accept the programs Oleg wants
 (or something like them) without allowing unpredictability to slip in too.

 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'd like to work this out; the inconsistency between overlappping
 instances and type families is troubling.

 Simon

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