The extra syntax has its advantages (more local information) and
disadvantages (more clutter). We weren't convinced that we need the
extra syntax, so left it out for the moment. However, this is
something that can always be changed if experience shows that programs
are easier to understand with extra syntax. It doesn't affect the
type theory and is really a pure language design question. I'd be

I would go for the braces as Claus suggested, although not necessary they would have helped me to better understand how type family application behaves.

> | The most clean solution may indeed be to outlaw partial
> applications of
> | vanilla type synonyms in the rhes of type instances. (Which is
> what I
> | will implement unless anybody has a better idea.)
>
> i always dislike losing expressiveness, and ghc does almost seem
> to behave as i would expect in those examples, so perhaps there
> is a way to fit the partial applications into the theory of your TLDI
> paper.

I don't think we can avoid losing that expressiveness, as you
demonstrated that it leads to non-confluence of type term
normalisation - see also my reply to SimonPJ's message in this thread.
glad to hear some more opinions about this matter.

Since I was the one to start this thread, I have managed to implement what I initially wanted as F a :: *->* with F a x::*, and the cost of not having partially applied type synonyms was not much apart from some more equality coercions that I wasn't expecting.
The most relevant tradeoffs are some more extra parameters in type classes (notice the d in fmapF) and having to bind explicit signatures to variables that only occur as a type-index to the type family (notice id::x->x).

class FunctorF x where fmapF :: d -> (a -> b) -> F x a -> F x b
fff :: forall d x. (FunctorF d) => d -> F d x -> F d x

fff a = fmapF a (id::x->x)

Generally, I love type-indexed types.
hugo