[Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Ganesh Sittampalam:
> 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?

That's what it does derive as a proof obligation and finds it can't  
prove.  The error message you are seeing is GHC's way of saying, I  
cannot assert that (Id a ~ Id b) holds.

>> 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'?

Sorry, but in the heat of explaining what GHC does, I missed the  
probably crucial point.  Your function foo is useless, as is foo'.   
Not only can't you rename foo (to foo'), but you generally can't use  
it.  It's signature is ambiguous.  Try evaluating (foo (1::Int)).  The  
problem is related to the infamous (show . read).

Manuel