#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