Re: Repeated variables in type family instances

Sure. Say you want a default type at any given kind. You could write something like this:

type family Default (a :: k) :: k type instance Default (a :: *) = () type instance Default (a :: * -> *) = [] type instance Default (a :: * -> * -> *) = (,) type instance Default (a :: * -> * -> * -> *) = (,,)

This isn't perhaps the most useful example, but it works. Richard On Jun 26, 2013, at 8:33 AM, Dominique Devriese wrote:

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