Note [Naughty quantification candidates]
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
- Recipe for checking a signature GHC.Tc.Gen.HsType
- Error on unconstrained meta-variables GHC.Tc.Utils.TcMType
Referenced by 11
- GHC.Tc.Utils.TcMType call site ×6
- Kind generalisation GHC.Tc.Gen.HsType
- GHC.Tc.Gen.Sig call site
- Generalising in tcTyFamInstEqnGuts GHC.Tc.TyCl
- GHC.Tc.TyCl.PatSyn call site
- Error on unconstrained meta-variables GHC.Tc.Utils.TcMType