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

 There's two reasons (at least) by which the OP program should be rejected
 (going by the FDs through CHRs paper):

 1. GHC's Fundep consistency check is bogus, as comment:15 explains.
 2. The FD is non-full. Paper section 6.1/Definition 13/Theorem 2 (Liberal-
 FD confluence).

 For non-full FDs, section 6.2 says to 'project' the FD on to a superclass
 constraint, and 'project' the class's instances:

 {{{
 class (C_FD a b) => C x a b where               -- no FD here, it's in the
 constraint
   op :: x -> a -> b

 class C_FD a b | a -> b

 instance C_FD [x] [x]
 instance C Char x y => C_FD [x] [Maybe y]       -- luckily we can take the
 context from C's instance
 }}}

 Now we can see those instances for `C_FD` overlap (another no-no for the
 paper). Furthermore there's no substitution ordering.

 The paper (Fig. 2) says to derive CHRs from all instances and solve to a
 consistent and confluent set of rules.

 So (after we've held our noses and looked the other way as we breach the
 rules) type improvement ends up unifying the `C_FD` instances.

 In particular, Fig. 2 applies from the class decl and instance decls
 alone. It doesn't wait to see whether/where instances apply.

 What I can't explain is why the same doesn't apply for the TTypeEq example
 comment:9. (The Fig. 2 process incorporates any constraints from
 instances.) For this ticket it must be that it's breaking 2 rules.

 I agree with the comment:15 sentiment that "This has been wrong for a long
 time."/by implication 'fixing' it to reject such programs will break
 stuff. Then I suggest two warnings:

 * `-Wfundep-consistency-bogus` where after applying the unifying
 substitution between instances, the types are **not equal** but merely
 unifiable.
   (Reported against an instance, as per the current consistency check --
 if **contradictory**, reject the instances, as currently.)

 * `-Wfundep-nonfull-noncovered` where a FunDep is non-full and there is no
 class constraint covering just the tyvars for the FunDep.
   (Reported against the class decl. Hmm hmm needs checking whether the
 constraining class has a FunDep of the right cover.)

 Note BTW the paper (section 6.3) has some fancy footwork for 'multi-range
 FDs':

 {{{
 class D1 x a b | a -> b x  where ...             -- counts as full, and
 equivalent to

 class D2 x a b | a -> b, a -> x  where ...       -- this

 class D3 x a b | a -> b, b -> x  where ...       -- and/or this
 }}}

 "There are in fact also cases where we can transform single-range FDs into
 equivalent multi-range FDs. This has the advantage that non-full single-
 range FDs become full multi-range FDs and then we can apply the results
 from Section 6.1."

 Definition 5 (Basic Conditions) apply at all times:

 * "The instance declarations must not overlap."

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