[Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

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?

No, it is not know.  Why do you think it is?

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

No.  The problem with a functions that has an ambiguous signature is  
that it contains type variables that are impossible to constrain by  
applying the function.  Providing a type signature at the application  
site makes this no easier.  Why?  Consider what a type annotation  
means.  By writing e :: t, you express your intent to use e at type t,  
but you also force the compiler to check that whatever type it derives  
for e is more general than t.  It is this check for type subsumption  
that is the tricky bit when typing TFs (or FDs).  See <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html 
 > for more detail on why this is a hard problem.

The problem with an ambiguous signature is that the subsumption check  
always fails, because the ambiguous signature contains some type  
variables for which the type checker cannot deduce a type instance.   
(You as a human reader may be able to *guess* an instance, but HM- 
based inference does generally not guess.  It's a deterministic  
process.)

The problem is really with foo and its signature, not with any use of  
foo.  The function foo is (due to its type) unusable.  Can't you  
change foo?

Manuel