Note [simplifyArgsWorker]

Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
rewriting is homogeneous.
This causes some trouble when rewriting a function applied to a telescope
of arguments, perhaps with dependency. For example, suppose

  type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]

and we wish to rewrite the args of (with kind applications explicit)

  F @a @b (Just @a c) (Right @a @b d) False

where all variables are skolems and

  a :: Type
  b :: Type
  c :: a
  d :: b

  [G] aco :: a ~ fa
  [G] bco :: b ~ fb
  [G] cco :: c ~ fc
  [G] dco :: d ~ fd

The first step is to rewrite all the arguments. This is done before calling
simplifyArgsWorker. We start from

  a
  b
  Just @a c
  Right @a @b d
  False

and get left-to-right reductions whose coercions are as follows:

  co1 :: a ~ fa
  co2 :: b ~ fb
  co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6)
  co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7)
  co5 :: False ~ False

where
  co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a
  co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b

We now process the rewritten args in left-to-right order. The first two args
need no further processing. But now consider the third argument. Let f3 = the rewritten
result, Just fa (fc |> aco) |> co6.
This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (F2).
And yet, when we build the application (F @fa @fb ...), we need this
argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
The coercion to use is determined by the kind of F:
we see in F's kind that the third argument has kind Maybe j.
Critically, we also know that the argument corresponding to j
(in our example, a) rewrote with a coercion co1. We can thus know the
coercion needed for the 3rd argument is (Maybe co1), thus building
(f3 |> Maybe co1)

More generally, we must use the Lifting Lemma, as implemented in
Coercion.liftCoSubst. As we work left-to-right, any variable that is a
dependent parameter (j and k, in our example) gets mapped in a lifting context
to the coercion that is output from rewriting the corresponding argument (co1
and co2, in our example). Then, after rewriting later arguments, we lift the
kind of these arguments in the lifting context that we've be building up.
This coercion is then used to keep the result of rewriting well-kinded.

Working through our example, this is what happens:

  1. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
     because the binder associated with the first argument has a closed type (no
     variables).

  2. Extend the LC with [k |-> co2]. No casting to do.

  3. Lifting the kind (Maybe j) with our LC
     yields co8 :: Maybe a ~ Maybe fa. Use (f3 |> co8) as the argument to F.

  4. Lifting the kind (Either j k) with our LC
     yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th
     argument to F, where f4 is the rewritten form of argument 4, written above.

  5. We lift Bool with our LC, getting <Bool>; casting has no effect.

We're now almost done, but the new application

  F @fa @fb (f3 |> co8) (f4 |> co9) False

has the wrong kind. Its kind is [fb], instead of the original [b].
So we must use our LC one last time to lift the result kind [k],
getting res_co :: [fb] ~ [b], and we cast our result.

Accordingly, the final result is

  F
    @fa
    @fb
    (Just @fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
    (Right @fa @fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
    False
  |> [sym bco]

The res_co (in this case, [sym bco]) is the third component of the
tuple returned by simplifyArgsWorker.