Repeated variables in type family instances

[Richard Eisenberg]

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