Okay, I get the difference. The "T a" annotation in "val :: T a)"and "val :: T a" does not help choose the "C a" dictionary. But the "val :: a-> T a" and "val (undefined :: a)" allows "a" to successfully choose the "C a" dictionary. val :: T a fixes "T a" but does not imply "C a". (undefined :: a) fixes "a" and does imply "C a". I now see how the functional dependency works here (which I should have tried to do in the first place -- I should have thought more and relied on the mailing list less). "class C a b | a -> b" is here "class C a where type T a = b". So only knowing "T a" or "b" does not allow "a" to be determined. -- Chris Tom Schrijvers wrote:
I don't see how your example explains this particular error. I agree Int cannot be generalized to (T Int) or (T Bool).
Generalized is not the right word here. In my example T Int, T Bool and Int are all equivalent.
I see Stefan's local type signature is not (val :: a) like your (val ::Int) but (val :: T a) which is a whole different beast.
Not all that different. As in my example the types T Int, T Bool and Int are equivalent, whether one writes val :: Int, val :: T Int or val :: T Bool. My point is that writing val :: T Int or val :: T Bool does not help determining whether one should pick the val implementation of instance C Int or C Bool.
And (T a) is the type that ghc should assign here.
As my example tries to point out, there is not one single syntactic form to denote a type.
Consider the val of in the first component. Because of val's signature in the type class the type checker infers that the val expression has a type equivalent to T a2 for some a2. The type checker also expects a type equivalent to T a, either because of the type annotation or because of the left hand side. So the type checker must solve the equation T a ~ T a2 for some as yet to determine type a2 (a unification variable). This is precisely where the ambiguity comes in. The type constructor T is not injective. That means that the equation may hold for more than one value of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type checker complains:
Couldn't match expected type `T a2' against inferred type `T a'.
Maybe you don't care what type is chosen, if multiple ones are possible. My example tried to show that this can effect the values computed by your program. So it does matter.
For this particular example, it seems that the type checker does not have have more than alternative for a2 in scope. However, it is not aware of that fact. It uniformly applies the same general strategy for solving equations in all contexts. This is a trade-off in type system complexity vs. expressivity.
There is an opportunity for exploring another point in the design space here.
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/