| >> 1. Should this feature be placed behind a LANGUAGE pragma? | > | > 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. On a branch we are working on a fundep-like extension of injectivity, which is a rather bigger feature. Personally I think it might be better for there to be a LANGUAGE pragma to signal that we are using it (both the current r -> a form, and the new piece). Simon