It's not exactly a bug, but it is a long story...
The Story
In 7.0 there used to be a coercion constructor called right which worked like this:
g : f a ~ f b
---------------
right g : a ~ b
That is, if g is a coercion between f a and f b, then right g is a coercion between a and b. This is only sound if f is guaranteed to be injective: otherwise we might legitimately have, say, f Int ~ f Char and then we would be able to conclude Int ~ Char, which would be Bad.
But of course, type synonyms and type families are not necessarily injective; for example:
type T a = Int
type family F a :: *
type instance F Int = Bool
type instance F Char = Bool
So how is this guarantee possible? Well, this is precisely the reason why partial applications of type synonyms and type families are not allowed. Partial applications of type synonyms and type families may not be injective, but saturated applications (even ones which result in a higher kind) always are.
Of course, the restriction on partial applications is annoying. So in 7.2, in an attempt to move in the direction of allowing partial application (and because it simplifies the theory and implementation of the coercion language), the right constructor was replaced by a constructor nth, with the accompanying rule
g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi
That is, nth only applies to a coercion g which is between two types which are known to be saturated applications of a type constructor T. In theory, this allows for partial applications of type synonyms and families, because we cannot decompose equalities until we know that they are between applications of a (necessarily injective) type constructor. In particular, nth does not apply to a coercion f a ~ f b because f is a type variable, not a type constructor.
It was thought at the time of the change that no one would really notice, but obviously this was wrong!
Interestingly, the Olegian trick outlined in the haskell-cafe message from Daniel Schüssler shows that the implementation of type families was not changed accordingly! The problem is that a definition like
type family Arg fa
type instance Arg (f a) = a
should not be allowed if f could be non-injective; in that case the definition does not even make sense.
Next Steps
I think the right thing to do is to reinstate right (or something equivalent), since people clearly want it! Hopefully this will be done soon.
In the meantime, it would still be really cool to allow partially applied type synonyms and families. It seems the Right Way (tm) to do that would be to track injectivity in the kind system: that is, each arrow kind would be annotated with its injectivity. This way when encountering an equality f a ~ f b we could look at the kind of f to determine whether it is safe to decompose it into the equality a ~ b. Not coincidentally, I am currently trying to work out the design of such a system. =)
