Note [Renaming injectivity annotation]

During renaming of injectivity annotation we have to make several checks to
make sure that it is well-formed.  At the moment injectivity annotation
consists of a single injectivity condition, so the terms "injectivity
annotation" and "injectivity condition" might be used interchangeably.  See
Note [Injectivity annotation] for a detailed discussion of currently allowed
injectivity annotations.

Checking LHS is simple because the only type variable allowed on the LHS of
injectivity condition is the variable naming the result in type family head.
Example of disallowed annotation:

    type family Foo a b = r | b -> a

Verifying RHS of injectivity consists of checking that:

 1. only variables defined in type family head appear on the RHS (kind
    variables are also allowed).  Example of disallowed annotation:

       type family Foo a = r | r -> b

 2. for associated types the result variable does not shadow any of type
    class variables. Example of disallowed annotation:

       class Foo a b where
          type F a = b | b -> a

Breaking any of these assumptions results in an error.