Opened 5 years ago

Last modified 2 years ago

#9210 new bug

"overlapping instances" through FunctionalDependencies

Reported by: rwbarton Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: FunDeps Cc: ekmett@…, dimitris@…, diatchki, dreixel
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This program prints ("1",2), but if you reverse the order of the two instances, it prints (1,"2").

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

-- extracted from http://lpaste.net/105656

import Control.Applicative
import Data.Functor.Identity

modify :: ((a -> Identity b) -> s -> Identity t) -> (a -> b) -> (s -> t)
modify l f s = runIdentity (l (Identity . f) s)

class Foo s t a b | a b s -> t where
  foo :: Applicative f => (a -> f b) -> s -> f t

instance Foo (x, a) (y, a) x y where
  foo f (a,b) = (\fa -> (fa,b)) <$> f a

instance Foo (a, x) (a, y) x y where
  foo f (a,b) = (\fb -> (a,fb)) <$> f b

main = print $ modify foo (show :: Int -> String) (1 :: Int, 2 :: Int)

Note that the two instances involved Foo (Int, Int) (String, Int) Int String and Foo (Int, Int) (Int, String) Int String are not actually overlapping. But, they have the same a, b, and s fields and it seems that this makes GHC think that either one is equally valid, thanks to the fundep.

Change History (12)

comment:1 Changed 5 years ago by ekmett

Cc: ekmett@… added

comment:2 Changed 5 years ago by rwbarton

Version: 7.8.17.8.2

Oh, since I minimized the example now I can test more easily with other GHC versions.

