Note [Conflict checking for axiom applications]

Consider the following type family and axiom:

type family Equal (a :: k) (b :: k) :: Bool
type instance where
  Equal a a = True
  Equal a b = False

Equal :: forall k::*. k -> k -> Bool
axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
           ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }

The coercion (axEqual[1] <*> <Int> <Int) is ill-typed, and Lint should reject it.
(Recall that the index is 0-based, so this is the second branch of the axiom.)
The problem is that, on the surface, it seems that

  (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False)

and that all is OK. But, all is not OK: we want to use the first branch of the
axiom in this case, not the second. The problem is that the parameters of the
first branch can unify with the supplied coercions, thus meaning that the first
branch should be taken. See also Note [Apartness] in "GHC.Core.FamInstEnv".

For more details, see the section "Branched axiom conflict checking" in
docs/core-spec, which defines the corresponding no_conflict function used by the
Co_AxiomInstCo rule in the section "Coercion typing".