Note [Levels for wildcards]
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
- GHC.Tc.Gen.HsType call site ×2
- Checking partial type signatures GHC.Tc.Gen.HsType