This is a regression from GHC 7.6.3, in that that version rejected main with the following error (that I don't really understand):

some.hs:22:23:
    Couldn't match type `Int' with `String'
    When using functional dependencies to combine
      Foo (a, x) (a, y) x y,
        arising from the dependency `a b s -> t'
        in the instance declaration at some.hs:19:10
      Foo (Int, Int) (String, Int) Int String,
        arising from a use of `foo' at some.hs:22:23-25
    In the first argument of `modify', namely `foo'
    In the second argument of `($)', namely
      `modify foo (show :: Int -> String) (1 :: Int, 2 :: Int)'
Failed, modules loaded: none.

If I remove main then GHC 7.6.3 does accept the instances, though. That seems wrong to me also (though certainly "less wrong").

I have a GHC 7.8.2.20140609 lying around and it displays the same behavior as GHC 7.8.1.

comment:3 Changed 5 years ago by simonpj

Cc: dimitris@… diatchki added

I can at least explain what is going on. I defer to Iavor (the Functional Dependency Expert) on what the right thing to do might be.

Problem 1: Should these instance declarations be accepted at all?

After all, unifying the a,b,s components of the instances shows that the constraint Foo (x,x) ?? x y would match both instances, and hence (via the fundep) force ?? to be both (y,x) and (x,y) respectively.

GHC doesn't currently complain about this, I think because there are some yet-more-specific constraints that would not give rise to a conflict. For example, suppose I was trying to solve (Foo (Int,Int) ?? Int Int). Then both fundeps would compatibly force ?? to be (Int,Int). Mind you, then the overlap checker would say that it couldn't pick which of the two instances to use.

So my instinct is that this check for "yet-more-specific" constraints is wrong. If the things on the LHS of the fundep arrow unify, then the things on the RHS should be equal. That would reject these two instance declarations. Iavor?

For completeness, the offending bit of code is this, in FunDeps.lhs line 318

        Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
                        -- Don't include any equations that already hold.
                        -- Reason: then we know if any actual improvement has happened,
                        --         in which case we need to iterate the solver
                        -- In making this check we must taking account of the fact that any
                        -- qtvs that aren't already instantiated can be instantiated to anything
                        -- at all

Problem 2: why does type checking succeed?

The second mystery is this: why is the constraint (Foo (Int,Int) alpha Int String), which is what arises from main, solved without error? alpha is a unification variable. What happens is this.

  • The constraint gives rise to two derived constraints, one from each fundep [D] alpha ~ (Int,String) and [D] alpha ~ (String,Int).
  • The first is solved by alpha := (Int,String).
  • Having made that choice, the constraint Foo (Int,Int) (Int,String) Int String uniquely matches the second instance declaration, and so can be solved.
  • The second derived constraint becomes [D] (Int,String) ~ (String,Int) and therefore leads to two isoluble derived constraints [D] Int ~ String and [D] String ~ Int.
  • But if we manage to solve everything else, we discard insoluble derived constraints; see Note [Dropping derived constraints] in TcRnTypes.

As a result of all this, we (totally bogusly) pick one instance declaration, ignoring the fact that the other matches too. Ugh!

I'm not quite sure what to do, but let's sort out (1) before thinking about (2). Because if (1) is resolved to reject such instances, (2) becomes moot.

Iavor?

Last edited 5 years ago by simonpj (previous) (diff)

comment:4 Changed 5 years ago by simonpj

Cc: dreixel added

OK, well I tried the effect of solving problem 1 by making the two instance declarations illegal. The changes in FunDeps are simple:

  • Remove altogether the alternative guarded by | isJust (tcUnifyTys bind_fn rtys1' rtys2'), mentioned above
  • Change the definition of fdeqs thus
    -                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
    +                    fdeqs = zipAndComputeFDEqs eqType rtys1' irs2'
    

This resulted in four test-suite failures

Unexpected failures:
   ghci/scripts              ghci047 [bad stderr] (ghci)
   polykinds                 T9106 [stderr mismatch] (normal)
   typecheck/should_compile  FD4 [exit code non-0] (normal)
   typecheck/should_compile  T7875 [exit code non-0] (normal)

All were for the same reason: instance declarations that were previously accepted are now rejected.

I looked a bit more at T7875. It is described by Note [Weird fundeps] in TcInteract, which reads as follows:

Note [Weird fundeps]
~~~~~~~~~~~~~~~~~~~~
Consider   class Het a b | a -> b where
              het :: m (f c) -> a -> m b

           class GHet (a :: * -> *) (b :: * -> *) | a -> b
           instance            GHet (K a) (K [a])
           instance Het a b => GHet (K a) (K b)

The two instances don't actually conflict on their fundeps,
although it's pretty strange.  So they are both accepted. Now
try   [W] GHet (K Int) (K Bool)
This triggers fudeps from both instance decls; but it also
matches a *unique* instance decl, and we should go ahead and
pick that one right now.  Otherwise, if we don't, it ends up
unsolved in the inert set and is reported as an error.

Trac #7875 is a case in point.

This does indeed look weird to me. And it's incredibly fragile. If the wanted constraint doesn't yet match a unique instance decl (perhaps because some other constraint has not yet done a unification) then we won't pick the instance, so we will generate both (conflicting) fundeps, and we will get an error (from the fundep) even though the constraint is ultimately solved. This seems terrible to me. So I think I'd argue that #7875 should be rejected (hence adding Pedro, its author, in cc).

FD4 actually comes from #1797, and involves a combination of functional dependencies and overlapping instances. I'm not sure we've ever fully thought through this conbination, but rejecting this would indeed make people unhappy.

I have not looked at #9106 or ghci047.

I feel strongly disinclined to dive once more into the functional dependency swamp. If someone (Iavor? Pedro?) would like to help that would be great.

Until then, I totally agree that the behaviour of this ticket is bizarre and wrong. But without help I don't know how to fix it.

comment:5 Changed 4 years ago by rwbarton

Somehow, this program no longer compiles in GHC 8.0 or HEAD. Yay!

I'd rather not just close this without knowing why it was fixed, and we should add a regression test.

comment:6 Changed 2 years ago by AntC

Keywords: FunDeps added

comment:7 Changed 2 years ago by diatchki

Here is a simplified version of the example in the ticket:

class Foo a b c | a b -> c

instance Foo (x, a) x ((), a)
instance Foo (x, a) a (x, ())

These two instances are accepted by GHC 8.0.1, but should be rejected as they violate the FD on the class. Here is the counter example:

Foo (Int,Int) Int ((), Int)
Foo (Int,Int) Int (Int, ())

comment:8 in reply to:  7 Changed 2 years ago by AntC

Replying to diatchki:

Here is a simplified version of the example in the ticket:

Thanks Iavor, are you sure this is the ticket you meant? This one is about the order of declaration of instances affecting type inference, and the problem seems to have cleared up, according to comment:5.

class Foo a b c | a b -> c

instance Foo (x, a) x ((), a)
instance Foo (x, a) a (x, ())

These two instances are accepted by GHC 8.0.1, ...

You mean the instance decls compile? They partially overlap, so GHC will delay any error reporting until a use site.

... but should be rejected as they violate the FD on the class.

They're inconsistent only for the cases of overlap per your counter-example below, not in general. That is, not when x is different to a.

Here is the counter example:

Foo (Int,Int) Int ((), Int)
Foo (Int,Int) Int (Int, ())

I get attempts at those usages roundly rejected by GHC. (It suggested I AllowAmbiguousTypes, but that didn't help. I also switched on UndecidableInstances to give it maximum help.)

{-# LANGUAGE   MultiParamTypeClasses, FunctionalDependencies,
              FlexibleInstances, FlexibleContexts,
              AllowAmbiguousTypes, UndecidableInstances   #-}
 
class Foo a b c | a b -> c where { foo :: a -> b -> c }
 
instance Foo (x, a) x ((), a) where foo (x, a) x2 = ((), a)
instance Foo (x, a) a (x, ()) where foo (x, a) a2 = (x, ())

f1 = foo (True, 'c') False 
f2 = foo (True, 'd') 'e'
f3 = foo (5 :: Int, 7 :: Int) (9 :: Int)
 
main = print $ "results" ++ show f1 ++ show f2  ++ show f3

prog.hs:12:6: error:
    • Couldn't match type ‘Int’ with ‘()’
        arising from a functional dependency between:
          constraint ‘Foo (Int, Int) Int (Int, ())’
            arising from a use of ‘foo’
          instance ‘Foo (x, a) x ((), a)’ at prog.hs:7:10-29
    • In the expression: foo (5 :: Int, 7 :: Int) (9 :: Int)
      In an equation for ‘f3’: f3 = foo (5 :: Int, 7 :: Int) (9 :: Int)

(Per the O.P., if I switch round the order of those instance declarations, I do get a different error message, essentially just a mirror image.)

comment:9 Changed 2 years ago by diatchki

I mean that the example I gave should be rejected, but the program is accepted.

The check for FD consistency is done when multiple instances come together, not when you use them. This is necessary, because it ensures that the FD invariant on the class holds, and then we can use the invariant in whatever context we want. For the same reason, you can't have instances be consistent only in some cases.

Currently GHC is very conservative in its use of FDs---it uses them only for type inference. This is why having inconsistent instances like the example I showed is not the end of the world: it may result in odd behavior where GHC sometimes infers the one type and sometimes the other, but the final result is still a sound Haskell program.

For example, if GHC encountered a constraint Foo (Int,Int) Int a, where a is a unification variable, it might instantiate a as either ((),Int) or (Int,()) depending on in what order it happened to consult the instances. This is essentially the problem that was reported in the ticket.

However, if GHC was to start using the FDs fully as they were intended, having inconsistent instances would lead to unsound type-checking. For example, in this case, GHC should be able to prove that ((),Int) ~ (Int,()), which is obviously bogus.

comment:10 in reply to:  9 Changed 2 years ago by AntC

Replying to diatchki:

I mean that the example I gave should be rejected, but the program is accepted.

Sorry, Iavor, I'm not following. GHC as at 8.0.1 seems to be behaving as documented here http://downloads.haskell.org/~ghc/8.0.2/docs/html/users_guide/glasgow_exts.html#instance-resolution

  • It is fine for there to be a potential of overlap (...); an error is only reported if a particular constraint matches more than one [instance].

.

The check for FD consistency is done when multiple instances come together, not when you use them.

Are you saying this is what you'd like to see happening? What GHC is actually doing is checking FD consistency when it sees the instance decls, and only rejecting if the instances are outright contradictory. If there's only a potential inconsistency (due to overlap), GHC only rejects at the use site if it can't resolve to a particular instance.

.

This is necessary, because it ensures that the FD invariant on the class holds, and then we can use the invariant in whatever context we want. For the same reason, you can't have instances be consistent only in some cases.

Again, I think you're saying you'd like to be able to "use the invariant"/rely on them being consistent(?)

.

Currently GHC is very conservative in its use of FDs---it uses them only for type inference.

Yes GHC is conservative. Whereas in the FDs-via-CHRs paper, it is expected that under an FD C a b | a -> b if we have C a b and C a b' we can conclude b = b' (that's type equality, not just unifiability); GHC does not arrive at any such conclusion.

.

This is why having inconsistent instances like the example I showed is not the end of the world: it may result in odd behavior where GHC sometimes infers the one type and sometimes the other, but the final result is still a sound Haskell program.

For example, if GHC encountered a constraint Foo (Int,Int) Int a, where a is a unification variable, it might instantiate a as either ((),Int) or (Int,()) depending on in what order it happened to consult the instances. This is essentially the problem that was reported in the ticket.

Yes that is the problem reported on the ticket. AFAICT is was still a problem at 7.10. I see no evidence it is still happening at 8.0. (I've tried the same code at both versions.) I agree with @Reid it's rather discomforting this change of behaviour can't be nailed down to a specific mod.

What you can still do in 8.0 is put a type signature, to get inconsistent behaviour:

f4 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: ((), Int)     -- results in ((), 7)
f5 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: (Int, ())     -- results in (5, ())

.

However, if GHC was to start using the FDs fully as they were intended, having inconsistent instances would lead to unsound type-checking. For example, in this case, GHC should be able to prove that ((),Int) ~ (Int,()), which is obviously bogus.

Hmm. "as they were intended" is rather debatable. For each of the examples you're bringing forward, you're using several extensions of Haskell beyond Haskell 2010: UndecidableInstances or non-full dependencies (in a way that breaks the FDs-via-CHRs rules) or overlap -- either OverlappingInstances or overlap of the types in a non-full dependency. In this case we're now discussing you need FlexibleInstances, again not envisaged in the paper.

I think each of those extensions is justifiable. Furthermore for GHC to be using FD inference as per the FDs-via-CHRs rules would block separate compilation. (The CHRs assume you can see all instance decls.) So I think it's prudent GHC does not try to go that far, and therefore avoids the risk of unsound type-checking.

comment:11 Changed 2 years ago by diatchki

The check for overlapping is done when GHC resolves instances. This is unrelated to this example. You can easily modify it, so that there are no overlapping instances:

class Foo tag a b c | a b -> c

instance Foo Int (x, a) x ((), a)
instance Foo Bool (x, a) a (x, ())

The check for the consistency of FDs ought to be done whenever instances exist in the same scope, and there are two ways in which this can happen:

  1. they were declared in the same module, in which case GHC will try to check their consistency---as this example illustrates, we have a bug in the checking code, as the instances are not reported as inconsistent;
  1. when instances are imported into the same module. In this case GHC doesn't try to validate the comparability of the instances at all, which leads to obviously inconsistent FDs (e.g., F Int Int in one module, F Int Char in another, and both are OK when imported in a third module). It also leads to the fairly well-known bug of incoherent instances where GHC will happily allow two different instances for the same type tp be used in different modules.

As far as I can tell, the new behavior in 8 is how GHC uses FDs to perform improvements. Instead of just using one of the instances, it will now try to improve with all of the instances. As a result, if there are inconsistencies, it will try to improve in two different ways, and report a delayed error.

The underlying bug of failing to detect the inconsistency of the instances is still present.

The thing that we should be checking is:

forall x1 a2 x2 a2. ( (x1,a1) ~ (x2,a2), x1 ~ a2 ) => ( ((), a1) ~ (x2, ()) )

comment:12 in reply to:  11 Changed 2 years ago by AntC

Replying to diatchki:

The check for overlapping is done when GHC resolves instances. This is unrelated to this example. You can easily modify it, so that there are no overlapping instances:

class Foo tag a b c | a b -> c

instance Foo Int (x, a) x ((), a)
instance Foo Bool (x, a) a (x, ())

No, that class decl is not allowed, according to the FDs-via-CHRs paper, Section 6.2 on Non-full dependencies. (And this example is similar to yours on #10675 -- which I think is also disallowed.) If the FD is non-full, the class must have a super-class constraint to enforce the FD. Otherwise we still get inconsistent behaviour, which is your complaint on #10675.

.

The check for the consistency of FDs ought to be done whenever instances exist in the same scope, ...

You mean like dear old Hugs? Yes I miss it for that reason. But I think you can still get inconsistent behaviour with overlapping instances, if some instances are in scope in one module but different instances in scope in a different module.

I think what it needs is to ban overlap altogether. (And that means for non-full FDs, banning overlap of the params involved with that FD. We have to be canny there: allow identical params, modulo alpha renaming.) Then we just reject any instance that attempts to overlap. (Again Hugs in effect did that with its check "Instance is inconsistent with FunDeps".)

But what we can do currently with overlapping instances is useful. We need a more expressive way to say in the instance: yes I know this looks like it overlaps, but actually I don't want it to; when the use site appears to be ambiguous, always pick that instance. For example with instance guards:

class Foo a b c | a b -> c

instance Foo (x, a) x ((), a)   | x /~ a
instance Foo (x, a) a (x, ())

The guard on that first instance says: x must not be unifiable with a, so do not select this instance if unifiable. That's the same as Richard's apartness check for Closed Type Families selecting equations. More discussion here https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/

.

As far as I can tell, the new behavior in 8 is how GHC uses FDs to perform improvements. Instead of just using one of the instances, it will now try to improve with all of the instances. As a result, if there are inconsistencies, it will try to improve in two different ways, and report a delayed error.

"New"? You're describing the behaviour Simon raises in #10675, which was at 7.10. And judging by "Examples in the testsuite that exploit this loophole ", it's been around for some time. I agree with you that GHC should not try to merge or mingle/mangle type improvements from different instances. The behaviour in #10675 is just nuts. (But trying to cure it might be worse than the disease. It does seem to be a swamp.)

.

The underlying bug of failing to detect the inconsistency of the instances is still present.

The thing that we should be checking is:

forall x1 a2 x2 a2. ( (x1,a1) ~ (x2,a2), x1 ~ a2 ) => ( ((), a1) ~ (x2, ()) )

Yes, which we can do with a superclass constraint, such as a type function with equality constraint.

Note: See TracTickets for help on using tickets.