[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:9 diatchki]:
 > I mean that the example I gave should be rejected, but the program is
 accepted.
 >

 Sorry, Iavor, I'm not following. GHC as at 8.0.1 seems to be behaving as
 documented here
 http://downloads.haskell.org/~ghc/8.0.2/docs/html/users_guide/glasgow_exts.html
 #instance-resolution

  * It is fine for there to be a ''potential'' of overlap (...); an error
 is only reported if a particular constraint matches more than one
 [instance].
 .

 >
 > The check for FD consistency is done when multiple instances come
 together, not when you use them.

 Are you saying this is what you'd like to see happening? What GHC is
 actually doing is checking FD consistency when it sees the instance decls,
 and only rejecting if the instances are outright contradictory. If there's
 only a ''potential'' inconsistency (due to overlap), GHC only rejects at
 the use site if it can't resolve to a particular instance.

 .
 >
 > 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.
 >

 Again, I think you're saying you'd like to be able to "use the
 invariant"/rely on them being consistent(?)

 .
 >
 > Currently GHC is very conservative in its use of FDs---it uses them only
 for type inference.

 Yes GHC is conservative. Whereas in the FDs-via-CHRs paper, it is expected
 that under an FD `C a b | a -> b` if we have `C a b` and `C a b'` we can
 conclude `b = b'` (that's type equality, not just unifiability); GHC does
 not arrive at any such conclusion.

 .
 >
 > 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.
 >

 Yes that is the problem reported on the ticket. AFAICT is was still a
 problem at 7.10. I see no evidence it is still happening at 8.0. (I've
 tried the same code at both versions.) I agree with @Reid it's rather
 discomforting this change of behaviour can't be nailed down to a specific
 mod.

 What you can still do in 8.0 is put a type signature, to get inconsistent
 behaviour:

 {{{
 f4 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: ((), Int)     -- results in
 ((), 7)
 f5 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: (Int, ())     -- results in
 (5, ())
 }}}

 .
 > 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.

 Hmm. "as they were intended" is rather debatable. For each of the examples
 you're bringing forward, you're using several extensions of Haskell beyond
 Haskell 2010: `UndecidableInstances` or non-full dependencies (in a way
 that breaks the FDs-via-CHRs rules) or overlap -- either
 `OverlappingInstances` or overlap of the types in a non-full dependency.
 In this case we're now discussing you need `FlexibleInstances`, again not
 envisaged in the paper.

 I think each of those extensions is justifiable. Furthermore for GHC to be
 using FD inference as per the FDs-via-CHRs rules would block separate
 compilation. (The CHRs assume you can see all instance decls.) So I think
 it's prudent GHC does not try to go that far, and therefore avoids the
 risk of unsound type-checking.

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