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

 ''Should these two instance declarations be accepted?''

 Depends what you mean by "accepted". I think the case is suffering from
 GHC's delayed/lazy instance enforcement, as affects the complications of
 confluence around partially overlapping instances.

 The `C Char ...` instance clearly could never work -- its constraint needs
 an infinite regress on `C Char [[[[ ... ]]]] ...`. Is anybody saying that
 instance on its own should be rejected? If so, see counter-example/highly
 valuable exploit below.

 It's an interesting experiment trying to find valid calls for `f` [I'm
 using 7.10]. This works: `f (Just "quoi?")`. This doesn't: `f ("quoi")` --
 GHC complains `"Couldn't match expected type 'Maybe y0' with actual type
 '[Char]'"`.

 So GHC __is__  applying the fundep `a -> b` Consistency Condition as per
 '''Definition 6''' in the CHRs/Mark Jones 2000 paper. It is taking `[x]
 [Maybe y]` to infer that in `[x] [x]` we must have `x ~ Maybe y` -- as the
 O.P. is saying.

 I think we've no reason to reject this example. Or perhaps Iavor could
 explain what "loophole" this opens up? Can it result in type incoherence?

 Before we reject this example as bogus, @Richard, I think there are
 examples similar to it that might get caught in the crossfire. [That's the
 reason I arrived here, because I'm trying to understand how/why the
 FunDeps work for it.] The classic Type-level type equality test:

 {{{
 class TTypeEq (a :: *) (a' :: *) (b :: Bool) | a a' -> b
 instance TTypeEq a a True
 instance (b ~ False) => TTypeEq a a' b
 }}}

 Seems to break '''Definition 6'''. There's a substitution for the two
 instances that makes the determinants of the FunDep equal, namely `{a' ~
 a}`. And under that substitution, the dependents are not equal `{b vs
 False}`. FWIW, Hugs applies a stricter interpretation of '''Definition
 6''', with the consequence no such declaration of `TTypeEq` is accepted
 [explored in Oleg/Ralph's HList paper].

 Or if we include substitution `{b ~ True}`, that substitution invalidates
 the constraint on the `False` instance. Clearly GHC isn't evaluating the
 instance's constraints for consistency with its improvement of the class
 parameters.

 We can't write that second instance as:
 {{{
 instance TTypeEq a a' False
 }}}
 GHC complains `"Functional Dependencies conflict between instance
 declarations"`

 What would any proposed fix for this ticket do to a class like?
 {{{
 class TTypeEq2 x a a' b | a a' -> b
 instance TTypeEq2 Bool a a True
 instance TTypeEq2 Char a a True
 instance (b ~ False) Bool a a' b
 instance (b ~ False) Char a a' b
 }}}

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