[GHC] #9210: "overlapping instances" through FunctionalDependencies

[GHC]

#9210: "overlapping instances" through FunctionalDependencies
--------------------------------------------+------------------------------
        Reporter:  rwbarton                 |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.2
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------
Changes (by simonpj):

 * cc: dimitris@…, diatchki (added)


Comment:

 I can at least explain what is going on. I defer to Iavor (the Functional
 Dependency Expert) on what the right thing to do might be.

 == Problem 1: Should these instance declarations be accepted at all?  ==

 After all, unifying the a,b,s components of the instances shows that the
 constraint `Foo (x,x) ?? x y` would match both instances, and hence (via
 the fundep) force `??` to be both `(y,x)` and `(x,y)` respectively.

 GHC doesn't currently complain about this, I think because there are some
 yet-more-specific constraints that would not give rise to a conflict. For
 example, suppose I was trying to solve `(Foo (Int,Int) ?? Int Int)`. Then
 both fundeps would compatibly force `??` to be `(Int,Int)`.  Mind you,
 then the overlap checker would say that it couldn't pick which of the two
 instances to use.

 So my instinct is that this check for "yet-more-specific" constraints is
 wrong.  If the things on the LHS of the fundep arrow unify, then the
 things on the RHS should be equal. That would reject these two instance
 declarations. Iavor?

 For completeness, the offending bit of code is this, in `FunDeps.lhs` line
 318
 {{{
         Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
                         -- Don't include any equations that already hold.
                         -- Reason: then we know if any actual improvement
 has happened,
                         --         in which case we need to iterate the
 solver
                         -- In making this check we must taking account of
 the fact that any
                         -- qtvs that aren't already instantiated can be
 instantiated to anything
                         -- at all
 }}}

 == Problem 2: why does type checking succeed? ==

 The second mystery is this: why is the constraint `(Foo (Int,Int) alpha
 Int String)`, which is what arises from `main`, solved without error?
 `alpha` is a unification variable. What happens is this.
  * The constraint gives rise to two derived constraints, one from each
 fundep `[D] alpha ~ (Int,String)` and `[D] alpha ~ (String,Int)`.
  * The first is solved by `alpha := (Int,String)`.
  * Having made that choice, the constraint `Foo (Int,Int) (Int,String) Int
 String` uniquely matches the second instance declaration, and so can be
 solved.
  * The second derived constraint becomes `[D] (Int,String) ~ (String,Int)`
 and therefore leads to two isoluble derived constraints `[D] Int ~ String`
 and `[D] String ~ Int`.
  * But if we manage to solve everything else, we discard insoluble derived
 constraints; see `Note [Dropping derived constraints]` in `TcRnTypes`.

 As a result of all this, we (totally bogusly) pick one instance
 declaration, ignoring the fact that the other matches too. Ugh!

 I'm not quite sure what to do, but let's sort out (1) before thinking
 about (2).  Iavor?

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