[Haskell-cafe] Equality constraints in type families

[Claus Reinke]

>>> again, i gave a concrete example of how ghc behaves as i would  
>>> expect, not as that decomposition rule would suggest.
>>
>> Maybe you can explain why you think so.  I didn't understand why you  
>> think the example is not following the decomposition rule.
> 
> Actually, see
> 
>   http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10
> 
> Manuel

for those following along here:

| However, I think I now understand what you are worried about.  It is the
| interaction of type families and GHC's generalised type synonyms (i.e.,
| type synonyms that may be partially applied).  I agree that it does lead
| to an odd interaction, because the outcome may depend on the order in
| which the type checker performs various operations.  In particular,
| whether it first applies a type instance declaration to reduce a type
| family application or whether it first performs decomposition.

yes, indeed, thanks! that was the central point of example one.

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

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.

my suggestion was to annotate the results of type family application
reductions with the type parameters. in essence, that would carry
the phantom types along for type checking, and the decomposition
rule could be taken care of even after reduction, by comparing these 
annotations. alternatively, use the decomposition rule as the reduction
rule. both would make clear that one is *not* dealing with simple
type-level function applications.

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

but in terms of actually implementing your design, and matching
your theory and proofs, it might be best to treat the rhs of a type 
family instance like a type class instance parameter (where partial 
applications of synonyms and families are ruled out), not like the 
rhs of a type synonym definition (where everything is allowed).

then users can try out an implementation that does what you
say it would, including constraints needed for your proofs, which 
might lead to extension requests later - as Tom said, there may 
still be some open ends. perhaps you could keep those two 
examples around in a separate ticket, collecting experiences
with and limitations of type families?

thanks,
claus