Note [decideAndPromoteTyVars]

We are about to generalise a let-binding at "outer level" N, where we have
typechecked its RHS at "rhs level" N+1.  Each tyvar must be either
  (P) promoted
  (D) defaulted
  (Q) quantified
The function `decideAndPromoteTyVars` figures out (P), the type variables
mentioned in constraints should definitely not be quantified, and promotes them
to the outer level, namely N.

The plan

* Step 1.  Use `approximateWCX` to extract, from the RHS `WantedConstraints`,
  the PredTypes that we might quantify over; and also those that we can't.
  Example: suppose the `wanted` is this:
     (d1:Eq alpha, forall b. (F b ~ a) => (co:t1 ~ t2), (d:Show alpha))
  Then
     can_quant = [Eq alpha, Show alpha]
     no_quant  = (t1 ~ t2)
  We can't quantify over that (t1~t2) because of the enclosing equality (F b ~ a).

  We also choose never to quantify over some forms of equality constraints.
  Both this and the "given-equality" thing are described in
  Note [Quantifying over equality constraints] in GHC.Tc.Types.Constraint.

* Step 2. Further trim can_quant using the Monomorphism Restriction, yielding the
  further `mr_no_quant` predicates that we won't quantify over; plus `post_mr_quant`,
  which we can in principle quantify.

* Step 3. Identify the type variables we definitely won't quantify, because they are:
  a) From an outer level <=N anyway
  b) Mentioned in a constraint we /can't/ quantify.  See Wrinkle (DP1).
  c) Mentioned in the kind of a CoVar; we can't quantify over a CoVar,
     so we must not quantify over a type variable free in its kind
  d) Mentioned in a constraint that the MR says we should not quantify.

  There is a special case for top-level bindings: see Wrinkle (DP2).

* Step 4.  Close wrt functional dependencies and equalities.Example
  Example
           f x y = ...
              where z = x 3
  The body of z tries to unify the type of x (call it alpha[1]) with
  (beta[2] -> gamma[2]). This unification fails because alpha is untouchable, leaving
       [W] alpha[1] ~ (beta[2] -> gamma[2])
  We don't want to quantify over beta or gamma because they are fixed by alpha,
  which is monomorphic. Actual test case:   typecheck/should_compile/tc213

  Another example. Suppose we have
      class C a b | a -> b
  and a constraint ([W] C alpha beta), if we promote alpha we should promote beta.

  See also Note [growThetaTyVars vs closeWrtFunDeps]

* Step 5. Further restrict the quantifiable constraints `post_mr_quant` to ones
  that do not mention a "newly mono" tyvar. The "newly-mono" tyvars are the ones
  not free in the envt, nor forced to be promoted by the MR; but are determined
  (via fundeps) by them. Example:
           class C a b | a -> b
           [W] C Int beta[1],  tau = beta[1]->Int
  We promote beta[1] to beta[0] since it is determined by fundep, but we do not
  want to generate f :: (C Int beta[0]) => beta[0] -> Int Rather, we generate
  f :: beta[0] -> Int, but leave [W] C Int beta[0] in the residual constraints,
  which will probably cause a type error

  See Note [Do not quantify over constraints that determine a variable]

* Step 6: actually promote the type variables we don't want to quantify.
  We must do this: see Note [Promote monomorphic tyvars].

We also add a warning that signals when the MR "bites".

Wrinkles

(DP1) In step 3, why (b)?  Consider the example given in Step 1.  we can't
  quantify over the constraint (t1~t2).  But if we quantify over the /tyvars/ in
  t1 or t2, we may simply make that constraint insoluble (#25266 was an example).

(DP2) In Step 3, for top-level bindings, we do (a,d), but /not/ (b,c). Reason:
  see Note [The top-level Any principle].  At top level we are very reluctant to
  promote type variables.  But for bindings affected by the MR we have no choice
  but to promote.

  An example is in #26004.
      f w e = case e of
        T1 -> let y = not w in False
        T2 -> True
  When generalising `f` we have a constraint
      forall. (a ~ Bool) => alpha ~ Bool
  where our provisional type for `f` is `f :: T alpha -> blah`.
  In a /nested/ setting, we might simply not-generalise `f`, hoping to learn
  about `alpha` from f's call sites (test T5266b is an example).  But at top
  level, to avoid spooky action at a distance.