Injective type families

Hi Jan, A few questions came up this morning while speaking Andres Loeh about injective type families: 1. Should this feature be placed behind a LANGUAGE pragma? Afterall, functional dependencies feel very similar and in this case we require a pragma. Now would be the last opportunity to change this. 2. Could you perhaps add some text to better motivate the feature in the users guide? Referring to the paper for the details of semantics of the feature and its implementation is fine, but expecting a new user to refer to the paper to even know *why* they might want to use it seems a bit unfriendly. Thanks! Cheers, - Ben