Note [Unused coercion variable in ForAllTy]

Suppose we have
  \(co:t1 ~# t2). e

What type should we give to the above expression?
  (1) forall (co:t1 ~# t2) -> t
  (2) (t1 ~# t2) -> t

If co is used in t, (1) should be the right choice.
if co is not used in t, we would like to have (1) and (2) equivalent.

However, we want to keep eqType simple and don't want eqType (1) (2) to return
True in any case.

We decide to always construct (2) if co is not used in t.

Thus in mkLamType, we check whether the variable is a coercion
variable (of type (t1 ~# t2), and whether it is un-used in the
body. If so, it returns a FunTy instead of a ForAllTy.

There are cases we want to skip the check. For example, the check is
unnecessary when it is known from the context that the input variable
is a type variable.  In those cases, we use mkForAllTy.