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?

Just to make sure. If you remove both of the first two instances there's still an error, right? — genisage
– genisage, Commented Feb 13, 2015 at 19:04
I can't reproduce the second part here. instance C (l i j) (r i j) i causes a conflict for me. (on ghc 7.8.3) — genisage
– genisage, Commented Feb 13, 2015 at 19:30
@ØrjanJohansen I tried it again and still got a conflict. I'm currently using windows and the Haskell platform. — genisage
– genisage, Commented Feb 13, 2015 at 20:05

Ørjan Johansen · Accepted Answer · 2015-02-13 19:25:21Z

6

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.

answered Feb 13, 2015 at 19:25

Ørjan Johansen

18.2k3 gold badges46 silver badges53 bronze badges

Sign up to request clarification or add additional context in comments.

2 Comments

chi Over a year ago

I'd agree with you. Experimenting, I found that class C a b ; instance C (l (i,j)) (r (i,j)) ; instance C (l i j) (r i j) is accepted without mentioning the overlap (!?). Maybe now some overlaps are being detected only later, when a method is called (just guessing here).

Nicolas Malebranche Over a year ago

Thank you for pointing out the unification process. @chi: Indeed, if I try to write a class method f :: a -> b -> c I get a complaint abount incoherency when calling f

Collectives™ on Stack Overflow

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

1 Answer 1

2 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

2 Comments

Your Answer

Sign up or log in

Post as a guest

Related