Note [Core type and coercion invariant]

We allow a /non-recursive/, /non-top-level/ let to bind type and
coercion variables.  These can be very convenient for postponing type
substitutions until the next run of the simplifier.

* A type variable binding must have a RHS of (Type ty)

* A coercion variable binding must have a RHS of (Coercion co)

  It is possible to have terms that return a coercion, but we use
  case-binding for those; e.g.
     case (eq_sel d) of (co :: a ~# b) -> blah
  where eq_sel :: (a~b) -> (a~#b)

  Or even
      case (df @Int) of (co :: a ~# b) -> blah
  Which is very exotic, and I think never encountered; but see
  Note [Equality superclasses in quantified constraints]
  in GHC.Tc.Solver.Dict