Is there a way to declare a type family to be injective?

I have

> data Z
> data S n

> type family n :+: m
> type instance Z   :+: m = m
> type instance S n :+: m = S (n :+: m)

My intent is that (:+:) really is injective in each argument (holding the other as fixed), but I don't know how to persuade GHC, leading to some compilation errors like the following:

    Couldn't match expected type `m :+: n'
           against inferred type `m :+: n1'
      NB: `:+:' is a type function, and may not be injective

I realize that someone could add more type instances for (:+:), breaking injectivity.

Come to think of it, I don't know how GHC could even figure out that the two instances above do not overlap on the right-hand sides.

Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue?

Thanks, - Conal