[Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Claus Reinke:
>> type family Id a
>> type instance Id Int = Int
>>
>> foo :: Id a -> Id a
>> foo = id n
>> foo' :: Id a -> Id a
>> foo' = foo
>
> type function notation is slightly misleading, as it presents
> qualified polymorphic types in a form usually reserved for  
> unqualified polymorphic types.
>
> rewriting foo's type helped me to see the ambiguity that
> others have pointed out:
>
> foo :: r ~ Id a => r -> r
>
> there's nowhere to get the 'a' from. so unless 'Id' itself is
> fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't
> really be used. for each type variable, there needs to be
> at least one position where it is not used as a type family
> parameter.

Yes.  It is generally so that the introduction of indexed types (ie,  
all of GADTs, data type families, or synonym families) means that a  
type with a parameter is not necessarily parametric.

> it might be useful to issue an ambiguity warning for such types?

The problem is that testing for ambiguity is, in general, difficult.   
Whether a context is ambiguous depends for example on the currently  
visible class instances.  As a result, a signature that is ambiguous  
in a module M, may be fine in a module N that imports M.

However, I think what should be easier is to improve the error  
messages given when a function with an ambiguous signature is used.   
For example, if the error message in the definition of foo' would have  
included a hint saying that the definition is illegal because its  
right hand side contains the use of a function with an ambiguous  
signature, then Ganesh may have had an easier time seeing what's  
happening.

> ps. i find these examples and discussions helpful, if often initially
>       puzzling - they help to clear up weak spots in the practice
>       of type family use, understanding, and implementation,         
> thereby improving all while making families more familiar!-)

Absolutely!

Manuel