#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by simonpj: Old description:

Consider {{{ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}

class C a b | a -> b where op :: a -> b

instance C [x] [x] instance {-# OVERLAPS #-} C x y => C [x] [Maybe y]

f x = op [x] }}} Should these two instance declarations be accepted? They are simply ''inconsistent'' in the sense of Definition 6 of the [http://research.microsoft.com/en-us/um/people/simonpj/papers/fd- chr/jfp06.pdf FDs through CHRs paper].

Sadly GHC does not currently reject these as inconsistent. As a result it'll use ''both'' instance for improvement. In the definition of `f` for example we get {{{ C [alpha] beta }}} where `x:alpha` and the result type of `f` is `beta`. By using both instances for improvement we get {{{ C [Maybe gamma] [Maybe gamma] }}} Is that what we want? The two instances don't ''contradict'' each other, but neither do they agree as all published work on FDs says they should!

Examples in the testsuite that exploit this loophole are {{{ ghci/scripts ghci047 polykinds T9106 typecheck/should_compile FD4 typecheck/should_compile T7875 }}} I'm not sure what the right thing here is.

New description: Consider {{{ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-} class C x a b | a -> b where op :: x -> a -> b instance C Bool [x] [x] instance C Char x y => C Char [x] [Maybe y] f x = op True [x] }}} Should these two instance declarations be accepted? The two instances don't ''contradict'' each other, but neither do they agree as all published work on FDs says they should! They are ''inconsistent'' in the sense of Definition 6 of the [http://research.microsoft.com/en-us/um/people/simonpj/papers/fd- chr/jfp06.pdf FDs through CHRs paper]. Sadly GHC does not currently reject these as inconsistent. As a result it'll use ''both'' instance for improvement. In the definition of `f` for example we get {{{ C Bool [alpha] beta }}} where `x:alpha` and the result type of `f` is `beta`. By using both instances for improvement we get {{{ C Bool [Maybe gamma] [Maybe gamma] }}} That can be solved, so we get {{{ f :: Maybe x -> [Maybe x] }}} But where did that `Maybe` come from? It's really nothing to do with it. Examples in the testsuite that exploit this loophole are {{{ ghci/scripts ghci047 polykinds T9106 typecheck/should_compile FD4 typecheck/should_compile T7875 }}} I'm not sure what the right thing here is. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jstolarek (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"d53d80890f2762b78071f5d53c88dc9e6c0ca72e/ghc" d53d8089/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="d53d80890f2762b78071f5d53c88dc9e6c0ca72e" Refactoring around FunDeps This refactoring was triggered by Trac #10675. We were using 'improveClsFD' (previously called 'checkClsFD') for both * Improvement: improving a constraint against top-level instances * Consistency: checking when two top-level instances are consistent Using the same code for both seemed attractive at the time, but it's just too complicated. So I've split it: * Improvement: improveClsFD * Consistency: checkFunDeps Much clearer now! }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rwbarton): See also #9210, where a potential fix broke the same four test cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: 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): ''Should these two instance declarations be accepted?'' Depends what you mean by "accepted". I think the case is suffering from GHC's delayed/lazy instance enforcement, as affects the complications of confluence around partially overlapping instances. The `C Char ...` instance clearly could never work -- its constraint needs an infinite regress on `C Char [[[[ ... ]]]] ...`. Is anybody saying that instance on its own should be rejected? If so, see counter-example/highly valuable exploit below. It's an interesting experiment trying to find valid calls for `f` [I'm using 7.10]. This works: `f (Just "quoi?")`. This doesn't: `f ("quoi")` -- GHC complains `"Couldn't match expected type 'Maybe y0' with actual type '[Char]'"`. So GHC __is__ applying the fundep `a -> b` Consistency Condition as per '''Definition 6''' in the CHRs/Mark Jones 2000 paper. It is taking `[x] [Maybe y]` to infer that in `[x] [x]` we must have `x ~ Maybe y` -- as the O.P. is saying. I think we've no reason to reject this example. Or perhaps Iavor could explain what "loophole" this opens up? Can it result in type incoherence? Before we reject this example as bogus, @Richard, I think there are examples similar to it that might get caught in the crossfire. [That's the reason I arrived here, because I'm trying to understand how/why the FunDeps work for it.] The classic Type-level type equality test: {{{ class TTypeEq (a :: *) (a' :: *) (b :: Bool) | a a' -> b instance TTypeEq a a True instance (b ~ False) => TTypeEq a a' b }}} Seems to break '''Definition 6'''. There's a substitution for the two instances that makes the determinants of the FunDep equal, namely `{a' ~ a}`. And under that substitution, the dependents are not equal `{b vs False}`. FWIW, Hugs applies a stricter interpretation of '''Definition 6''', with the consequence no such declaration of `TTypeEq` is accepted [explored in Oleg/Ralph's HList paper]. Or if we include substitution `{b ~ True}`, that substitution invalidates the constraint on the `False` instance. Clearly GHC isn't evaluating the instance's constraints for consistency with its improvement of the class parameters. We can't write that second instance as: {{{ instance TTypeEq a a' False }}} GHC complains `"Functional Dependencies conflict between instance declarations"` What would any proposed fix for this ticket do to a class like? {{{ class TTypeEq2 x a a' b | a a' -> b instance TTypeEq2 Bool a a True instance TTypeEq2 Char a a True instance (b ~ False) Bool a a' b instance (b ~ False) Char a a' b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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): Some afterthoughts: * What if the instances from the O.P. were declared in separate modules? Then GHC couldn't apply the mutual improvement. Would it reject the instances as inconsistent? * I find the statement of '''Definition 6''' in the CHR paper a bit imprecise. Mark Jones 2000 paper is clearer [Section 6.1]. It says "if `tX` and `sX` have a most general unifier `U`, then `UtY = UsY`." where `tX, sX` are the determinant types from the instance decl, `tY, sY` are the dependents. * I wonder if what GHC is doing to apply that test is rather than `UtY = UsY`, it's checking `UtY ~ UsY` -- that is, checking unifiability rather than equality(?) That would explain the behaviour with the `TTypeEq` examples. * Re the "dysfunctional" Functional Dependencies ;-), we could do with some better way of writing instances to give maximum help for type improvement. Currently you keep running up against instance-FunDep conflicts. And I don't think Injective type functions help much. For example type-level `Plus` over `Nat`s, with three-way FunDeps. [Yes I know Oleg worked it out years ago, but it's a ''tour de force''.] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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): Thanks Iavor, * Yes the `C Char ...` instance is vacuous. I think GHC must accept it, because for all it knows there is some other instance decl for `C` that will provide a base case. That tells us we should be cautious if an instance (or set of instances) is accepted: the instances alone are weak evidence until/unless we can prove they can be inhabited. * I think what Simon's worried about is that the two instance decls have got entangled. And yet they don't overlap. So I'd be suspicious we'd see different behaviour under separate compilation. * Your instances for `F` break the FunDep coverage condition, so presumably you needed UndecidableInstances. What's reasonable to expect after that? I did get some types to inhabit those instances; and yes they were inconsistent with the Fundeps on `F`. * I guess GHC with UndecidableInstances sees there's a constraint on the instance (`G`, `H`), and that constraint carries a FunDep, so delegates the FunDep to it. We know GHC doesn't/can't chase round all the constraints, because it can't see all the instances. It delays that check to the use site -- but then that only considers the instances selected at that site. * Constraints like you've put are useful -- the type-level Type Equality test example. Arguably any such Type Equality test breaks '''Definition 6''' Consistency condition. * Does your example actually do any harm anywhere? Could some distant module end up treating an Int as a Char/segfaulting? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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 simonpj): Let me note that the commit in comment:5 added this note {{{ Note [Bogus consistency check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In checkFunDeps we check that a new ClsInst is consistent with all the ClsInsts in the environment. The bogus aspect is discussed in Trac #10675. Currenty it if the two types are *contradicatory*, using (isNothing . tcUnifyTys). But all the papers say we should check if the two types are *equal* thus not (substTys subst rtys1 `eqTypes` substTys subst rtys2) For now I'm leaving the bogus form because that's the way it has been for years. }}} Would someone like to fix the bogus-ness as suggested, and check what, if anything, goes wrong. (See #9210 comment:4 for some possible testsuite failures. Maybe they SHOULD fail.) It'd be worth checking what Hackage libraries build before, but fail to build after. This has been wrong for a long time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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:15 simonpj]: On the broader issue of should those instances be accepted together

Let me note that the commit in comment:5 added this note {{{ ... Currenty [checking] if the two types are *contradicatory*, using (isNothing . tcUnifyTys). But all the papers say we should check if the two types are *equal* thus ... }}}

Thank you. So that confirms my suspicion in comment:11, bullet 3.

{{{ For now I'm leaving the bogus form because that's the way it has been for years. }}}

Yes I think that's wise, given how many fragile programs are out there using FunDeps and overlaps.

Would someone like to fix the bogus-ness as suggested, and check what, if anything, goes wrong.

I'm keen to help, but lack the resources or expertise.

It'd be worth checking what Hackage libraries build before, but fail to build after.

I would guess that any library using type-level programming switches on `UndecidableInstances` by default, whether or not it actually needs it.

(... Maybe they SHOULD fail.) This has been wrong for a long time.

Given the howls every time GHC tries to apply the FunDep rules more strictly; and given how long a time it's been wrong; I wonder if there's a softly-softly strategy? * Move from module-wide `UndecidableInstances` to a per-instance {-# UNDECIDABLE #-} pragma. (Same idea as with {-# OVERLAP* #-}.) * The '''Coverage Condition''' is defined in terms of checks on each instance alone, so it's just more closely targetting the logic. * Being in the instance gives a more in-your-face signal that this instance is suspicious -- essentially the programmer is acknowledging GHC can't necessarily enforce the '''Consistency Condition'''. * And I suspect a large proportion of instances do obey the '''Coverage Conditions'''. Could we go further to a per-parameter-per-instance flag? * The idiom I see is there's a bare type var in the instance decl, for the target of the FunDep. It doesn't appear elsewhere in the head, so it's breaking the '''Coverage Condition'''. But there's an equality constraint on it, where the improved type __would__ meet the '''Coverge Condition'''. Like: {{{ instance (b ~ False) => TTypeEq a a' b -- breaks Coverage, compare: instance TTypeEq a a' False -- Coverage OK }}} * The reason for the bare type var is to ensure this instance is {-# OVERLAPPABLE #-}; and a more specific instance will override it. With `{-# LANGUAGE IrrefutableInstanceParams #-}` (or some equally ugly name), you can go: {{{ instance TTypeEq a a' ~False -- tilde prefix ? maybe too subtle }}} This: 1. Is syntactic sugar for the form with Equality constraint, for a fresh- generated type var. 2. Means the compiler can validate the '''Coverage Condition''', so this doesn't need {-# UNDECIDABLE #-} 3. Lets the dog see the rabbit: the compiler can check the '''Consistency Condition'''. [To bikeshed about syntax, it's pleasing `~` is already the prefix for irrefutable pattern matches, and the operator for type Equality constraints. It appearing within the instance head is currently illegal syntax; but I guess with a very badly formed head, it might be confused with a type operator(?)] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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 [ticket:10675 simonpj]:

Should these two instance declarations be accepted?

* I'm going to '''argue they should''' * In addition to the bogusness documented on this ticket, there's a '''design weakness''' in the FunDep consistency check. * Exploiting that with malice aforethought, there's some '''disturbing behaviour''' '''Argument to accept:''' Yes GHC's consistency check is bogus/contrary to all the literature. But it's been in place since at least 2004. Lot's of code relies on it. So we can provide no grounds to reject the instances, unless we can look also at other class params not involved in the FunDep. But then according to the Type Families work, a FunDep should be equivalent to a superclass equi constraint with a Type Family call. I.e. {{{ class C x a b | a -> b where -- O.P. class (F a ~ b) => C x a b where -- Type Family F }}} The Type Family can look only at the class's second parameter. The (weird) unification behaviour described in the O.P. is in effect trying to reverse engineer `F`'s equations from the class instances. So ghc must unify. OTOH there's no definition for `F` you could write that would be consistent with where ghc ends up in the type for function `f`. '''Design weakness:''' in ghc checking instances for FunDep consistency is that it only checks (and unifies) pairwise. It doesn't check all instances globally. Then arguably '''Definition 6 (Consistency Condition)''' in the ''FunDeps via CHRs'' paper is too weak. (Note that the definition of Functional Dependency in database theory quantifies across all rows in a table.) '''Disturbing behaviour:''' consider this exploit {{{ {-# LANGUAGE as per O.P. #-} class C x a b | a -> b where -- as O.P. op :: x -> a -> b instance C Bool [x] (x, Bool) instance C Char x y => C Char [x] (Int, y) instance C Char x y => C Char [x] (y, y) f x = op True [x] -- as O.P. }}} Quick: what type inferred for `f`? What odds would you lay it's `f :: Int -> (Int, Int)`? Luckily we can't actually call `f`: `Couldn't match type 'Bool' with 'Int'`. So the `True` parameter to `op` in `f`'s rhs is trying to pick the 'right' instance for `C`. More disturbingly, if you switch round the order of instances, you'll get a different inferred type for `f`: it's the unifier of whichever are the last two instances. (Full disclosure: this is at ghc 8.0.1. Sensitivity to ordering of instances sounds like #9210, but that seems to have gone away at 8.0.) The fix in all these examples is to make the FunDep full (which it really should be) {{{ class C x a b | x a -> b where }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10675: GHC does not check the functional dependency consistency condition correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 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): Applying the [ticket:15632#comment:2 suggested rules here] * The instances on the O.P. get rejected as inconsistent under the FunDep, because A) Upon unifying the `a` parameter positions (argument to the FunDep), applying the substitution to the `b` position does not give ''equal'' type for the result. B) i) The FunDep is not full. ii) The instance heads overall are in no substitution ordering (they're apart). If you insist on those instances go either {{{#!hs instance C Bool [x] [x] -- per O.P. instance {-# OVERLAPPABLE #-} C' x a b => C x a b where -- catch-all op = op' class C' x a b | a -> b where op' :: x -> a -> b instance C Char x y => C' Char [x] [Maybe y] -- per O.P. but indirect f x = op True [x] -- per O.P. -- inferred ===> f :: C Bool [a] [a] => a -> [a] }}} or {{{#!hs instance C Char x y => C Char [x] [Maybe y] -- per O.P. instance {-# OVERLAPPABLE #-} C'' x a b => C x a b where -- catch-all op = op'' class C'' x a b | a -> b where op'' :: x -> a -> b instance C'' Bool [x] [x] -- per O.P. but indirect f x = op True [x] -- per O.P. -- inferred ===> f :: a -> [a] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10675#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler