Note [ForAllTy]

A (ForAllTy (Bndr tcv vis) ty) can quantify over a TyVar or, less commonly, a CoVar.
See Note [Why ForAllTy can quantify over a coercion variable] for why we need the latter.

(FT1) Invariant: See Note [Weird typing rule for ForAllTy]

(FT2) Invariant: in (ForAllTy (Bndr tcv vis) ty),
      if tcv is a CoVar, then vis = coreTyLamForAllTyFlag.
   Visibility is not important for coercion abstractions,
   because they are not user-visible.

(FT3) Invariant: see Note [Unused coercion variable in ForAllTy]