#9210: "overlapping instances" through FunctionalDependencies --------------------------------------------+------------------------------ Reporter: rwbarton | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by rwbarton): * version: 7.8.1 => 7.8.2 Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#9210: "overlapping instances" through FunctionalDependencies --------------------------------------------+------------------------------ Reporter: rwbarton | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by simonpj): * cc: dreixel (added) Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#9210: "overlapping instances" through FunctionalDependencies -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by AntC): * keywords: => FunDeps -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#9210: "overlapping instances" through FunctionalDependencies -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:7 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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#9210: "overlapping instances" through FunctionalDependencies -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:9 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.h... #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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#9210: "overlapping instances" through FunctionalDependencies -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:11 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler