Note [Rewriting]

  rewrite ty  ==>  Reduction co xi
    where
      xi has no reducible type functions
         has no skolems that are mapped in the inert set
         has no filled-in metavariables
      co :: ty ~ xi (coercions in reductions are always left-to-right)

Key invariants:
  (F0) co :: zonk(ty') ~ xi   where zonk(ty') ~ zonk(ty)
  (F1) typeKind(xi) succeeds and returns a fully zonked kind
  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))

Note that it is rewrite's job to try to reduce *every type function it sees*.

Rewriting also:
  * zonks, removing any metavariables, and
  * applies the substitution embodied in the inert set

Because rewriting zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
we can rely on this fact:

  (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)

Note that the right-hand type of co is *always* precisely xi. The left-hand
type may or may not be ty, however: if ty has unzonked filled-in metavariables,
then the left-hand type of co will be the zonk-equal to ty.
It is for this reason that we occasionally have to explicitly zonk,
when (co :: ty ~ xi) is important even before we zonk the whole program.
For example, see the RTRNotFollowed case in rewriteTyVar.

Why have these invariants on rewriting? Because we sometimes use typeKind
during canonicalisation, and we want this kind to be zonked (e.g., see
GHC.Tc.Solver.Equality.canEqCanLHS).

Rewriting is always homogeneous. That is, the kind of the result of rewriting is
always the same as the kind of the input, modulo zonking. More formally:

  (F2) zonk(typeKind(ty)) `eqType` typeKind(xi)

This invariant means that the kind of a rewritten type might not itself be rewritten.

Note that we prefer to leave type synonyms unexpanded when possible,
so when the rewriter encounters one, it first asks whether its
transitive expansion contains any type function applications or is
forgetful -- that is, omits one or more type variables in its RHS.  If so,
it expands the synonym and proceeds; if not, it simply returns the
unexpanded synonym. See also Note [Rewriting synonyms].

Where do we actually perform rewriting within a type? See Note [Rewritable] in
GHC.Tc.Solver.InertSet.