Note [Use level numbers for quantification]

The level numbers assigned to metavariables are very useful. Not only
do they track touchability (Note [TcLevel invariants] in GHC.Tc.Utils.TcType),
but they also allow us to determine which variables to
generalise. The rule is this:

  When generalising, quantify only metavariables with a TcLevel greater
  than the ambient level.

This works because we bump the level every time we go inside a new
source-level construct. In a traditional generalisation algorithm, we
would gather all free variables that aren't free in an environment.
However, if a variable is in that environment, it will always have a lower
TcLevel: it came from an outer scope. So we can replace the "free in
environment" check with a level-number check.

Here is an example:

  f x = x + (z True)
    where
      z y = x * x

We start by saying (x :: alpha[1]). When inferring the type of z, we'll
quickly discover that z :: alpha[1]. But it would be disastrous to
generalise over alpha in the type of z. So we need to know that alpha
comes from an outer environment. By contrast, the type of y is beta[2],
and we are free to generalise over it. What's the difference between
alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
generalisation, and so we generalise it. alpha[1] does not, and so
we leave it alone.

Note that not *every* variable with a higher level will get
generalised, either due to the monomorphism restriction or other
quirks. See, for example, the code in GHC.Tc.Solver.decidePromotedTyVars
and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude
certain otherwise-eligible variables from being generalised.

Using level numbers for quantification is implemented in the candidateQTyVars...
functions, by adding only those variables with a level strictly higher than
the ambient level to the set of candidates.