Note [Kinding rules for types]

GHC/Core/Type.hs:2600 compiler

Here are the key kinding rules for types

          torc1 is TYPE or CONSTRAINT
          torc2 is TYPE or CONSTRAINT
          t1 : torc1 rep1
          t2 : torc2 rep2
   (FUN)  ----------------
          t1 -> t2 : torc2 LiftedRep
          In fact the arrow varies with torc1/torc2
          See Note [Function type constructors and FunTy]
          in GHC.Builtin.Types.Prim

          torc is TYPE or CONSTRAINT
          ty : body_torc rep
          ki : Type
          `a` is a type variable
          `a` is not free in rep
(FORALL1) -----------------------
          forall (a::ki). ty : body_torc rep

          torc is TYPE or CONSTRAINT
          ty : body_torc rep
          `c` is a coercion variable
          `c` is not free in rep
          `c` is free in ty       -- Surprise 1!
(FORALL2) -------------------------
          forall (cv::k1 ~#{N,R} k2). ty : body_torc LiftedRep
                                           Surprise 2!

Note that:
* (FORALL1) rejects (forall (a::Maybe). blah)

* (FORALL2) Surprise 1:
  See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]

* (FORALL2) Surprise 2: coercion abstractions are not erased, so
  this must be LiftedRep, just like (FUN).  (FORALL2) is just a
  dependent form of (FUN).

References 2

Referenced by 1