Martin, thanks. Yes, as comment:14 specifies (fairly precisely I
#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature | Status: new request | Milestone: 7.10.1 Priority: high | Version: 7.7 Component: Compiler | Keywords: Resolution: | Operating System: Unknown/Multiple Differential Revisions: Phab:D69 | Type of failure: None/Unknown Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: #1241, | #2247, #8356, #9103, #9227 | -------------------------------------+------------------------------------- Comment (by diatchki): comment:14 specifies what GHC is NOT going to do, but it does not specify what it will do! As a programmer, when I see a class-declaration: {{{ class C a b | a -> b }}} I think: ''Aha, there is a functional relation between the parameters of this class. This means that whenever the first parameters of instances are the same, so will be the second ones''. I don't know what this declaration means in the context of `Dysfunctional Dependencies`. I am also unclear about why `DysfunctionalDependencies` removes some of the consistency checks but not ``all``? I believe that due to the current GHC implementation, "nothing will go wrong" even if we allowed instances such as `C Int Char` and `C Int Bool`, or am I missing something? All of this will change, however, if we were to complete the implementation of FDs and added support for using the FDs on given constraints: then type-safety actually depends on the consistency of the instances, and we better not have any `Dysfunctoinal Dependencies` around. Replying to [comment:25 simonpj]: thought), `DysFunctionalDependencies` means relaxing the coverage condition altogether.
Let me stress once more that, apparently contrary to your second bullet,
dropping coverage does not threaten type soundness. I'm not quite sure what you mean by "type safety". I did actually go back to our JFP paper "Understanding functional dependencies using constraint handling rules" to see if I could find a concrete example of the problems that might arise, but all I could find I was the unsupported claim that "all is lost" if we don't have confluence.
I ''believe'' (but I have no example that demonstrates) that dropping
the Coverage Condition might mean that a small change in the program makes a large difference in whether the type inference algorithm succeeds. But it would be good to have some concrete cases. One way to gather some might be to allow it, and see whether our users start complaining about unpredicatable inference.
Simon
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler