[Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

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.)

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.

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

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?

Manuel

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