[Haskell-cafe] type families and type signatures

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

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

perhaps, with closed type families, one might be able to
reason backwards (is there a unique 'a' such that 'Id a ~ Int'?),
as with bidirectional FDs. but if you want to flatten all
'Maybe'-nests, even that direction isn't unique.
 
> The type checking problem for foo' boils down to verifying the formula
> 
> forall a. exists b. Id a ~ Id b

naively, i'd have expected to run into this instead/first:

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

which ought to be true modulo alpha conversion, without guesses,
making 'foo'' as valid/useless as 'foo' itself.

where am i going wrong?
claus

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