Note [checkTyEqRhs]

The key function `checkTyEqRhs ty_eq_flags rhs` is called on the
RHS of a type equality
       lhs ~ rhs
and checks to see if `rhs` satisfies, or can be made to satisfy,
invariants described by `ty_eq_flags`.  It can succeded or fail; in
the latter case it returns a `CheckTyEqResult` that describes why it
failed.

When `lhs` is a touchable type variable, so unification might happen, then
`checkTyEqRhs` enforces the unification preconditions of Note [Unification preconditions].

Notably, it can check for things like:
  * Insoluble occurs check
      e.g.  alpha[tau] ~ [alpha]
       or   F Int      ~ [F Int]
  * Potentially-soluble occurs check
      e.g.  alpha[tau] ~ [F alpha beta]
  * Impredicativity error:
      e.g.  alpha[tau] ~ (forall a. a->a)
  * Skolem escape
      e.g  alpha[1] ~ (b[sk:2], Int)
  * Concreteness error
      e.g. alpha[conc] ~ r[sk]

Its specific behaviour is governed by the `TyEqFlags` that are passed
to it; see Note [TyEqFlags].

Note, however, that `checkTyEqRhs` specifically does /not/ check for:
  * Touchability of the LHS (in the case of a unification variable)
  * Shape of the LHS (e.g. we can't unify Int with a TyVarTv)
These things are checked by `simpleUnifyCheck`.