Note [Why ForAllTy can quantify over a coercion variable]

The ForAllTyBinder in a ForAllTy can be (most often) a TyVar or (rarely)
a CoVar. We support quantifying over a CoVar here in order to support
a homogeneous (~#) relation (someday -- not yet implemented). Here is
the example:

  type (:~~:) :: forall k1 k2. k1 -> k2 -> Type
  data a :~~: b where
    HRefl :: a :~~: a

Assuming homogeneous equality (that is, with
  (~#) :: forall k. k -> k -> TYPE (TupleRep '[])
) after rejigging to make equalities explicit, we get a constructor that
looks like

  HRefl :: forall k1 k2 (a :: k1) (b :: k2).
           forall (cv :: k1 ~# k2). (a |> cv) ~# b
        => (:~~:) k1 k2 a b

Note that we must cast `a` by a cv bound in the same type in order to
make this work out.

See also https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell/phase2
which gives a general road map that covers this space.  Having this feature in
Core does *not* mean we have it in source Haskell.  See #15710 about that.