Functional dependency Coverage Condition is lifted, and should not be

[guest]

Hello, GHC 6.6 (with flags -fglasgow-exts -fallow-undecidable-instances) is too liberal when accepting instances. Here is an example:

class F a b | a -> b where f :: (a,b)
instance F Int b

The instance violates the functional dependency constraint of F because (in theory) it can be used to solve both F Int Bool and F Int Char. In practice, it seems that some free variable gets bound upon the first use of f with a concrete type, leading to some rather confusing behavior. Example:

x :: (Int,a)
x = f
 
y :: (Int,Bool)
y = f
 
z :: (Int,Char)
z = x -- works, but 'z = f' does not

-Iavor

[simonpj]

This is interesting. Section 5.2 of  Understanding functional dependencies via Constraint Handling Rules explains why it is desirable to lift the Coverage Condition, which is what -fallow-undecidable-instances is doing here.

The strange behaviour you get is because the occurrece of f in y gives rise to a top-level constraint (F Int Bool). Then with the definition z = f we get a second top-level constraint (F Int Char), and thence the error message

Foo12.hs:1:0:
    Couldn't match expected type `Bool' against inferred type `Char'
    When using functional dependencies to combine
      F Int Char, arising from a use of `f' at Foo12.hs:15:4
      F Int Bool, arising from a use of `f' at Foo12.hs:12:4

However, with the definition z = x no constraint is genreated (since x does not have an overloaded type) and all is well.

This is an unexected (to me) consequence of lifting the Coverage Condition. Yet I do not want to re-impose it because (as 5.2 explains) it's sometimes useful to have it lifted.

I'm not sure what the Right Answer here is. It looks like another fundep brain-bender. I'm inclined to continue working on type inference for associated types!

[guest]

The problem is that the class instance F Int b vialotes the functional dependecy on F and, for this reason, it should be rejected. This is similar to rejecting an instance F Char Bool when we already have an instance for F Char Char except that, in this case, the instance is conflicting with itself.

Relaxing the coverage condition is OK but we still need to check that instances satisfy the functional dependecies of the class (just like we need to check that instances satisfy the super classes for a class). I thought that GHC was supposed to use the "dependecy" rule (according to  http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies) and I think that in 6.4 this used to work but, I guess, in 6.6 this check was removed?

-Iavor

[sulzmann]

I agree with Iavor. The above FD program simply makes no sense. You can check "Understanding Functional Dependencies via Constraint Handling Rules" Section 6.1. for the details of the "dependency" rule mentioned by Iavor.

BTW, associated types would show the same strange behavior as the above FD program, if we could define

type F :: * -> * type instance F Int = b

-Martin

[simonpj]

Thanks Martin. I'd like your advice. Here is GHC's spec for instance declarations

http://www.haskell.org/ghc/dist/current/docs/users_guide/other-type-extensions.html#instance-decls

Notice (1) the Paterson Conditions (PCs), (2) the Coverage Condition (CC)

We agree that these conditions are conservative. At the moment they are both lifted by adding -fallow-undecidable-instances. But I gather you think that maybe the CC should *not* be lifted, is that right.

So are you saying this?

• The CC should always hold
• The PCs can be lifted; the only problem is that you may get non-termination

The trouble is, as you know, that sometimes the CC can validly not hold. Example:

class C a b | a->b
class D a b | a->b
instance D a b => C [a] [b]

Here the CC does not hold, but the context (D a b) enforces the dependency. We call this the Weak Coverage condition in the paper.

So you could be saying: you can only lift the CC if you replace it with a weaker, but still sufficiently strong alternative.

I'm also not sure whether lifting it altogether (as GHC now does) is simply confusing, or whether it can be unsound or something really bad like that.

Simon

[claus]

> GHC 6.6 (with flags {{{-fglasgow-exts -fallow-undecidable-instances}}}) is
> too liberal when accepting instances.  Here is an example:
> {{{
> class F a b | a -> b where f :: (a,b)
> instance F Int b
> }}}
> The instance violates the functional dependency constraint of {{{F}}}
> because (in theory) it can be used to solve both {{{F Int Bool}}} and {{{F
> Int Char}}}.  

doesn't that depend on the interpretation of the instance? since we can formalise any consistent interpretation, we need to think about the intended interpretation before we dive into formalisations. i can think of three interpretations, in two of which the instance is valid because it is interpreted _as constrained by the FD_. the third interpretation, which Hugs seems to apply, is to interpret the instance _independent of the FD_, then use the FD to check whether the instance conforms to it.

i've always had problems with that third interpretation, because it pretends that FDs are just a _check_ on which constraints are valid. whereas the major purpose of FDs has always been to reduce the set of FD-valid instantiations to a singleton if possible, and then _to go beyond mere checking_ by _instantiating type variables_ to the only possibly valid option.

now, since everybody seems to agree that it is fine to use FDs for type variable instantiation in some contexts, i don't understand why we don't do the same in all contexts, if only for consistency.

back to my three interpretations of "instance F Int b":

1 the instance says b is polymorphic. the FD says b is uniquely determined. so b is uniquely determined to be fully polymorphic. similar to GHC's rigid type variables, it cannot be instantiated to anything but a fully polymorphic type forall a. a.

2 the instance is polymorphic in b. the FD says b is uniquely determined. so any constraints involving this instance have to involve mutually consistent instantiations of b, b_i, and the ultimate interpretation of the instance is instance F Int mgu(b_i). only if no mgu exists is there a conflict to report.

3 the instance is polymorphic in b, so could be instantiated to any specific type. the FD says b is uniquely determined, so it cannot have differing instantiations. so the instance is in conflict with the FD.

GHC seems to tend towards 2, Hugs towards 3. i've listed 1 for completeness (although there might be other interpretations?). it would be difficult to argue in favour of 1, as it would amount to implicit existential quantification, when the general preference is towards explicit quantification. as i mentioned, i can't think of 3 as a consequent interpretation - the point of using a constraint logic is to find things that fulfill all given constraints, not to complain about things that do not.

> class F a b | a -> b where f :: (a,b)
> instance F Int b

this would be a valid instance in 2 - there is a unique b such that F Int b, but we do not yet know what that is.

> x :: (Int,a)
> x = f

this is the devious part of the example. there is no doubt about the interpretation of the first line - if the definition type-checks, x may be used polymorphically. at first look, it might look as if that could be squared with interpretation 2 of f: the instance definition sets a bound on b on one side, x's type sets a bound on b on the other side, so b ends up fixed as a rigid type variable.

but this means trouble: first, it would once again smuggle in implicit existentials, which we don't want. second, the FD says that b is uniquely determined, and this right-hand side type-checks only if b is fully polymorphic, to match x's rigid type, but in order to switch from the rhs to the lhs, x's type goes from rigid to fully polymorphic itself, but since the FD fixes f's type, f has really become rigid, not polymorphic. (it hurts to think about this, and i'm not sure i got it right;-)

> y :: (Int,Bool)
> y = f

valid in 2, as long as there are no conflicting instantiations of f. incompatible with either of x or z.

> z :: (Int,Char)
> z = x -- works, but 'z = f' does not

i don't think z=x should work, for the reasons given above. z=f would work on its own in 2, but is incompatible with either x or y.

to sum up, while the program as a whole makes no sense, i think there is a consistent interpretation, close to GHC's current one, in which the instance itself is valid, as well as use of f at one specific type. but i don't think GHC gets this quite right: after type-checking the rhs of x, f's type gets rigid, so type-checking the whole definition/declaration of x ought to fail. (i think:-)

note that i haven't even referred to the coverage condition here.

> However, with the definition `z = x` no constraint is genreated (since `x`
> does not have an overloaded type) and all is well.

at this point, it is already too late. x=f should have generated a constraint, one that is in fact incompatible with the type declaration for x.

> I'm not sure what the Right Answer here is.  It looks like another fundep
> brain-bender.  I'm inclined to continue working on type inference for
> associated types!

while i can understand the sentiment, i doubt that this is a real choice. starting from type classes (reduction of type predicates):

- associated types add a kind of semantic unification (equating types by instantiating variables, intermingled with reduction of type functions)

- functional dependencies add syntactic unification, but we still end up with a kind of narrowing (reduction of type predicates intermingled with equating types by instantiating variables)

whichever way you start out, you end up with both unification and reduction, so the problems should be very similar in both forms, i'd suspect.

[claus]

actually, while FDs are used to instantiate type variables, that never seems to happen for explicit type declarations. and the type parameters of an instance head become part of the explicit type declarations for the class methods.

also, even after we filter out the instantiations of the instance that do not conform to the FD, we still don't know precisely what b is, and yet it isn't universally quantified either.

so, while interpretation 2 might be self-consistent, and possibly useful, and apparently closest to what GHC is doing, it differs from the standard interpretation of the constructs it would apply to, and should probably get its own syntactic clues to indicate that difference.

> class F a b | a -> b where f :: (a,b)
> instance F Int b

as i can no longer offer an interpretation in which this instance would be valid (at least not without some extra syntax to indicate the special role of b in interpretation 2), i agree that it is not. and unless GHC's interpretation is based on something other than interpretation 2, its behaviour ought to change. it might be helpful to report the problem not just as "instance conflicts with FD", as Hugs does, but as "instance is more general than FD permits".

[simonpj]

See also this Haskell Cafe thread  A question about functional dependencies and existential quantification

The issue is identical: GHC with -fallow-undecidable-instances is lifting the Coverage Condition, and probably should not do so.

Question: if we did not lift the Coverage Condition, would anyone mind? Or perhaps lifting it deserves its own flag. Or we could combine it with the already-scary flag -fallow-incoherent-instances, which also has the same loss-of-confluence property. Opinions?

Simon

[Stefan O'Rear <stefanor@…>]

Last I checked, the Coverage Condition is incompatible with MTL, so we *really* shouldn't make the CC mandatory. (I'm not against a general refactor of -fallow-undecidable-instances into smaller, more self-documenting pieces, as long as the functionality is still there)

[simonpj]

Stefan adds: Editing Control.Monad.State.Strict to remove -fallow-undecidable-instances:

stefan@stefans:/tmp$ ghc -fglasgow-exts Control/Monad/State/Strict.hs

Control/Monad/State/Strict.hs:207:0:
    Illegal instance declaration for `MonadError e (StateT s m)'
        (the Coverage Condition fails for one of the functional dependencies;
         Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `MonadError e (StateT s m)'

Control/Monad/State/Strict.hs:213:0:
    Illegal instance declaration for `MonadReader r (StateT s m)'
        (the Coverage Condition fails for one of the functional dependencies;
         Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `MonadReader r (StateT s m)'

Control/Monad/State/Strict.hs:218:0:
    Illegal instance declaration for `MonadWriter w (StateT s m)'
        (the Coverage Condition fails for one of the functional dependencies;
         Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `MonadWriter w (StateT s m)'

Yes, these are the same instances that break h98 compatibility.

[guest]

Hello, would it be too much trouble to use the "dependency" instead of the "coverage" condition when type-checking with -fallow-undecidable-instances? As far as I recall, the main issue with the dependency condition was that it could lead to non-termination in the type-checker but that is to be expected with -fallow-undecidable-instances anyways. -Iavor

[simonpj]

What is the "dependency condition"? (The "coverage condition" is defined here http://www.haskell.org/ghc/dist/current/docs/users_guide/other-type-extensions.html#instance-rules)

Simon

[guest]

Hello, I was referring to the condition that GHC used to implement in version 6.4. There is a brief description at:  http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies (in the section "GHC and Hugs"). There is a more detailed discussion that uses the name "Weak Coverage Condition" in Section 6.1 of "Understanding functional dependencies via Constraint Handling Rules". -Iavor

[simonpj]

Ah, but if you want the Weak Coverage Condition then the functional dependencies must be "full" (see the paper). So we seem agreed that

• -fallow-undecidable-instances should not lift the Coverage Condition.

Beyond that we could also:

• Replace the Coverage Condition by the Weak Coverage Condition (suitably modified to account for "fullness"). I think the modification is: either the Coverage Condition is satisified, or the FDs of this class are full and the Weak Coverage Condition is satisfied.

And perhaps also

• Allow whatever coverage condition we have to be lifted
  • Either by -fallow-incoherent-instances
  • Or by a new flag -fno-coverage-condition

None of this sounds too hard, but I can't say I'm eager to get on with it :-)

[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
2. 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 the GHC user manual instance rules

I propose to replace (2) with (2') namely:

• EITHER The Coverage Condition (as written above)
• OR
  1. 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]
  2. AND the function dependencies of this class are full
  3. 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).

[simonmar]

Discussion is ongoing; no milestone for a fix as yet.

[simonpj]

See also #2247, which gives an example of the confusing things that happen if we don't impose the Coverage Condition.

[iavor.diatchki@…]

commit fe61599ffebb27924c4beef47b6237542644f3f4

Author: Iavor S. Diatchki <iavor.diatchki@gmail.com>
Date:   Sun Jan 13 16:29:10 2013 -0800

    Use a version of the coverage condition even with UndecidableInstances.
    
    This fixes bug #1241 and #2247.  When UndecidableInstances are on,
    we use the "Liberal Coverage Condition", which is what GHC used to do in
    the past.  This is the gist of the check:
    
    class C a b | a -> b
    instance theta => C t1 t2
    
    we check that `fvs t2` is a subset of `fd-closure(theta,fvs t1)`.
    
    This is strictly more general than the coverage condition, while
    it still guarantees consistency with the FDs of the class.  This
    check is completely orthogonal to termination (it by no means guarantees
    it).
    
    I am not sure of the role of the "coverage condition" in termination---
    the comments suggest that it is important.  This is why, for the moment,
    we only use this check when UndecidableInstances are on.

 compiler/typecheck/TcValidity.lhs |    8 ++++-
 compiler/types/FunDeps.lhs        |   65 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 71 insertions(+), 2 deletions(-)