Manuel Your short program tickles a lot of different questions. Here's an explanation. Simon | Assume the following type class declarations with functional | dependencies: Actually much of the behaviour you see happens without fundeps. | > {-# OPTIONS -fglasgow-exts #-} | > | > class C a b c | a b -> c where | > foo :: (a, b) -> c | > | > instance C a a r => C a (b, c) r where | > foo (a, (b, c)) = foo (a, a) You are already on dodgy ground here, because the instance decl doesn't guarantee that the bit before the => is smaller than the bit after the =>. E.g. context reduction could go: C (Int,Int) (Bool, Bool) r --> C (Int,Int) (Int,Int) r --> C (Int,Int) (Int,Int) r So [Point 1]: GHC should require -fallow-undecidable-instances if you use repeated type variables before the =>. | Now, in GHCi (version 6.4), | | > *FDs> let bar x = foo ((x, x), (x, x)) | > *FDs> :t bar | > bar :: (C (a, a) (a, a) c) => a -> c | | but GHC is also happy to accept the more general type | | > bar :: a -> c | > bar x = foo ((x, x), (x, x)) There are two separate things going on here [Point 2] GHC postpones context reduction until it's forced to do it (except if a single step will eliminate the dictionary altogether). Example: data T a = T a instance Eq (T a) bar x = [T x] == [] GHC will *infer* bar :: Eq [T a] => a -> Bool, but it will happily *check* bar :: a -> Bool bar x = [T x] == [] The reason for this lazy context reduction is overlapping instances; in principle there might be more instances for Eq [T a] at bar's call site. But now I look at it again, I think it would be OK to postpone context reduction only if there actually were overlapping instances (right here at bar's defn). That might be a good idea because it'd give less confusing types perhaps. However, note that the two types are indeed equivalent -- both are more general than the other. It's like saying (Eq Int => t) <= t, and vice versa. [Point 3] As Iavor notes, yes, GHC is building recursive dictionaries. Suppose GHC is trying to find evidence for constraint C from a set of constraints (with evidence provided) D. Suppose it finds an instance decl D' => C which matches C. Then it tries to prove the constraints D'. The new bit is that it adds C to D before trying to prove D'. That's all! This is Jolly Useful sometimes. (See John Hughes's paper about restricted type synonyms for example.) It's a bit like infinite data structures. ML doesn't let you build them, so there's a static error. Haskell does, and that is sometimes just what you want; and sometimes gives you runtime divergence (e.g. take the length of an infinite list). In the same way, this recursive-dictionary thing is sometimes just what you want; but sometimes gives you runtime divergence instead of a static error. | Again, in GHCi, | | > *FDs> let bar x = foo ((x::Int, x), (x, x)) | > *FDs> :t bar | > bar :: Int -> () | | (which by itself is bizarre) This is the first time when the functional dependency plays a role.
From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int) c), and the type (Int -> c). Now GHC tries to decide what to quantify over. Shall we quantify over c? Well, no. GHC never quantifies over type variables that are free in the environment (of course) OR are fixed by functional dependencies from type variables free in the environment. In this case the functional dependencies tell us that since (Int,Int) is obviously completely fixed, then there's no point in quantifying over c.
So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is satisfied via the recursive dictionary thing, leaving 'c' completely unconstrained. So GHC chooses c to be (), because it doesn't like to leave programs with completely free type variables. | but it also accepts | | > bar :: Int -> c | > bar x = foo ((x::Int, x), (x, x)) Here you are *telling* GHC what to quantify over, so the inference of what to quantify doesn't happen.