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

[GHC]

#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
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 diatchki):

 I mean that the example I gave should be rejected, but the program is
 accepted.

 The check for FD consistency is done when multiple instances come
 together, not when you use them.  This is necessary, because it ensures
 that the FD invariant on the class holds, and then we can use the
 invariant in whatever context we want.  For the same reason, you can't
 have instances be consistent only in some cases.

 Currently GHC is very conservative in its use of FDs---it uses them only
 for type inference.  This is why having inconsistent instances like the
 example I showed is not the end of the world: it may result in odd
 behavior where GHC sometimes infers the one type and sometimes the other,
 but the final result is still a sound Haskell program.

 For example, if GHC encountered a constraint `Foo (Int,Int) Int a`, where
 `a` is a unification variable, it might instantiate `a` as either
 `((),Int)` or `(Int,())` depending on in what order it happened to consult
 the instances.  This is essentially the problem that was reported in the
 ticket.

 However, if GHC was to start using the FDs fully as they were intended,
 having inconsistent instances would lead to unsound type-checking. For
 example, in this case, GHC should be able to prove that `((),Int) ~
 (Int,())`, which is obviously bogus.

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