[Git][ghc/ghc][wip/T25647] fix ordering issue in tcFamInstLHSBinders
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Thu Mar 13 21:24:27 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
3cc33fd8 by Patrick at 2025-03-14T05:24:15+08:00
fix ordering issue in tcFamInstLHSBinders
- - - - -
4 changed files:
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Zonk/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -258,13 +258,14 @@ tcFamInstLHSBinders tclvl skol_info outer_bndrs hs_outer_bndrs wcs lhs_ty wanted
; checkFamTelescope tclvl hs_outer_bndrs outer_exp_tvs
-- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
-- See Note [Type variables in type families instance decl]
- ; (dvs, wc_itvs, outer_imp_itvs) <- candidateQTyVarsWithBinders outer_exp_tvs outer_imp_tvs wcs lhs_ty
- ; (qtvs, outer_imp_qtvs) <- quantifyTyVarsWithBinders wc_itvs outer_imp_itvs skol_info dvs
+ ; (dvs, outer_wcs_imp_dvs) <- candidateQTyVarsWithBinders outer_exp_tvs (outer_imp_tvs ++ wcs) lhs_ty
+ ; qtvs <- quantifyTyVarsWithBinders skol_info dvs outer_wcs_imp_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 ++ outer_imp_qtvs)
+ ; let final_tvs = scopedSort (qtvs ++ outer_exp_tvs)
+ ; let non_user_tvs = dVarSetElems $ mkDVarSet qtvs `delDVarSetList` outer_wcs_imp_dvs
-- This scopedSort is important: the qtvs may be /interleaved/ with
-- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
; traceTc "tcFamInstLHSBinders" $
@@ -276,17 +277,16 @@ tcFamInstLHSBinders tclvl skol_info outer_bndrs hs_outer_bndrs wcs lhs_ty wanted
, text "wcs:" <+> pprTyVars wcs
-- after zonking
- , text "wc_itvs:" <+> pprTyVars wc_itvs
- , text "outer_imp_itvs:" <+> pprTyVars outer_imp_itvs
, text "dvs:" <+> ppr dvs
+ , text "outer_wcs_imp_dvs:" <+> pprTyVars outer_wcs_imp_dvs
-- after quantification
- , text "qtvs(include wildcards):" <+> pprTyVars qtvs
- , text "outer_imp_qtvs:" <+> pprTyVars outer_imp_qtvs
+ , text "qtvs:" <+> pprTyVars qtvs
+ , text "non_user_tvs:" <+> pprTyVars non_user_tvs
, text "final_tvs:" <+> pprTyVars final_tvs
]
; reportUnsolvedEqualities skol_info final_tvs tclvl wanted
- return (final_tvs, qtvs)
+ return (final_tvs, non_user_tvs)
-- Gives the kind for every TyCon that has a standalone kind signature
type KindSigEnv = NameEnv Kind
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -1347,7 +1347,8 @@ captureWildCards thing_inside
; res <- updLclEnv (\ env -> env { tcl_wcs = wcs_var}) $
thing_inside
; wcs <- readTcRef wcs_var
- ; return (wcs, res) }
+ -- Reverse the list to preserve the order in which the wildcards were added
+ ; return (reverse wcs, res) }
capture_messages :: TcM r -> TcM (r, Messages TcRnMessage)
-- capture_messages simply captures and returns the
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -86,6 +86,7 @@ module GHC.Tc.Utils.TcMType (
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
candidateQTyVarsWithBinders,
CandidatesQTvs(..), delCandidates,
+ intersectCandidates,
candidateKindVars, partitionCandidates,
------------------------------
@@ -1389,20 +1390,20 @@ 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] -> [TyVar] -> Type -> TcM (CandidatesQTvs, [TyVar], [TyVar])
+candidateQTyVarsWithBinders :: [TyVar] -> [TyVar] -> Type -> TcM (CandidatesQTvs, [TyVar])
-- (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
-candidateQTyVarsWithBinders outer_exp_tvs outer_imp_tvs wcs ty
+candidateQTyVarsWithBinders outer_exp_tvs outer_wcs_imp_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, intersectCandidates all_tvs outer_imp_tvs, intersectCandidates all_tvs wcs) }
+ ; return (all_tvs `delCandidates` outer_exp_tvs, all_tvs `intersectCandidates` outer_wcs_imp_tvs) }
where
- bound_tvs = outer_exp_tvs ++ outer_imp_tvs ++ wcs
+ bound_tvs = outer_exp_tvs ++ outer_wcs_imp_tvs
-- | Gathers free variables to use as quantification candidates (in
-- 'quantifyTyVarsWithBinders'). This might output the same var
@@ -1752,15 +1753,14 @@ quantifyTyVars :: SkolemInfo
-> CandidatesQTvs -- See Note [Dependent type variables]
-- Already zonked
-> TcM [TcTyVar]
-quantifyTyVars ski tvs = fst <$> quantifyTyVarsWithBinders [] [] ski tvs
+quantifyTyVars ski tvs = quantifyTyVarsWithBinders ski tvs []
quantifyTyVarsWithBinders ::
- [TcTyVar]
- -> [TcTyVar]
- -> SkolemInfo
+ SkolemInfo
-> CandidatesQTvs -- See Note [Dependent type variables]
-- Already zonked
- -> TcM ([TcTyVar], [TcTyVar])
+ -> [TcTyVar]
+ -> 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.
@@ -1769,39 +1769,36 @@ quantifyTyVarsWithBinders ::
-- free in the environment here. Just quantify unconditionally, subject
-- to the restrictions in Note [quantifyTyVars].
--- for wildcards, do not default, just skolemise add to the list of quantified
--- for outer_imp_qtvs, do not default, just skolemise, and return separately
-quantifyTyVarsWithBinders wc_itvs outer_imp_itvs skol_info dvs
+-- for outer_wcs_imp_tvs, do not default, just skolemise add to the list of quantified
+quantifyTyVarsWithBinders skol_info dvs outer_wcs_imp_tvs
-- short-circuit common case
- | isEmptyCandidates dvs && null wc_itvs && null outer_imp_itvs
+ | isEmptyCandidates dvs && null outer_wcs_imp_tvs
= do { traceTc "quantifyTyVars has nothing to quantify" empty
- ; return ([], []) }
+ ; return [] }
| otherwise
= do { traceTc "quantifyTyVars {"
( vcat [
text "dvs =" <+> ppr dvs,
- text "wc_qtvs =" <+> ppr wc_itvs,
- text "outer_imp_qtvs =" <+> ppr outer_imp_itvs
+ text "outer_wc_imp_qtvs=" <+> ppr outer_wcs_imp_tvs
])
- ; undefaulted <- defaultTyVars dvs
- ; (final_qtvs, out_imp_qtvs) <- liftZonkM $ do
- qtvs <- mapMaybeM zonk_quant (undefaulted ++ wc_itvs)
- out_imp_qtvs <- mapMaybeM zonk_quant outer_imp_itvs
- return (qtvs, out_imp_qtvs)
+ ; undefaulted <- defaultTyVars $ dvs `delCandidates` outer_wcs_imp_tvs
+ ; final_qtvs <- liftZonkM $ do
+ -- resume order and then skolemise
+ qtvs <- mapMaybeM zonk_quant $ dvs `intersectCandidates` (undefaulted ++ outer_wcs_imp_tvs)
+ return qtvs
; traceTc "quantifyTyVars }"
(vcat [ text "undefaulted:" <+> pprTyVars undefaulted
, 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 ++ out_imp_qtvs)
+ ; let co_vars = filter isCoVar final_qtvs
; massertPpr (null co_vars) (ppr co_vars)
- ; return (final_qtvs, out_imp_qtvs) }
+ ; return final_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
=====================================
@@ -83,7 +83,7 @@ import GHC.Core.Predicate
import GHC.Utils.Constants
import GHC.Utils.Outputable
import GHC.Utils.Misc
-import GHC.Utils.Monad ( mapAccumLM, mapMaybeM )
+import GHC.Utils.Monad ( mapAccumLM )
import GHC.Utils.Panic
import GHC.Data.Bag
@@ -269,7 +269,6 @@ zonkTcTyVar tv
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
zonkTcTyVarsToTcTyVars = mapM zonkTcTyVarToTcTyVar
-
zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> ZonkM TcTyVar
zonkTcTyVarToTcTyVar tv
= do { ty <- zonkTcTyVar tv
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3cc33fd819469dc0c41e5c05e6a01c22ea43e9e6
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3cc33fd819469dc0c41e5c05e6a01c22ea43e9e6
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/20250313/d42a3e9b/attachment-0001.html>
More information about the ghc-commits
mailing list