[GHC] #10675: GHC does not check the functional dependency consistency condition correctly

[GHC]

#10675: GHC does not check the functional dependency consistency condition
correctly
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.1
      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 [ticket:10675 simonpj]:
 > Should these two instance declarations be accepted?

 * I'm going to '''argue they should'''
 * In addition to the bogusness documented on this ticket, there's a
 '''design weakness''' in the FunDep consistency check.
 * Exploiting that with malice aforethought, there's some '''disturbing
 behaviour'''

 '''Argument to accept:''' Yes GHC's consistency check is bogus/contrary to
 all the literature. But it's been in place since at least 2004. Lot's of
 code relies on it. So we can provide no grounds to reject the instances,
 unless we can look also at other class params not involved in the FunDep.
 But then according to the Type Families work, a FunDep should be
 equivalent to a superclass equi constraint with a Type Family call. I.e.
 {{{
 class C x a b | a -> b where             -- O.P.
 class (F a ~ b) => C x a b where         -- Type Family F
 }}}
 The Type Family can look only at the class's second parameter. The (weird)
 unification behaviour described in the O.P. is in effect trying to reverse
 engineer `F`'s equations from the class instances. So ghc must unify. OTOH
 there's no definition for `F` you could write that would be consistent
 with where ghc ends up in the type for function `f`.

 '''Design weakness:''' in ghc checking instances for FunDep consistency is
 that it only checks (and unifies) pairwise. It doesn't check all instances
 globally. Then arguably '''Definition 6 (Consistency Condition)''' in the
 ''FunDeps via CHRs'' paper is too weak. (Note that the definition of
 Functional Dependency in database theory quantifies across all rows in a
 table.)

 '''Disturbing behaviour:''' consider this exploit

 {{{
 {-# LANGUAGE as per O.P. #-}

 class C x a b | a -> b where          -- as O.P.
    op :: x -> a -> b
 instance C Bool [x] (x, Bool)
 instance C Char x y => C Char [x] (Int, y)
 instance C Char x y => C Char [x] (y, y)

 f x = op True [x]                     -- as O.P.
 }}}

 Quick: what type inferred for `f`? What odds would you lay it's `f :: Int
 -> (Int, Int)`?

 Luckily we can't actually call `f`: `Couldn't match type 'Bool' with
 'Int'`. So the `True` parameter to `op` in `f`'s rhs is trying to pick the
 'right' instance for `C`.

 More disturbingly, if you switch round the order of instances, you'll get
 a different inferred type for `f`: it's the unifier of whichever are the
 last two instances. (Full disclosure: this is at ghc 8.0.1. Sensitivity to
 ordering of instances sounds like #9210, but that seems to have gone away
 at 8.0.)

 The fix in all these examples is to make the FunDep full (which it really
 should be)
 {{{
 class C x a b | x a -> b where
 }}}

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