shouldn't the check go the other way?  (i.e., if the RHSs unify, then the LHS must be the same).  Here is an example:

-- This function is not injective.

type instance F a = Int

type instance F b = Int

Yes, you’re right.

Still, Conal's example would not work if we just added support for injective type functions because + is not injective (e.g., 2 + 3 = 1 + 4).  Instead, what we'd need to say is that it is injective in each argument separately, which would basically amount to adding functional dependencies to type functions.  Perhaps something like this:

type family (a :+: b) ~ c | c b -> a, c a -> b

Interesting!  Injectivity is more complicated than one might think! 

Simon