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

 Replying to [comment:11 diatchki]:
 > The check for overlapping is done when GHC resolves instances. This is
 unrelated to this example. You can easily modify it, so that there are no
 overlapping instances:
 >
 > {{{
 > class Foo tag a b c | a b -> c
 >
 > instance Foo Int (x, a) x ((), a)
 > instance Foo Bool (x, a) a (x, ())
 > }}}

 No, that class decl is not allowed, according to the FDs-via-CHRs paper,
 Section 6.2 on Non-full dependencies. (And this example is similar to
 yours on #10675 -- which I think is also disallowed.) If the FD is non-
 full, the class must have a super-class constraint to enforce the FD.
 Otherwise we still get inconsistent behaviour, which is your complaint on
 #10675.

 .
 >
 > The check for the consistency of FDs ought to be done whenever instances
 exist in the same scope, ...

 You mean like dear old Hugs? Yes I miss it for that reason. But I think
 you can still get inconsistent behaviour with overlapping instances, if
 some instances are in scope in one module but different instances in scope
 in a different module.

 I think what it needs is to ban overlap altogether. (And that means for
 non-full FDs, banning overlap of the params involved with that FD. We have
 to be canny there: allow identical params, modulo alpha renaming.) Then we
 just reject any instance that attempts to overlap. (Again Hugs in effect
 did that with its check "Instance is inconsistent with FunDeps".)

 But what we can do currently with overlapping instances is useful. We need
 a more expressive way to say in the instance: yes I know this looks like
 it overlaps, but actually I don't want it to; when the use site appears to
 be ambiguous, always pick that instance. For example with instance guards:

 {{{
 class Foo a b c | a b -> c

 instance Foo (x, a) x ((), a)   | x /~ a
 instance Foo (x, a) a (x, ())
 }}}

 The guard on that first instance says: `x` must not be unifiable with `a`,
 so do not select this instance if unifiable. That's the same as Richard's
 apartness check for Closed Type Families selecting equations. More
 discussion here https://typesandkinds.wordpress.com/2013/04/29/coincident-
 overlap-in-type-families/

 .
 >
 > As far as I can tell, the new behavior in 8 is how GHC uses FDs to
 perform improvements.  Instead of just using one of the instances, it will
 now try to improve with all of the instances.  As a result, if there are
 inconsistencies, it will try to improve in two different ways, and report
 a delayed error.

 "New"? You're describing the behaviour Simon raises in #10675, which was
 at 7.10. And judging by "Examples in the testsuite that exploit this
 loophole ", it's been around for some time. I agree with you that GHC
 should not try to merge or mingle/mangle type improvements from different
 instances. The behaviour in #10675 is just nuts. (But trying to cure it
 might be worse than the disease. It does seem to be a swamp.)

 .
 >
 > The underlying bug of failing to detect the inconsistency of the
 instances is still present.
 >
 > The thing that we should be checking is:
 > {{{
 > forall x1 a2 x2 a2. ( (x1,a1) ~ (x2,a2), x1 ~ a2 ) => ( ((), a1) ~ (x2,
 ()) )
 > }}}

 Yes, which we can do with a superclass constraint, such as a type function
 with equality constraint.

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