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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
