[Haskell-cafe] Equality constraints in type families

[Claus Reinke]

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