[GHC] #14832: QuantifiedConstraints: Strengthening context causes failure

[GHC]

#14832: QuantifiedConstraints: Strengthening context causes failure
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints wipT2893
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):

 GHC is very careful about picking instances. See
 http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html
 #overlapping-instances, esp the bit about "all instances that unify".

 The constraint `rel xx xx` matches both `(Refl rel)` and `(Trans rel)`;
 but the (head of) the former is an instance of the (head of) the latter so
 it should win.  At least with overlapping instances on.  (There's no way
 to add an OVERLAPPING pragama to an individual quantified constraint --
 yet anyway.)

 The constraint `rel xx zz` could (if `zz` was further instantiated)
 match`(Refl rel)`, so GHC refains from picking it.  `IncoherentInstnaces`
 might help.

 In short, right now I'm being very conservative about ambiguity.  Once we
 pick the "wrong" path there is no way back -- GHC does no backtracking.

 I'm inclined to park this one until we have the basics nailed.

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