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.
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
To flicky frans: 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