
#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 simonpj): Martin, thanks. Yes, as comment:14 specifies (fairly precisely I 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:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler