Note [Rewritable]

Definition. A CanEqLHS lhs is *rewritable* in a type t if the
lhs tree appears as a subtree within t without traversing any of the following
components of t:
  * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
  * kinds of variable occurrences
The check for rewritability *does* look in kinds of the bound variable of a
ForAllTy.

The reason for this definition is that the rewriter does not rewrite in coercions
or variables' kinds. In turn, the rewriter does not need to rewrite there because
those places are never used for controlling the behaviour of the solver: these
places are not used in matching instances or in decomposing equalities.

This definition is used by the anyRewritableXXX family of functions and is meant
to model the actual behaviour in GHC.Tc.Solver.Rewrite.

Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
for all f.

Wrinkles

* Taking roles into account: we must consider a rewrite at a given role. That is,
  a rewrite arises from some equality, and that equality has a role associated
  with it. As we traverse a type, we track what role we are allowed to rewrite with.

  For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
  Maybe b but not in F b, where F is a type function. This role-aware logic is
  present in both the anyRewritableXXX functions and in the rewriter.
  See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.

* There is one exception to the claim that non-rewritable parts of the tree do
  not affect the solver: we sometimes do an occurs-check to decide e.g. how to
  orient an equality. (See the comments on GHC.Tc.Solver.Equality.canEqTyVarFunEq.)
  Accordingly, the presence of a variable in a kind or coercion just might
  influence the solver. Here is an example:

    type family Const x y where
      Const x y = x

    AxConst :: forall x y. Const x y ~# x

    alpha :: Const Type Nat
    [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
                        AxConst Type alpha ;;
                        sym (AxConst Type Nat))

  The cast is clearly ludicrous (it ties together a cast and its symmetric
  version), but we can't quite rule it out. (See (EQ1) from Note [Respecting
  definitional equality] in GHC.Core.TyCo.Rep to see why we need the Const Type
  Nat bit.) And yet this cast will (quite rightly) prevent alpha from unifying
  with the RHS. I (Richard E) don't have an example of where this problem can
  arise from a Haskell program, but we don't have an air-tight argument for why
  the definition of *rewritable* given here is correct.