Note [Decomposing AppTy equalities]

For AppTy all the same questions arise as in
Note [Decomposing TyConApp equalities]. We have

    s1 ~r s2,  t1 ~N t2   ==>   s1 t1 ~r s2 t2       (rule CO_APP)
    s1 t1 ~N s2 t2        ==>   s1 ~N s2,  t1 ~N t2  (CO_LEFT, CO_RIGHT)

In the first of these, why do we need Nominal equality in (t1 ~N t2)?
See {2} below.

For sound and complete solving, we need both directions to decompose. So:
* At nominal role, all is well: we have both directions.
* At representational role, decomposition of Givens is unsound (see {1} below),
  and decomposition of Wanteds is incomplete.

Here is an example of the incompleteness for Wanteds:

    [G] g1 :: a ~R b
    [W] w1 :: Maybe b ~R alpha a
    [W] w2 :: alpha ~N Maybe

Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get

    w1 := AppCo w3 w4
    [W] w3 :: Maybe ~R alpha
    [W] w4 :: b ~N a

Note that w4 is *nominal*. A nominal role here is necessary because AppCo
requires a nominal role on its second argument. (See {2} for an example of
why.) Now we are stuck, because w4 is insoluble. On the other hand, if we
see w2 first, setting alpha := Maybe, all is well, as we can decompose
Maybe b ~R Maybe a into b ~R a.

Another example:
    newtype Phant x = MkPhant Int
    [W] w1 :: Phant Int ~R alpha Bool
    [W] w2 :: alpha ~ Phant

If we see w1 first, decomposing would be disastrous, as we would then try
to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
    [W] w1' :: Phant Int ~R Phant Bool

which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
and all will be well. See also Note [Unwrap newtypes first].

Bottom line:
* Always decompose AppTy at nominal role: can_eq_app
* Never decompose AppTy at representational role (neither Given nor Wanted):
  the lack of an equation in can_eq_nc

Extra points
{1}  Decomposing a Given AppTy over a representational role is simply
     unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
     the newtype Phant, above), then we surely don't want any relationship
     between Int and Bool, lest we also have co2 :: Phant ~ a around.

{2} The role on the AppCo coercion is a conservative choice, because we don't
    know the role signature of the function. For example, let's assume we could
    have a representational role on the second argument of AppCo. Then, consider

    data G a where    -- G will have a nominal role, as G is a GADT
      MkG :: G Int
    newtype Age = MkAge Int

    co1 :: G ~R a        -- by assumption
    co2 :: Age ~R Int    -- by newtype axiom
    co3 = AppCo co1 co2 :: G Age ~R a Int    -- by our broken AppCo

    and now co3 can be used to cast MkG to have type G Age, in violation of
    the way GADTs are supposed to work (which is to use nominal equality).