[Haskell-cafe] Injective type families for GHC - syntax proposals

[Jan Stolarek]

Thank you all for replies.

To Carter:
> what about adding some annotation to the args that act injectively wrt the result?
I'm afraid that's not enough. How would you annotate Plus using this syntax?

type family Plus a b | Plus a -> b, Plus b -> a where ...

> Or should we actually think of the solver process as being analagous to fundeps?
I think that injectivity will be very similar to fundeps: you'll have some types determining the 
others, except for type families not type classes.

To flicky frans:
> Maybe it's worth adding an explicit type variable for the result?
Oh, this sounds good. But we must remember that type families already allow providing the kind of 
the result like this:

   type family Id a :: * where
   type family G a b c :: * where
   type family Plus a b :: Nat where

So we'd have to do this:

   type family Id a :: (r :: *) | r -> a where
   type family G a b c :: (res :: *) | res -> a b where
   type family Plus a b :: (result :: Nat) | result a -> b, result b -> a where

This would effectively force the user to provide kind annotation for the result but that doesn't 
seem to be a high price to pay.

To Jason:
> I have some code that currently needs AllowAmbiguousTypes to compile in
> 7.8, but didn't need it in 7.6. It's actually an example of your form of
> injectivity C.
I took the liberty of reporting this as a GHC bug: #9607. However, I don't see how injectivity 
would help here. I of course see that '++ is injective in the same way as Plus but I don't see 
how this would aid in type checking of rightUnit (especially that it used to work!). The error 
message mentions injectivity but that doesn't mean that injectivity would really help.

Janek