#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