diff options
Diffstat (limited to 'compiler/typecheck/TcMType.hs')
| -rw-r--r-- | compiler/typecheck/TcMType.hs | 293 |
1 files changed, 149 insertions, 144 deletions
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 2953a466ad..a0297c61f5 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -69,9 +69,9 @@ module TcMType ( zonkTyCoVarsAndFVList, candidateQTyVarsOfType, candidateQTyVarsOfKind, candidateQTyVarsOfTypes, candidateQTyVarsOfKinds, - CandidatesQTvs(..), delCandidates, candidateKindVars, + CandidatesQTvs(..), delCandidates, candidateKindVars, partitionCandidates, zonkAndSkolemise, skolemiseQuantifiedTyVar, - defaultTyVar, quantifyTyVars, + defaultTyVar, quantifyTyVars, isQuantifiableTv, zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, @@ -79,7 +79,6 @@ module TcMType ( zonkId, zonkCoVar, zonkCt, zonkSkolemInfo, - tcGetGlobalTyCoVars, skolemiseUnboundMetaTyVar, ------------------------------ @@ -1029,14 +1028,17 @@ quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds we default the kind variables to *. So, to support this defaulting, and only for that reason, when -collecting the free vars of a type, prior to quantifying, we must keep -the type and kind variables separate. +collecting the free vars of a type (in candidateQTyVarsOfType and friends), +prior to quantifying, we must keep the type and kind variables separate. But what does that mean in a system where kind variables /are/ type variables? It's a fairly arbitrary distinction based on how the variables appear: - "Kind variables" appear in the kind of some other free variable + or in the kind of a locally quantified type variable + (forall (a :: kappa). ...) or in the kind of a coercion + (a |> (co :: kappa1 ~ kappa2)). These are the ones we default to * if -XPolyKinds is off @@ -1136,7 +1138,7 @@ 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_cant_qtvs. Skipping this check caused #16517. +in collect_cand_qtvs. Skipping this check caused #16517. -} @@ -1146,10 +1148,17 @@ data CandidatesQTvs -- -- Invariants: -- * All variables are fully zonked, including their kinds + -- * All variables are at a level greater than the ambient level + -- See Note [Use level numbers for quantification] -- -- This *can* contain skolems. For example, in `data X k :: k -> Type` -- we need to know that the k is a dependent variable. This is done - -- by collecting the candidates in the kind. + -- by collecting the candidates in the kind after skolemising. It also + -- comes up when generalizing a associated type instance, where instance + -- variables are skolems. (Recall that associated type instances are generalized + -- independently from their enclosing class instance, and the associated + -- type instance may be generalized by more, fewer, or different variables + -- than the class instance.) -- = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) @@ -1159,9 +1168,8 @@ data CandidatesQTvs -- See Note [Dependent type variables] , dv_cvs :: CoVarSet - -- These are covars. We will *not* quantify over these, but - -- we must make sure also not to quantify over any cv's kinds, - -- so we include them here as further direction for quantifyTyVars + -- These are covars. Included only so that we don't repeatedly + -- look at covars' kinds in accumulator. Not used by quantifyTyVars. } instance Semi.Semigroup CandidatesQTvs where @@ -1185,6 +1193,14 @@ instance Outputable CandidatesQTvs where candidateKindVars :: CandidatesQTvs -> TyVarSet candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) +partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (DTyVarSet, CandidatesQTvs) +partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred + = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs }) + where + (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs + (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs + extracted = extracted_kvs `unionDVarSet` extracted_tvs + -- | Gathers free variables to use as quantification candidates (in -- 'quantifyTyVars'). This might output the same var -- in both sets, if it's used in both a type and a kind. @@ -1282,28 +1298,33 @@ collect_cand_qtvs is_dep bound dvs ty -- (which comes next) works correctly ; cur_lvl <- getTcLevel - ; if tcTyVarLevel tv `strictlyDeeperThan` cur_lvl && - -- this tyvar is from an outer context: see Wrinkle - -- in Note [Naughty quantification candidates] - - intersectsVarSet bound (tyCoVarsOfType tv_kind) - - then -- See Note [Naughty quantification candidates] - do { traceTc "Zapping naughty quantifier" $ - vcat [ ppr tv <+> dcolon <+> ppr tv_kind - , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound) - , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $ - tyCoVarsOfType tv_kind) ] - - ; writeMetaTyVar tv (anyTypeOfKind tv_kind) - ; collect_cand_qtvs True bound dv tv_kind } - - else do { let tv' = tv `setTyVarKind` tv_kind - dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' } - | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' } - -- See Note [Order of accumulation] - ; collect_cand_qtvs True emptyVarSet dv' tv_kind } } - -- Why emptyVarSet? See Note [Closing over free variable kinds] in TyCoRep + ; if | tcTyVarLevel tv <= cur_lvl + -> return dv -- this variable is from an outer context; skip + -- See Note [Use level numbers ofor quantification] + + | intersectsVarSet bound (tyCoVarsOfType tv_kind) + -- the tyvar must not be from an outer context, but we have + -- already checked for this. + -- See Note [Naughty quantification candidates] + -> do { traceTc "Zapping naughty quantifier" $ + vcat [ ppr tv <+> dcolon <+> ppr tv_kind + , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound) + , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $ + tyCoVarsOfType tv_kind) ] + + ; writeMetaTyVar tv (anyTypeOfKind tv_kind) + + -- See Note [Recurring into kinds for candidateQTyVars] + ; collect_cand_qtvs True bound dv tv_kind } + + | otherwise + -> do { let tv' = tv `setTyVarKind` tv_kind + dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' } + | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' } + -- See Note [Order of accumulation] + + -- See Note [Recurring into kinds for candidateQTyVars] + ; collect_cand_qtvs True bound dv' tv_kind } } collect_cand_qtvs_co :: VarSet -- bound variables -> CandidatesQTvs -> Coercion @@ -1329,19 +1350,11 @@ collect_cand_qtvs_co bound = go_co go_co dv (KindCo co) = go_co dv co go_co dv (SubCo co) = go_co dv co - go_co dv@(DV { dv_cvs = cvs }) (HoleCo hole) + go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole case m_co of Just co -> go_co dv co - Nothing - | cv `elemVarSet` cvs -> return dv - - | otherwise - -> collect_cand_qtvs True bound (dv { dv_cvs = cvs `extendVarSet` cv }) - cv_type - -- See Note [Free vars in coercion hole] - where cv = coHoleCoVar hole - cv_type = varType cv + Nothing -> go_cv dv (coHoleCoVar hole) go_co dv (CoVarCo cv) = go_cv dv cv @@ -1362,8 +1375,8 @@ collect_cand_qtvs_co bound = go_co | is_bound cv = return dv | cv `elemVarSet` cvs = return dv - -- Why emptyVarSet below? See Note [Closing over free variable kinds] in TyCoRep - | otherwise = collect_cand_qtvs True emptyVarSet + -- See Note [Recurring into kinds for candidateQTyVars] + | otherwise = collect_cand_qtvs True bound (dv { dv_cvs = cvs `extendVarSet` cv }) (idType cv) @@ -1389,35 +1402,42 @@ element to the right. Note that the unitDVarSet/mappend implementation would not be wrong against any specification -- just suboptimal and confounding to users. -Note [Free vars in coercion hole] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -First, read Note [Closing over free variable kinds] in TyCoRep, paying +Note [Recurring into kinds for candidateQTyVars] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +First, read Note [Closing over free variable kinds] in TyCoFVs, paying attention to the end of the Note about using an empty bound set when traversing a variable's kind. -We do not do this for coercion holes. (The other Note doesn't address coercion -holes, because that Note is about Core, where coercion holes do not exist.) -Coercion holes are *never* bound. Yet a coercion hole *can* mention a locally -bound type/coercion variable in its kind. This would happen if the constraint -associated with the coercion hole is inside an implication constraint, and the -bound variables in the hole's type are the skolems of the implication. We do -not want to collect *all* free variables in the coercion hole's kind, because -that list might contain skolems. (This actually happened in test case -dependent/should_fail/BadTelescope5.) Instead, we remember the bound variables -when traversing the coercion hole's kind so we can avoid visiting bound -variables there. - -Example: forall k1 k2. .... |> (hole :: k1 ~# k2) .... -This is obviously bogus, but if we collect k1 and k2 into the candidates, -we'll have skolems in the CandidatesQTvs, directly contradicting that data -structure's invariant. See its definition. - -Of course, Note [Closing over free variable kinds] observes that maintaining -a bound set while going into a kind is potentially wrong, if there is shadowing. -However, given that we are in the type-checker now, not in Core, shadowing cannot -happen: the renamer would have sorted it out. So the bug that Note is fixing -cannot occur here, and so we do not have to zap the bound set when looking at -kinds. +That Note concludes with the recommendation that we empty out the bound +set when recurring into the kind of a type variable. Yet, we do not do +this here. I have two tasks in order to convince you that this code is +right. First, I must show why it is safe to ignore the reasoning in that +Note. Then, I must show why is is necessary to contradict the reasoning in +that Note. + +Why it is safe: There can be no +shadowing in the candidateQ... functions: they work on the output of +type inference, which is seeded by the renamer and its insistence to +use different Uniques for different variables. (In contrast, the Core +functions work on the output of optimizations, which may introduce +shadowing.) Without shadowing, the problem studied by +Note [Closing over free variable kinds] in TyCoFVs cannot happen. + +Why it is necessary: +Wiping the bound set would be just plain wrong here. Consider + + forall k1 k2 (a :: k1). Proxy k2 (a |> (hole :: k1 ~# k2)) + +We really don't want to think k1 and k2 are free here. (It's true that we'll +never be able to fill in `hole`, but we don't want to go off the rails just +because we have an insoluble coercion hole.) So: why is it wrong to wipe +the bound variables here but right in Core? Because the final statement +in Note [Closing over free variable kinds] in TyCoFVs is wrong: not +every variable is either free or bound. A variable can be a hole, too! +The reasoning in that Note then breaks down. + +And the reasoning applies just as well to free non-hole variables, so we +retain the bound set always. -} @@ -1433,17 +1453,8 @@ quantifyTyVars is given the free vars of a type that we are about to wrap in a forall. It takes these free type/kind variables (partitioned into dependent and -non-dependent variables) and - 1. Zonks them and remove globals and covars - 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals) - 3. Calls skolemiseQuantifiedTyVar on each - -Step (2) is often unimportant, because the kind variable is often -also free in the type. Eg - Typeable k (a::k) -has free vars {k,a}. But the type (see #7916) - (f::k->*) (a::k) -has free vars {f,a}, but we must add 'k' as well! Hence step (2). +non-dependent variables) skolemises metavariables with a TcLevel greater +than the ambient level (see Note [Use level numbers of quantification]). * This function distinguishes between dependent and non-dependent variables only to keep correct defaulting behavior with -XNoPolyKinds. @@ -1453,6 +1464,48 @@ has free vars {f,a}, but we must add 'k' as well! Hence step (2). - a coercion variable (or any tv mentioned in the kind of a covar) - a runtime-rep variable +Note [Use level numbers for quantification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The level numbers assigned to metavariables are very useful. Not only +do they track touchability (Note [TcLevel and untouchable type variables] +in TcType), but they also allow us to determine which variables to +generalise. The rule is this: + + When generalising, quantify only metavariables with a TcLevel greater + than the ambient level. + +This works because we bump the level every time we go inside a new +source-level construct. In a traditional generalisation algorithm, we +would gather all free variables that aren't free in an environment. +However, if a variable is in that environment, it will always have a lower +TcLevel: it came from an outer scope. So we can replace the "free in +environment" check with a level-number check. + +Here is an example: + + f x = x + (z True) + where + z y = x * x + +We start by saying (x :: alpha[1]). When inferring the type of z, we'll +quickly discover that z :: alpha[1]. But it would be disastrous to +generalise over alpha in the type of z. So we need to know that alpha +comes from an outer environment. By contrast, the type of y is beta[2], +and we are free to generalise over it. What's the difference between +alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for +generalisation, and so we generalise it. alpha[1] does not, and so +we leave it alone. + +Note that not *every* variable with a higher level will get generalised, +either due to the monomorphism restriction or other quirks. See, for +example, the code in TcSimplify.decideMonoTyVars and in +TcHsType.kindGeneralizeSome, both of which exclude certain otherwise-eligible +variables from being generalised. + +Using level numbers for quantification is implemented in the candidateQTyVars... +functions, by adding only those variables with a level strictly higher than +the ambient level to the set of candidates. + Note [quantifyTyVars determinism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The results of quantifyTyVars are wrapped in a forall and can end up in the @@ -1468,15 +1521,17 @@ Note [Deterministic UniqFM] in UniqDFM. -} quantifyTyVars - :: TcTyCoVarSet -- Global tvs; already zonked - -> CandidatesQTvs -- See Note [Dependent type variables] + :: CandidatesQTvs -- See Note [Dependent type variables] -- Already zonked -> TcM [TcTyVar] -- See Note [quantifyTyVars] -- Can be given a mixture of TcTyVars and TyVars, in the case of -- associated type declarations. Also accepts covars, but *never* returns any. -quantifyTyVars gbl_tvs - dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars }) +-- According to Note [Use level numbers for quantification] and the +-- invariants on CandidateQTvs, we do not have to filter out variables +-- free in the environment here. Just quantify unconditionally, subject +-- to the restrictions in Note [quantifyTyVars]. +quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) -- short-circuit common case | isEmptyDVarSet dep_tkvs , isEmptyDVarSet nondep_tkvs @@ -1484,53 +1539,21 @@ quantifyTyVars gbl_tvs ; return [] } | otherwise - = do { outer_tclvl <- getTcLevel - ; traceTc "quantifyTyVars 1" (vcat [ppr outer_tclvl, ppr dvs, ppr gbl_tvs]) - ; let co_tvs = closeOverKinds covars - mono_tvs = gbl_tvs `unionVarSet` co_tvs - -- NB: All variables in the kind of a covar must not be - -- quantified over, as we don't quantify over the covar. - - dep_kvs = scopedSort $ dVarSetElems $ - dep_tkvs `dVarSetMinusVarSet` mono_tvs + = do { traceTc "quantifyTyVars 1" (ppr dvs) + + ; let dep_kvs = scopedSort $ dVarSetElems dep_tkvs -- scopedSort: put the kind variables into -- well-scoped order. -- E.g. [k, (a::k)] not the other way roud - nondep_tvs = dVarSetElems $ - (nondep_tkvs `minusDVarSet` dep_tkvs) - `dVarSetMinusVarSet` mono_tvs + nondep_tvs = dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs) -- See Note [Dependent type variables] -- The `minus` dep_tkvs removes any kind-level vars -- e.g. T k (a::k) Since k appear in a kind it'll -- be in dv_kvs, and is dependent. So remove it from -- dv_tvs which will also contain k - -- No worry about dependent covars here; - -- they are all in dep_tkvs -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV - -- This block uses level numbers to decide what to quantify - -- and emits a warning if the two methods do not give the same answer - ; let dep_kvs2 = scopedSort $ dVarSetElems $ - filterDVarSet (quantifiableTv outer_tclvl) dep_tkvs - nondep_tvs2 = filter (quantifiableTv outer_tclvl) $ - dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs) - - all_ok = dep_kvs == dep_kvs2 && nondep_tvs == nondep_tvs2 - bad_msg = hang (text "Quantification by level numbers would fail") - 2 (vcat [ text "Outer level =" <+> ppr outer_tclvl - , text "gbl_tvs =" <+> ppr gbl_tvs - , text "mono_tvs =" <+> ppr mono_tvs - , text "dep_tkvs =" <+> ppr dep_tkvs - , text "co_vars =" <+> vcat [ ppr cv <+> dcolon <+> ppr (varType cv) - | cv <- nonDetEltsUniqSet covars ] - , text "co_tvs =" <+> ppr co_tvs - , text "dep_kvs =" <+> ppr dep_kvs - , text "dep_kvs2 =" <+> ppr dep_kvs2 - , text "nondep_tvs =" <+> ppr nondep_tvs - , text "nondep_tvs2 =" <+> ppr nondep_tvs2 ]) - ; MASSERT2( all_ok, bad_msg ) - -- In the non-PolyKinds case, default the kind variables -- to *, and zonk the tyvars as usual. Notice that this -- may make quantifyTyVars return a shorter list @@ -1544,9 +1567,7 @@ quantifyTyVars gbl_tvs -- now refer to the dep_kvs' ; traceTc "quantifyTyVars 2" - (vcat [ text "globals:" <+> ppr gbl_tvs - , text "mono_tvs:" <+> ppr mono_tvs - , text "nondep:" <+> pprTyVars nondep_tvs + (vcat [ text "nondep:" <+> pprTyVars nondep_tvs , text "dep:" <+> pprTyVars dep_kvs , text "dep_kvs'" <+> pprTyVars dep_kvs' , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ]) @@ -1578,10 +1599,10 @@ quantifyTyVars gbl_tvs False -> do { tv <- skolemiseQuantifiedTyVar tkv ; return (Just tv) } } -quantifiableTv :: TcLevel -- Level of the context, outside the quantification - -> TcTyVar - -> Bool -quantifiableTv outer_tclvl tcv +isQuantifiableTv :: TcLevel -- Level of the context, outside the quantification + -> TcTyVar + -> Bool +isQuantifiableTv outer_tclvl tcv | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separately = tcTyVarLevel tcv > outer_tclvl | otherwise @@ -1859,22 +1880,6 @@ a \/\a in the final result but all the occurrences of a will be zonked to () -} --- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in --- the environment. To improve subsequent calls to the same function it writes --- the zonked set back into the environment. Note that this returns all --- variables free in anything (term-level or type-level) in scope. We thus --- don't have to worry about clashes with things that are not in scope, because --- if they are reachable, then they'll be returned here. --- NB: This is closed over kinds, so it can return unification variables mentioned --- in the kinds of in-scope tyvars. -tcGetGlobalTyCoVars :: TcM TcTyVarSet -tcGetGlobalTyCoVars - = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv - ; gbl_tvs <- readMutVar gtv_var - ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs - ; writeMutVar gtv_var gbl_tvs' - ; return gbl_tvs' } - zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet -- Zonk a type and take its free variables -- With kind polymorphism it can be essential to zonk *first* |