Haskell functional dependency a b -> c depending on c?

Question

Consider the following Haskell code:

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

class C a b c | a b -> c

instance C (l (i,j)) (r i j)   j
instance C (l i j)   (r (i,j)) j
-- Conflict between the following two lines
instance C (l (i,j)) (r (i,j)) j  
instance C (l i j)   (r i j)   j

Here, GHC yields a functional dependencies error between the last two lines. If I drop any of the last two instance declarations, the code compiles. I tried an analogue using type families, which also produced a conflict. My first question is: Why do the last two lines conflict, while the other declarations all work fine together?

In addition, if I change the very last line to

instance C (l i j)   (r i j)   i

GHC accepts the code. This seems quite weird, since the only thing that changes is the dependent type variable c. Can somebody explain this behavior?

Answer 1

The last two instances have a conflicting unification. Let me use completely different variable names:

C (a c (d,e)) (b c (d,e)) e
vs.
C (a c (d,e)) (b c (d,e)) (d,e)

In particular, your l from the third instance can be unified with a type constructor which already has an argument applied.

Changing your j to i makes the last one instead:

C (a c (d,e)) (b c (d,e)) c

I still don't understand why that doesn't give a complaint. Perhaps it's because you can assign the types such that c = e, but not such that e = (d,e) (that would give an infinite type which Haskell doesn't allow), but it still seems like a dubious thing to allow. Perhaps this is even a GHC bug.

The other instance combinations don't conflict because when you try to unify them, you end up with contradictions similar to the e = (d,e) above, but in the non-dependent parts, so they cannot match.