Note [Levels for wildcards]

GHC/Tc/Gen/HsType.hs:4348 compiler

Consider
     f :: forall b. (forall a. a -> _) -> b
We do /not/ allow the "_" to be instantiated to 'a'; although we do
(as before) allow it to be instantiated to the (top level) 'b'.
Why not?  Suppose
   f x = (x True, x 'c')

During typecking the RHS we must instantiate that (forall a. a -> _),
so we must know /precisely/ where all the a's are; they must not be
hidden under (possibly-not-yet-filled-in) unification variables!

We achieve this as follows:

- For /named/ wildcards such sas
     g :: forall b. (forall la. a -> _x) -> b
  there is no problem: we create them at the outer level (ie the
  ambient level of the signature itself), and push the level when we
  go inside a forall.  So now the unification variable for the "_x"
  can't unify with skolem 'a'.

- For /anonymous/ wildcards, such as 'f' above, we carry the ambient
  level of the signature to the hole in the TcLevel part of the
  mode_holes field of TcTyMode.  Then, in tcAnonWildCardOcc we us that
  level (and /not/ the level ambient at the occurrence of "_") to
  create the unification variable for the wildcard.  That is the sole
  purpose of the TcLevel in the mode_holes field: to transport the
  ambient level of the signature down to the anonymous wildcard
  occurrences.

References 0

This Note does not link to any other.

Referenced by 3