#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): OK, Martin, that's a good example (in comment:26). Let's see a bit more detail. We start with {{{ F [a] [b], F [a] c }}} Now there are two sorts of "improvement" rules which might fire: A. '''Between two constraints'''. Since we have `F [a] [b]` and `F [a] c`, we may derive `[b] ~ c`. After all the class fundep for `F` claims that `a -> b`. B. '''Between a constraint and an instance declaration'''. Here we have * `instance forall p q. F q p => F [p] [q]` (I have alpha-renamed.) * `F [a] c` Since the `[a]` matches the `[p]` we may conclude that `c ~ [q']`, where `q'` is a fresh unification variable, reflecting the fact that the instance declaration says the second parameter must be a list but doesn't tell you what the element type is. So Martin's point is that there are two possible solution paths: {{{ F [a] [b], F [a] c ===> Use (A) to combine the two F [a] [b], F [a] c, c ~ [b] ===> Use the instance declaration to simplify F b a, c ~ [b] }}} Here is the other path: {{{ F [a] [b], F [a] c ===> use the instance declaration F b a, F [a] c ===> use (B) to combine the second constraint with the instance F b a, F [a] c, c ~ [q'] ===> use the instance declaration again F b a, F q' a, c ~ [q'] (stuck) }}} This is helpful: it's a concrete example that demonstrates how minor variations in the way the inference engine works may lead to unpredictable failures in type inference. One possible reaction is that if you are going to lift the Coverage Condition, then (A) yields too many equalities, and you shouldn't use it. But (B) is still useful, and is actually what is wanted here. So maybe we want {{{ class C a b | a ~> b }}} notice `a ~> b` rather than `a -> b`, meaning "`a` specifies the ''shape'' of `b`", which would make use improvement rule (B) but not (A) for this fundep. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler