#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 | -------------------------------------+------------------------------------- Comment (by simonpj): Provoked by this ticket, and other recent ones (#9227, #9103) I’ve taken another look. Here are my preliminary conclusions. * #1241 has the best overall discussion, and the paper “[http://research.microsoft.com/en-us/um/people/simonpj/papers/fd-chr/ Understanding functional dependencies using constraint handling rules]” * The [http://www.haskell.org/ghc/docs/latest/html/users_guide/type- class-extensions.html#instance-rules user manual section] that claims “Both the Paterson Conditions and the Coverage Condition are lifted if you give the `-XUndecidableInstances` flag” is plain wrong. * What actually happens is that `-XUndecideableInstances` weakens the Coverage Condition to the Liberal Coverage condition. See `Note [Coverage conditions]` in `FunDeps.lhs`. (Actually, looking at the paper, what is called “Liberal Coverage Condition” here and in the code is the “Refined Weak Coverage Condition” in the paper, Definition 15. * Even this looks bogus. Looking at #1241 comment 15, we see that to get good behaviour (termination, confluence) we need “full fundeps” and “S(tvsright) are all type variables”, neither of which are checked by GHC. * I disagree with Richard's comment above (comment 11). There is no way that fundeps can cause a program to pass the type checker but fail Core Lint. All that fundeps do is cause extra “derived” type equalities to be added to the constraint solver’s pile. That can cause type errors, and perhaps confusing ones, but it cannot cause unsoundness. * The worst that can happen is 1. Non-termination of the type inference engine. This can definitely happen, but is acceptable; c.f. `-XUndecideableInstances`. 2. Non-confluence of type inference. The paper goes on about this at length. I think it amounts to incompleteness. Maybe type inference will succeed one day, but fail the next because of some random variation in the order in which the constraint solver tackles its constraints. I do not have an example that shows this behaviour, but it would be a Bad Thing. I see no good reason to stop programmers getting perhaps-strange behaviour if they ask for it. So I would be OK with doing this (which is exactly what https://phabricator.haskell.org/D69 proposes this behaviour for the Coverage Condition (see [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-rules user manual]) * No flags: Coverage Condition enforced * `-XUndecidableInstances`: changes Coverage Condition to Liberal Coverage Condition. This risks non-termination. I’m still uneasy about the consequences of not checking for “full” fundeps (see comment 15 of #1241) but it’s what happens right now. * `-XDysFunctionalDependencies`: removes the Coverage Condition altogether, with somewhat unknown consequences. So this is a long-winded way of saying I’m ok with the D69 proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler