Note [Decomposing TyConApp equalities]

Suppose we have
        [G/W] T ty1 ~r T ty2
Can we decompose it, and replace it by
        [G/W] ty1 ~r' ty2
and if so what role is r'?  (In this Note, all the "~" are primitive
equalities "~#", but I have dropped the noisy "#" symbols.)  Lots of
background in the paper "Safe zero-cost coercions for Haskell".

This Note covers the topic for
  * Datatypes
  * Newtypes
  * Data families
For the rest:
  * Type synonyms: are always expanded
  * Type families: see Note [Decomposing type family applications]
  * AppTy:         see Note [Decomposing AppTy equalities].

Roles of the decomposed constraints ----
For a start, the role r' will always be defined like this:
  * If r=N then r' = N
  * If r=R then r' = role of T's first argument

For example:
   data TR a = MkTR a       -- Role of T's first arg is Representational
   data TN a = MkTN (F a)   -- Role of T's first arg is Nominal

The function tyConRolesX :: Role -> TyCon -> [Role] gets the argument
role r' for a TyCon T at role r.  E.g.
   tyConRolesX Nominal          TR = [Nominal]
   tyConRolesX Representational TR = [Representational]

Soundness and completeness ----
For Givens, for /soundness/ of decomposition we need, forall ty1,ty2:
    T ty1 ~r T ty2   ===>    ty1 ~r' ty2
Here "===>" means "implies".  That is, given evidence for (co1 : T ty1 ~r T co2)
we can produce evidence for (co2 : ty1 ~r' ty2).  But in the solver we
/replace/ co1 with co2 in the inert set, and we don't want to lose any proofs
thereby. So for /completeness/ of decomposition we also need the reverse:
    ty1 ~r' ty2   ===>    T ty1 ~r T ty2

For Wanteds, for /soundness/ of decomposition we need:
    ty1 ~r' ty2   ===>    T ty1 ~r T ty2
because if we do decompose we'll get evidence (co2 : ty1 ~r' ty2) and
from that we want to derive evidence (T co2 : T ty1 ~r T ty2).
For /completeness/ of decomposition we need the reverse implication too,
else we may decompose to a new proof obligation that is stronger than
the one we started with.  See Note [Decomposing newtype equalities].

Injectivity ----
When do these bi-implications hold? In one direction it is easy.
We /always/ have
    ty1 ~r'  ty2   ===>    T ty1 ~r T ty2
This is the CO_TYCONAPP rule of the paper (Fig 5); see also the
TyConAppCo case of GHC.Core.Lint.lintCoercion.

In the other direction, we have
    T ty1 ~r T ty2   ==>   ty1 ~r' ty2  if T is /injective at role r/
This is the very /definition/ of injectivity: injectivity means result
is the same => arguments are the same, modulo the role shift.
See comments on GHC.Core.TyCon.isInjectiveTyCon.  This is also
the CO_NTH rule in Fig 5 of the paper, except in the paper only
newtypes are non-injective at representation role, so the rule says
"H is not a newtype".

Injectivity is a bit subtle:
                 Nominal   Representational
   Datatype        YES        YES
   Newtype         YES        NO{1}
   Data family     YES        NO{2}

{1} Consider newtype N a = MkN (F a)   -- Arg has Nominal role
    Is it true that (N t1) ~R (N t2)   ==>   t1 ~N t2  ?
    No, absolutely not.  E.g.
       type instance F Int = Int; type instance F Bool = Char
       Then (N Int) ~R (N Bool), by unwrapping, but we don't want Int~Char!

    See Note [Decomposing newtype equalities]

{2} We must treat data families precisely like newtypes, because of the
    possibility of newtype instances. See also
    Note [Decomposing newtype equalities]. See #10534 and
    test case typecheck/should_fail/T10534.

Takeaway summary -----
For sound and complete decomposition, we simply need injectivity;
that is for isInjectiveTyCon to be true:

* At Nominal role, isInjectiveTyCon is True for all the TyCons we are
  considering in this Note: datatypes, newtypes, and data families.

* For Givens, injectivity is necessary for soundness; completeness has no
  side conditions.

* For Wanteds, soundness has no side conditions; but injectivity is needed
  for completeness. See Note [Decomposing newtype equalities]

This is implemented in `can_decompose` in `canTyConApp`; it looks at
injectivity, just as specified above.