Richard,
Thanks for your answers.
2013/6/24 Richard Eisenberg
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