With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:

data Nat = Zero | Succ a

class Add a b r | a b -> r, r a -> b
instance                Add Zero     b b
instance (Add a b r) => Add (Succ a) b (Succ r)

Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:

type family AddTF a b = r | r a -> b where
     AddTF Zero     b = b
     AddTF (Succ a) b = Succ (AddTF a b)

But we want to be able to say that.