[Haskell-cafe] Re: type families and type signatures

[apfelmus]

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