Hi.
No, I don't think it should. I consider it a tiny addition to TypeFamilies that is not worth having its separate pragma. Injective TFs are fully backwards compatible, so no existing code will be broken.
That being said, it does claim new syntax and consequently would be rather difficult to back out if we realize that this implementation isn't the right direction. I don't have a strong opinion here, just playing devil's advocate.
I think it should be a new language extension. Forward compatibility on its own is not a sufficient argument. Aren't e.g. GADTs forward compatible? Or functional dependencies? Or flexible instances? Yet all of these also have separate language extensions. If I actually want to write backward-compatible type family code using GHC-8.0, I'd prefer to be able to enable TypeFamilies yet not InjectiveTypeFamilies, and have GHC check that I am in the common subset. Also, I think it would be nice to be able to track how many packages will make use of TypeFamilies and InjectiveTypeFamilies separately from each other. Cheers, Andres