RE: Injective type families?

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