Note [Deciding quantification]
If the monomorphism restriction does not apply, then we quantify as follows:
* Step 1: decidePromotedTyVars.
Take the global tyvars, and "grow" them using functional dependencies
E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
happen because alpha is untouchable here) then do not quantify over
beta, because alpha fixes beta, and beta is effectively free in
the environment too; this logic extends to general fundeps, not
just equalities
We also account for the monomorphism restriction; if it applies,
add the free vars of all the constraints.
Result is mono_tvs; we will promote all of these to the outer levek,
and certainly not quantify over them.
* Step 2: defaultTyVarsAndSimplify.
Default any non-promoted tyvars (i.e ones that are definitely
not going to become further constrained), and re-simplify the
candidate constraints.
Motivation for re-simplification (#7857): imagine we have a
constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
not free in the envt, and instance forall (a::*) (b::*). (C a) => C
(a -> b) The instance doesn't match while l1,l2 are polymorphic, but
it will match when we default them to LiftedRep.
This is all very tiresome.
This step also promotes the mono_tvs from Step 1. See
Note [Promote monomorphic tyvars]. In fact, the *only*
use of the mono_tvs from Step 1 is to promote them here.
This promotion effectively stops us from quantifying over them
later, in Step 3. Because the actual variables to quantify
over are determined in Step 3 (not in Step 1), it is OK for
the mono_tvs to be missing some variables free in the
environment. This is why removing the psig_qtvs is OK in
decidePromotedTyVars. Test case for this scenario: T14479.
* Step 3: decideQuantifiedTyVars.
Decide which variables to quantify over, as follows:
- Take the free vars of the partial-type-signature types and constraints,
and the tau-type (zonked_tau_tvs), and then "grow"
them using all the constraints. These are grown_tcvs.
See Note [growThetaTyVars vs closeWrtFunDeps].
- Use quantifyTyVars to quantify over the free variables of all the types
involved, but only those in the grown_tcvs.
Result is qtvs.
* Step 4: Filter the constraints using pickQuantifiablePreds and the
qtvs. We have to zonk the constraints first, so they "see" the
freshly created skolems. References 2
- growThetaTyVars vs closeWrtFunDeps GHC.Tc.Solver
- Promote monomorphic tyvars GHC.Tc.Solver
Referenced by 2
- GHC.Tc.Solver call site ×2