#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): Correct. I'm too pessimistic in my comment. For type safety (well-typed programs cannot go wrong) it suffices to have consistency. Simon, surely the Consistency Condition must hold at least, right? I agree then that the Coverage Condition (or variants) can be dropped. See Theorem 1 in the above mentioned paper. I still find it strange that you want to drop the Coverage Condition (or variants of it). This clearly leads to non-confluence, hence, unpredictable type inference. Consider class F a b | a -> b where f :: a -> b -> a instance F b a => F [a] [b] -- Order of 'a' and 'b' swapped! -- Hence, (weak) coverage is violated. g as bs c = (f as bs, f as c) The above gives (roughly) rise to the constraints F [a] [b], F[a] c Depending on the order type inference rules are applied, the following two final constraints may arise (1) c = [b], F b a (2) c = [b'], F b a, F b' a Say we use (1) for some type annotation but the type checker only comes up with (2). Urgh! To conclude: - For type safety we require at least consistency - For predictable type inference we require (local) termination and (weak) coverage. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler