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