[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke:
> one might say that the central point of example two were two
> partially applied type synonym families in the same position
> (rhs of a type synonym family instance definition).
>
> usually, when reduction meets typing, there is a subject reduction
> theorem, stating that types do not change during reduction. since,
> in this case, reduction and constraint generation happen at the
> same (type) level, the equivalent would be a proof of confluence,
> so that it doesn't matter which type rules are applied in which
> order (in this case, decomposition and reduction).

Well, we still need normal subject reduction (i.e., types don't change  
under value term reduction), and we have established that for System  
FC (in the TLDI paper).

In addition, type term normalisation (much like value term  
normalisation) needs to be confluent; otherwise, you won't get a  
complete type inference/checking algorithm.

> as far as i could determine, the TLDI paper does not deal with
> the full generality of ghc's type extensions, so it doesn't stumble
> over this issue, and might need elaboration.

System FC as described in the paper is GHC's current Core language.   
What are you missing?

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

> and i still don't like the decomposition rule, and i still don't
> even understand that first part about comparing partially applied  
> type constructors!-)

Haskell always had the decomposition rule.  Maybe we confused the  
matter, by always showing a particular instance of the decomposition  
rule, rather than the general rule.  Here it is in all it's glory:

   t1 t2 ~ t1' t2'  <==>  t1 ~ t1', t2 ~ t2'

No mention of a type family.  However, the rule obviously still needs  
to be correct if we allow any of the type terms (including t1 and t1')  
to include *saturated* applications of type families.

Manuel