On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very unintuitive. This is for the following reason.
Let's alpha-rename the signatures and use explicit foralls for clarity:
foo :: forall a. Id a -> Id a foo' :: forall b. Id b -> Id b
GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
Can't it derive (Id a ~ Id b), though?
Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name.
Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id b ~ Id b. Thanks for the explanation, anyway. I'll need to have another think about what I'm actually trying to do (which roughly speaking is to specialise a general function over type families using a signature which I think I need for other reasons). Generally speaking, is there any way to give a signature to foo'?
Given that this is a confusing issue, I am wondering whether we could improve matters by giving a better error message, or an additional hint in the message. Do you have any suggestion regarding what sort of message might have helped you?
I can't think of anything good. Perhaps printing out the (type classes + equalities) context would have helped me to see that it was empty and understand why, but probably not. Cheers, Ganesh