#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: dimitris@…, diatchki (added) Comment: 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). Iavor? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9210#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler