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

Consider (typecheck/should_compile/tc231), where we're trying to infer
the type of a top-level declaration. We have
  class Zork s a b | a -> b
and the candidate constraint at the end of simplifyInfer is
  [W] Zork alpha[1] (Z [Char]) beta[1]
We definitely want to quantify over `alpha` (which is mentioned in the
tau-type).

But we do *not* want to quantify over `beta`: it is determined by the
functional dependency on Zork: note that the second argument to Zork
in the Wanted is a variable-free `Z [Char]`.  Quantifying over it
would be "Henry Ford polymorphism".  (Presumably we don't have an
instance in scope that tells us what `beta` actually is.)  Instead
we promote `beta[1]` to `beta[0]`, in `decidePromotedTyVars`.

The question here: do we want to quantify over the constraint, to
give the type
   forall a. Zork a (Z [Char]) beta[0] => blah
Definitely not: see Note [The top-level Any principle]

What we really want (to catch the Zork example) is this:

   Quantify over the constraint only if all its free variables are
   (a) quantified, or
   (b) appears in the type of something in the environment (mono_tvs0).

To understand (b) consider

  class C a b where { op :: a -> b -> () }

  mr = 3                      -- mr :: alpha
  f1 x = op x mr              -- f1 :: forall b. b -> (), plus [W] C b alpha
  intify = mr + (4 :: Int)

In `f1` should we quantify over that `(C b alpha)`?  Answer: since `alpha` is
free in the type envt, yes we should.  After all, if we'd typechecked `intify`
first, we'd have set `alpha := Int`, and /then/ we'd certainly quantify.  The
delicate Zork situation applies when beta is completely unconstrained (not free
in the environment) -- except by the fundep.  Hence `newly_mono`.

Another way to put it: let's say `alpha` is in `outer_tvs`. It must be that
some variable `x` has `alpha` free in its type. If we are at top-level (and we
are, because nested decls don't go through this path all), then `x` must also
be at top-level. And, by induction, `x` will not have Any in its type when all
is said and done. The induction is well-founded because, if `x` is mutually
recursive with the definition at hand, then their constraints get processed
together (or `x` has a type signature, in which case the type doesn't have
`Any`). So the key thing is that we must not introduce a new top-level
unconstrained variable here.

However this regrettably-subtle reasoning is needed only for /top-level/
declarations.  For /nested/ decls we can see all the calls, so we'll instantiate
that quantifed `Zork a (Z [Char]) beta` constraint at call sites, and either
solve it or not (probably not).  We won't be left with a still-callable function
with Any in its type.  So for nested definitions we don't make this tricky test.

Historical note: we had a different, and more complicated test before, but it
was utterly wrong: #23199.