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