Repeated variables in type family instances

[Dominique Devriese]

Richard,

Thanks for your answers.

2013/6/24 Richard Eisenberg <eir at cis.upenn.edu>:
>
> The nub of the difference is that type families can pattern-match on kinds,
> whereas term-level functions cannot pattern-match on types. So, while the @a
> is repeated in the pattern as written above, GHC does not, when matching a
> pattern, check that these are the same. In fact, they have to be the same if
> the function argument is well-typed. On the other hand, type family
> equations *can* branch based solely on kind information, making the repeated
> variable semantically important.

Interesting,  I wasn't aware this was possible.  I agree that if it's
possible to branch solely on kind info, then they should be taken into
account for the linearity check. Do you perhaps have an example of how
to do this sort of branching?

Thanks,
Dominique