[Haskell-cafe] Equality constraints in type families

[Claus Reinke]

> was hoping for. in fact, the decomposition rule seems to be 
> saying that type function results cannot matter, only the 
> structure of type family applications does:
> 
>    F x y ~ F u v <=> F x ~ F u /\ y ~ v
> 
> or do you have a specific type rule application order in mind
> where all type-level reductions are performed before this
> decomposition rule can be applied?

hmm, it seems that here i was confused by the extra syntactic
restrictions you have alluded to, meaning that the decomposition
rule only applies to extra parameters, not to the type indices.
also, given

    type family F a :: * -> *

'F x' and 'F u' are full applications, so may still be rewritten
according to the family instance rules, which means that
decomposition does not prevent reduction.

it would really be helpful to have local indications of such
differences that have an influence on interpretation, eg, a
way to distinguish the type indices from the extra parameters.

given that type families are never meant to be partially 
applied, perhaps a different notation, avoiding confusion
with type constructor applications in favour of something
resembling products, could make that clearer?

something simple, like braces to group families and indices:

    type family {F a} :: * -> *
    {F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v

would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters 
are subject to the decomposition rule.

assuming that you are going to rule out partial applications
of type synonyms (example 1) and type families (example 2)
in the rhs of type family instances for now, i think that answers
my questions in this thread, although i'd strongly recommend
the alternative syntax, grouping type indices with braces.

sorry about the confusion,
claus