On Sat, Jul 3, 2010 at 4:28 PM, Dan Doel
It's potentially not just a violation of intent, but of soundness. The following code doesn't actually work, but one could imagine it working:
class C a b | a -> b
instance C () a
-- Theoretically works because C a b, C a c implies that b ~ c -- -- GHC says b doesn't match c, though. f :: (C a b, C a c) => a -> (b -> r) -> c -> r f x g y = g y
The funny part is that GHC eventually would decide they match, but not until after it complains about (g y). For instance, if you do this: f :: (C a b, C a c) => a -> (b -> r) -> c -> r f x g y = undefined ...and load it into GHCi, it says the type is: > :t f f :: (C a c) => a -> (c -> r) -> c -> r As far as I can tell, type variables in scope simultaneously that "should" be equal because of fundeps will eventually be unified, but too late to make use of it without using some sort of type class-based indirection. This can lead to interesting results when combined with UndecidableInstances. For instance, consider the following: class C a b c | a b -> c where c :: a -> c -> c c = flip const instance C () b (c, c) f x = (c x ('a', 'b'), c x (True, False)) g :: (c, c) -> (c, c) g = c () This works fine: Because "b" remains ambiguous, the "c" parameters also remain distinct; yet for the same reason, "a" effectively determines "c" anyway, such that g ends up with the type (forall c. (c, c) -> (c, c)), rather than something like (forall c. c -> c) or (forall b c. (C () b c) => c -> c). But if we remove the (seemingly unused) parameter b from the fundep... class C a b c | a -> c where ...GHC now, understandably enough, complains that it can't match Char with Bool. It will still accept this: f x = c x ('a', 'b') g x = c x (True, False) ...but not if you add this as well: h x = (f x, g x) Or even this: h = (f (), g ()) On the other hand, this is still A-OK: f = c () ('a', 'b') g = c () (True, False) h = (f, g) Note that all of the above is without venturing into the OverlappingInstances pit of despair. I don't know if this is how people expect this stuff to work, but I've made occasional use of it--introducing a spurious parameter in order to have a fundep that uniquely determines a polymorphic type. Perhaps there's a better way to do that? - C.