[Git][ghc/ghc][wip/T25647] improve zonking logic for tcFamInstLHSBinders
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Thu Mar 13 00:31:45 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
3d92409e by Patrick at 2025-03-13T08:31:35+08:00
improve zonking logic for tcFamInstLHSBinders
- - - - -
3 changed files:
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Zonk/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -249,47 +249,43 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
th_bndrs' `plusNameEnv` th_bndrs) }
--- tcFamInstLHSBinders :: FamEqn TyVar Name -> TcM [TyVar]
tcFamInstLHSBinders :: TcLevel -> SkolemInfo -> HsOuterFamEqnTyVarBndrs GhcTc -> HsOuterFamEqnTyVarBndrs GhcRn
-> [TcTyVar] -> Type -> WantedConstraints -> IOEnv (Env TcGblEnv TcLclEnv) ([TyCoVar], [TcTyVar])
tcFamInstLHSBinders tclvl skol_info outer_bndrs hs_outer_bndrs wcs lhs_ty wanted = do
- -- This code (and the stuff immediately above) is very similar
- -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the
- -- common code; but for the moment I concluded that it's
- -- clearer to duplicate it. Still, if you fix a bug here,
- -- check there too!
-- See Note [Type variables in type families instance decl]
; let outer_exp_tvs = scopedSort $ explicitOuterTyVars outer_bndrs
; let outer_imp_tvs = implicitOuterTyVars outer_bndrs
; checkFamTelescope tclvl hs_outer_bndrs outer_exp_tvs
- ; outer_imp_wc_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVarsMaybe $ outer_imp_tvs ++ wcs
+ ; wc_itvs <- liftZonkM $ zonkInvariants wcs
+ ; outer_imp_itvs <- liftZonkM $ zonkInvariants outer_imp_tvs
-- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
- ; (dvs, cqdvs) <- candidateQTyVarsWithBinders outer_imp_wc_tvs outer_exp_tvs lhs_ty
- ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
- -- Have to make a same defaulting choice for reuslt kind here
+ ; dvs <- candidateQTyVarsWithBinders (outer_exp_tvs ++ outer_imp_tvs ++ wcs) lhs_ty
+ ; (qtvs, outer_imp_qtvs) <- quantifyTyVarsWithBinders wc_itvs outer_imp_itvs skol_info dvs
+ -- Have to make a same defaulting choice for result kind here
-- and the `kindGeneralizeAll` in `tcConDecl`.
-- see (GT4) in
-- GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
-
- ; let final_tvs = scopedSort (qtvs ++ outer_exp_tvs)
-
+ ; let final_tvs = scopedSort (qtvs ++ outer_exp_tvs ++ outer_imp_qtvs)
+ -- This scopedSort is important: the qtvs may be /interleaved/ with
+ -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
; traceTc "tcFamInstLHSBinders" $
vcat [
- -- ppr fam_tc
- text "lhs_ty:" <+> ppr lhs_ty
- , text "final_tvs:" <+> pprTyVars final_tvs
+ text "outer_bndrs:" <+> ppr outer_bndrs
, text "outer_imp_tvs:" <+> pprTyVars outer_imp_tvs
, text "outer_exp_tvs:" <+> pprTyVars outer_exp_tvs
, text "wcs:" <+> pprTyVars wcs
- , text "outer_imp_wc_tvs:" <+> pprTyVars outer_imp_wc_tvs
- , text "outer_bndrs:" <+> ppr outer_bndrs
- , text "qtvs:" <+> pprTyVars qtvs
- , text "cqdvs:" <+> pprTyVars cqdvs
- , text "dvs:" <+> ppr dvs
+
+ -- after zonking
+ , text "wc_itvs:" <+> pprTyVars wc_itvs
+ , text "outer_imp_itvs:" <+> pprTyVars outer_imp_itvs
+ , text "dvs:" <+> ppr dvs
+
+ -- after quantification
+ , text "qtvs(include wildcards):" <+> pprTyVars qtvs
+ , text "outer_imp_qtvs:" <+> pprTyVars outer_imp_qtvs
+ , text "final_tvs:" <+> pprTyVars final_tvs
]
- -- This scopedSort is important: the qtvs may be /interleaved/ with
- -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
; reportUnsolvedEqualities skol_info final_tvs tclvl wanted
return (final_tvs, qtvs)
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1392,23 +1392,18 @@ partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
(extracted_tvs, rest_tvs) = partitionDVarSet pred tvs
extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs
-candidateQTyVarsWithBinders :: [TyVar] -> [TyVar] -> Type -> TcM (CandidatesQTvs, [TyVar])
+candidateQTyVarsWithBinders :: [TyVar] -> Type -> TcM CandidatesQTvs
-- (candidateQTyVarsWithBinders tvs ty) returns the candidateQTyVars
-- of (forall tvs. ty), but do not treat 'tvs' as bound for the purpose
-- of Note [Naughty quantification candidates]. Why?
-- Because we are going to scoped-sort the quantified variables
-- in among the tvs
--- also return the bound variables that need to be quantified
--- since they can be come from implicit binders and wildcards
--- See Note [Type variables in type families instance decl]
-candidateQTyVarsWithBinders imp_bound_tvs exp_bound_tvs ty
+candidateQTyVarsWithBinders bound_tvs ty
= do { kvs <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs)
; cur_lvl <- getTcLevel
; all_tvs <- collect_cand_qtvs ty False cur_lvl emptyVarSet kvs ty
- ; return (all_tvs `delCandidates` bound_tvs, boundedCandidates all_tvs imp_bound_tvs) }
- where bound_tvs = imp_bound_tvs ++ exp_bound_tvs
-
+ ; return (all_tvs `delCandidates` bound_tvs)}
-- | Gathers free variables to use as quantification candidates (in
-- 'quantifyTyVarsWithBinders). This might output the same var
@@ -1758,14 +1753,15 @@ quantifyTyVars :: SkolemInfo
-> CandidatesQTvs -- See Note [Dependent type variables]
-- Already zonked
-> TcM [TcTyVar]
-quantifyTyVars = quantifyTyVarsWithBinders []
+quantifyTyVars ski tvs = fst <$> quantifyTyVarsWithBinders [] [] ski tvs
quantifyTyVarsWithBinders ::
[TcTyVar]
+ -> [TcTyVar]
-> SkolemInfo
-> CandidatesQTvs -- See Note [Dependent type variables]
-- Already zonked
- -> TcM [TcTyVar]
+ -> TcM ([TcTyVar], [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.
@@ -1773,31 +1769,41 @@ quantifyTyVarsWithBinders ::
-- 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].
-quantifyTyVarsWithBinders cvs skol_info dvs
+
+-- for wildcards, do not default, just skolemise add to the list of quantified
+-- for outer_imp_qtvs, do not default and skolemise, and return separately
+quantifyTyVarsWithBinders wc_itvs outer_imp_itvs skol_info dvs
-- short-circuit common case
- | isEmptyCandidates dvs && null cvs
+ | isEmptyCandidates dvs && null wc_itvs && null outer_imp_itvs
= do { traceTc "quantifyTyVars has nothing to quantify" empty
- ; return [] }
+ ; return ([], []) }
| otherwise
= do { traceTc "quantifyTyVars {"
( vcat [
text "dvs =" <+> ppr dvs,
- text "cvs =" <+> ppr cvs
+ text "wc_qtvs =" <+> ppr wc_itvs,
+ text "outer_imp_qtvs =" <+> ppr outer_imp_itvs
])
; undefaulted <- defaultTyVars dvs
- ; final_qtvs <- liftZonkM $ mapMaybeM zonk_quant (undefaulted++cvs)
+ ; (final_qtvs, out_imp_qtvs) <- liftZonkM $ do
+ qtvs <- mapMaybeM zonk_quant undefaulted
+ wc_qtv <- mapMaybeM zonk_quant wc_itvs
+ out_imp_qtvs <- mapMaybeM zonk_quant outer_imp_itvs
+ return (qtvs ++ wc_qtv, out_imp_qtvs)
; traceTc "quantifyTyVars }"
(vcat [ text "undefaulted:" <+> pprTyVars undefaulted
- , text "final_qtvs:" <+> pprTyVars final_qtvs ])
+ , text "final_qtvs:" <+> pprTyVars final_qtvs
+ , text "out_imp_qtvs:" <+> pprTyVars out_imp_qtvs
+ ])
-- We should never quantify over coercion variables; check this
; let co_vars = filter isCoVar final_qtvs
; massertPpr (null co_vars) (ppr co_vars)
- ; return final_qtvs }
+ ; return (final_qtvs, out_imp_qtvs) }
where
-- zonk_quant returns a tyvar if it should be quantified over;
-- otherwise, it returns Nothing. The latter case happens for
=====================================
compiler/GHC/Tc/Zonk/TcType.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Tc.Zonk.TcType
, zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars
, zonkInvisTVBinder
, zonkCo
- , zonkTcTyVarsToTcTyVarsMaybe
+ , zonkInvariants
-- ** Zonking 'TyCon's
, zonkTcTyCon
@@ -270,8 +270,13 @@ zonkTcTyVar tv
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
zonkTcTyVarsToTcTyVars = mapM zonkTcTyVarToTcTyVar
-zonkTcTyVarsToTcTyVarsMaybe :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
-zonkTcTyVarsToTcTyVarsMaybe = mapMaybeM (fmap getTyVar_maybe . zonkTcTyVar)
+-- let x = zonked and y = unzonked
+-- take intersection of x and y
+zonkInvariants :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
+zonkInvariants y = do
+ x <- mapMaybeM (fmap getTyVar_maybe . zonkTcTyVar) y
+ return $ dVarSetElems $ mkDVarSet y `intersectDVarSet` mkDVarSet x
+
zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> ZonkM TcTyVar
zonkTcTyVarToTcTyVar tv
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d92409e96b7cb1521492d00aaf6b1d6384a9a58
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d92409e96b7cb1521492d00aaf6b1d6384a9a58
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20250312/4de03ac4/attachment-0001.html>
More information about the ghc-commits
mailing list