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'.
{-# LANGUAGE TypeFamilies #-} module Test7 where
type family Id a
type instance Id Int = Int
foo :: Id a -> Id a foo = id
foo' :: Id a -> Id a foo' = foo
Is this expected?
Yes, unfortunately, this is expected, although it is very unintuitive. This is for the following reason.
Huh? This sounds very wrong to me, simply because foo and foo' have the very same type.
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.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes it "true" in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int -> Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo .
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.
Since both type variables are quantified, the types as a whole are the same, alpha conversion notwithstanding.
BTW, here is the equivalent problem using FDs:
class IdC a b | a -> b instance IdC Int Int
bar :: IdC a b => b -> b bar = id
bar' :: IdC a b => b -> b bar' = bar
Hugs rejects bar as ambiguous whereas GHC accepts bar but rejects bar' . Something is wrong here. I think that only rejecting both definitions due to ambiguity is correct, since bar has access to a from the class. For instance, consider class C a b | a -> b fromA :: a -> b oneA :: a instance C Int Int where fromA = const 1 oneA = 1 instance C Char Int where fromA = const 2 oneA = 'a' bar :: C a b => b -> b bar _ = fromA oneA This definition is clearly ambiguous, bar could be 1 or 2. The subtle difference in the type synonym family case is that a is "more parametric" there. At least, that's my feeling. In full System F , neither definition would be a problem since the type a is an explicit parameter. Regards, apfelmus