Note [Naughty quantification candidates]

GHC/Tc/Utils/TcMType.hs:1235 compiler 2 tickets

Consider (#14880, dependent/should_compile/T14880-2), suppose
we are trying to generalise this type:

  forall arg. ... (alpha[tau]:arg) ...

We have a metavariable alpha whose kind mentions a skolem variable
bound inside the very type we are generalising.
This can arise while type-checking a user-written type signature
(see the test case for the full code).

We cannot generalise over alpha!  That would produce a type like
  forall {a :: arg}. forall arg. ...blah...
The fact that alpha's kind mentions arg renders it completely
ineligible for generalisation.

However, we are not going to learn any new constraints on alpha,
because its kind isn't even in scope in the outer context (but see Wrinkle).
So alpha is entirely unconstrained.

What then should we do with alpha?  During generalization, every
metavariable is either (A) promoted, (B) generalized, or (C) zapped
(according to Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType).

 * We can't generalise it.
 * We can't promote it, because its kind prevents that
 * We can't simply leave it be, because this type is about to
   go into the typing environment (as the type of some let-bound
   variable, say), and then chaos erupts when we try to instantiate.

Previously, we zapped it to Any. This worked, but it had the unfortunate
effect of causing Any sometimes to appear in error messages. If this
kind of signature happens, the user probably has made a mistake -- no
one really wants Any in their types. So we now error. This must be
a hard error (failure in the monad) to avoid other messages from mentioning
Any.

We do this eager erroring in candidateQTyVars, which always precedes
generalisation, because at that moment we have a clear picture of what
skolems are in scope within the type itself (e.g. that 'forall arg').

This change is inspired by and described in Section 7.2 of "Kind Inference
for Datatypes", POPL'20.

NB: this is all rather similar to, but sadly not the same as
    Note [Error on unconstrained meta-variables]

Wrinkle:

We must make absolutely sure that alpha indeed is not from an outer
context. (Otherwise, we might indeed learn more information about it.)
This can be done easily: we just check alpha's TcLevel.  That level
must be strictly greater than the ambient TcLevel in order to treat it
as naughty. We say "strictly greater than" because the call to
candidateQTyVars is made outside the bumped TcLevel, as stated in the
comment to candidateQTyVarsOfType. The level check is done in go_tv in
collect_cand_qtvs. Skipping this check caused #16517.

References 2

Referenced by 11