[GHC] #13284: Incoherent instance solving is over-eager

[GHC]

#13284: Incoherent instance solving is over-eager
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       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):

 There is a real difficulty with what you are asking for.  The constraint
 solver sees a single 'wanted' constraint:
 {{{
 [W] CTest Int alpha
 }}}
 where `alpha` is a unification variable standing for an as-yet-unknown
 type.  It tries to solve it; and with `IncoherentInstances` it can do so
 with the `CTest a out` instance.  But that's not what danilo2 wants.  He
 wants the solver to leave it unsolved, and instead generate the 'derived'
 instance coming from the fundep. So we add the new constraint
 {{{
 [D] alpha ~ String
 }}}
 Now we can solve `alpha := String`, so the original constraint becomes
 {{{
 [W] CTest Int String
 }}}
 which can be solved with the `CTest Int String` instance.

 All this depends on waiting until some other unification happens, to
 render `[W] CTest Int alpha` soluble.  But when shoudl we give up and use
 the `CTest out a` instance anyway?  Suppose there wasn't a fundep on
 `CTest` and we had
 {{{
 [W] CTest Int alpha
 [W] Boo [Tree (alpha, Int)]
 }}}
 and after a lot of work, applying instances etc, the second constraint
 simplifies to something that unifies `alpha := Int`.  Aha!  Now we can
 solve the first one.

 So you might say "solve using all rules EXCEPT incoherent instances, and
 THEN apply incoherent instances".  But that isn't well defined.  E.g.
 {{{
 [W] C1 Int alpha
 [W] C2 Int alpha
 }}}
 Suppose both have incoherent instances.  Should I solve the first with the
 incoherent instance (thereby, perhaps, fixing `alpha`)?  Or the second?
 We might get quite different answers.

 You could say "well, just do your best; incoherence is, well, incoherent".
 So yes, I suppose we could take a bit more trouble to delay using
 incoherent instances.  Would enough people care?  I don't know.

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