[Haskell-cafe] type families and type signatures

[Sittampalam, Ganesh]

Manuel Chakravarty wrote:
>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.

No, I meant can't it derive that equality when matching (Id a) against (Id b)?
As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known,
surely?

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

My real code is somewhat analogous to (foo :: (Id Int -> Id Int)) (1::Int).
Isn't that unambiguous in the same way as (show.read) is if I give show or
read a signature?

Cheers,

Ganesh

==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================