#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 sulzmann): Some brief comments regarding the various conditions/flags. * Paterson Conditions and the Coverage Condition (plus the FD Consistency Condition) The above guarantee sound and decidable type inference. In CHR speak, termination and confluence. Confluence effectively means that we find unique answers. Hence, confluence implies consistency. Hence, we also obtain type safety. * Dropping the Coverage Condition There are numerous examples which violate this condition. Naively dropping this condition potentially threatens decidable type inference (due to non-termination) and type safety (due to non-confluence). * Weak (aka refined) Coverage Condition Guarantees local confluence (critical pairs are joinable). Assuming that instances are terminating we obtain confluence (by Newman's Lemma). The bad news is that typical examples which violate the coverage but satisfy the weak coverage condition are non-terminating. Consider the classic example class F a b | a -> b instance F a b => F [a] [b] where for constraint F [a] a the type inferencer will not terminate The good news is that in "On Termination, Confluence and Consistent CHR-based Type Inference", ICLP'14, we show that (under some modest extra conditions) for terminating type inference goals we find unique answers. In essence, we're happy to achieve local confluence under the assumption that we have local termination. * XUndecidableInstances Enforces the weak coverage condition but gives up on (global) termination. Assuming that the GHC type inference terminates nothing bad will happen though (cause we find unique answers, see above) * DysfunctionalDependencies I can only guess what this means as I couldn't find any concrete definition. My impression is to drop the weak coverage condition? Bad idea! We no longer have local confluence. We might be lucky enough that GHC always applies type inference rules (FD improvement, instances) in a fixed order and thus 'unique' answers are guarantees. Sounds rather brittle to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler