Note [Verifying injectivity annotation]

Injectivity means that the RHS of a type family uniquely determines the LHS (see
Note [Type inference for type families with injectivity]).  The user informs us about
injectivity using an injectivity annotation and it is GHC's task to verify that
this annotation is correct w.r.t. type family equations. Whenever we see a new
equation of a type family we need to make sure that adding this equation to the
already known equations of a type family does not violate the injectivity annotation
supplied by the user (see Note [Injectivity annotation]).  Of course if the type
family has no injectivity annotation then no check is required.  But if a type
family has injectivity annotation we need to make sure that the following
conditions hold:

1. For each pair of *different* equations of a type family, one of the following
   conditions holds:

   A:  RHSs are different. (Check done in GHC.Core.FamInstEnv.injectiveBranches)

   B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
       then it must be possible to unify the LHSs under the same substitution.
       Example:

          type family FunnyId a = r | r -> a
          type instance FunnyId Int = Int
          type instance FunnyId a = a

       RHSs of these two equations unify under [ a |-> Int ] substitution.
       Under this substitution LHSs are equal therefore these equations don't
       violate injectivity annotation. (Check done in GHC.Core.FamInstEnv.injectiveBranches)

   B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
       substitution then either the LHSs unify under the same substitution or
       the LHS of the latter equation is overlapped by earlier equations.
       Example 1:

          type family SwapIntChar a = r | r -> a where
              SwapIntChar Int  = Char
              SwapIntChar Char = Int
              SwapIntChar a    = a

       Say we are checking the last two equations. RHSs unify under [ a |->
       Int ] substitution but LHSs don't. So we apply the substitution to LHS
       of last equation and check whether it is overlapped by any of previous
       equations. Since it is overlapped by the first equation we conclude
       that pair of last two equations does not violate injectivity
       annotation. (Check done in GHC.Tc.Validity.checkValidCoAxiom#gather_conflicts)

   A special case of B is when RHSs unify with an empty substitution ie. they
   are identical.

   If any of the above two conditions holds we conclude that the pair of
   equations does not violate injectivity annotation. But if we find a pair
   of equations where neither of the above holds we report that this pair
   violates injectivity annotation because for a given RHS we don't have a
   unique LHS. (Note that (B) actually implies (A).)

   Note that we only take into account these LHS patterns that were declared
   as injective.

2. If an RHS of a type family equation is a bare type variable then
   all LHS variables (including implicit kind variables) also have to be bare.
   In other words, this has to be a sole equation of that type family and it has
   to cover all possible patterns.  So for example this definition will be
   rejected:

      type family W1 a = r | r -> a
      type instance W1 [a] = a

   If it were accepted we could call `W1 [W1 Int]`, which would reduce to
   `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
   which is bogus. Checked FamInst.bareTvInRHSViolated.

3. If the RHS of a type family equation is a type family application then the type
   family is rejected as not injective. This is checked by FamInst.isTFHeaded.

4. If a LHS type variable that is declared as injective is not mentioned in an
   injective position in the RHS then the type family is rejected as not
   injective.  "Injective position" means either an argument to a type
   constructor or argument to a type family on injective position.
   There are subtleties here. See Note [Coverage condition for injective type families]
   in GHC.Tc.Instance.Family.

Check (1) must be done for all family instances (transitively) imported. Other
checks (2-4) should be done just for locally written equations, as they are checks
involving just a single equation, not about interactions. Doing the other checks for
imported equations led to #17405, as the behavior of check (4) depends on
-XUndecidableInstances (see Note [Coverage condition for injective type families] in
FamInst), which may vary between modules.

See also Note [Injective type families] in GHC.Core.TyCon