type family F a :: * -> * F x y ~ F u v <=> F x ~ F u /\ y ~ v
words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor.
i'm not sure haskell offers the kind of distinction that we need to talk about this: 'data constructor' is value-level, 'type constructor' doesn't distinguish between type- vs data-defined type constructors. i think i know what you mean, but it confuses me that you use 'data constructor' (should be data/newtype-defined type constructor?) and 'type constructor' (don't you want to exclude type-defined type constructors here). data ConstD x y = ConstD x type ConstT x y = x 'ConstD x' and 'ConstT x' have the same kind, that of type constructors: * -> *. but: ConstD x y1 ~ ConstD x y2 => y1 ~ y2 whereas forall y1, y2: ConstT x y1 ~ ConstT x y2 and i thought 'type family' was meant to suggest type synonym families, in contrast to 'data family'? you did notice that i gave an example of how ghc does not seem to follow that decomposition rule, didn't you? ghc seems to behave almost as i would expect, not as the decomposition rule seems to suggest. still confused, claus