#1241: Functional dependency Coverage Condition is lifted, and should not be
----------------------------------------+-----------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 6.8 branch
Component: Compiler (Type checker) | Version: 6.6
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
----------------------------------------+-----------------------------------
Comment (by simonpj):
Here's an exchange I had with Martin Sulzmann a month or two back, but
have not acted on. It refines my informal proposal above.
The current situation is this. An instance decl must satisfy:
1. The Paterson Conditions: for each assertion in the context
* No type variable has more occurrences in the assertion than in the
head
* The assertion has fewer constructors and variables (taken together
and counting repetitions) than the head
1. The Coverage Condition. For each functional dependency, tvsleft ->
tvsright, of the class, every type variable in S(tvsright) must appear in
S(tvsleft), where S is the substitution mapping each type variable in the
class declaration to the corresponding type in the instance declaration.
See [http://www.haskell.org/ghc/dist/current/docs/users_guide/other-type-
extensions.html#instance-rules the GHC user manual instance rules]
I propose to replace (2) with (2') namely:
* EITHER The Coverage Condition (as written above)
* OR
A. The Refined Weak Coverage Condition. For each functional
dependency, tvsleft -> tvsright, of the class, every type variable in
S(tvsright) must be “reachable” from S(tvsleft), where S is <...text as
before...>. By “reachable” we mean “can be reached in a finite number of
hops using the functional dependencies of the context of the instance
decl” [I’ll formalise this more]
B. AND the function dependencies of this class are full
C. AND S(tvsright) are all type variables.
Furthermore, if the programmer specifies `–fallow-undecidable-instances`
(i.e takes responsibility for termination) then we lift
* the Paterson conditions
* condition (C) above
Throughout, I’m taking for granted the non-overlap of instance decls.
Now my questions are these:
* Is the above correct? That is guarantee confluence, termination.
'''Martin''': YES
* The either-or above is a bit unsatisfactory, because (A) relaxes one
condition, but (B),(C) add new conditions. Can you see any way to avoid
that? I’m guessing not. '''Martin''': We definitely need some new
conditions. (A) + (B) are sufficient and necessary conditions to guarantee
confluence, assuming we have termination, (C) is sufficient to guarantee
termination. So, the answers is we cannot avaoid (A) + (B) but there
might be further conditions (C') which guarantee termination.
* Condition (C) is in our paper (Defn 14, page 30). But if the Paterson
conditions hold, is (C) necessary in addition? '''Martin''': Yes! The
Paterson conditions guarantee that the instances terminate. The subtle
problem created by FDs is that type inference may not terminate (even if
the instances terminate). We know that the coverage condition is also
crucial for termination, but the refined weak coverage condition is only
good enough to ensure confluence. Hence, we need the additional condition
(C).
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1241#comment:15>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
