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