[Git][ghc/ghc][wip/T25647] handle [Naughty quantification candidates]

[Patrick (@soulomoon)]

Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC


Commits:
def98f3c by Patrick at 2025-03-11T04:39:48+08:00
handle [Naughty quantification candidates]

- - - - -


3 changed files:

- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Utils/TcMType.hs


Changes:

=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3459,8 +3459,8 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
        -- check there too!
 
        -- See Note [Generalising in tcTyFamInstEqnGuts]
-       ; dvs  <- candidateQTyVarsWithBinders outer_tvs lhs_ty
-       ; qtvs <- quantifyTyVars' outer_tvs skol_info dvs
+       ; (dvs, cqdvs)  <- candidateQTyVarsWithBinders outer_tvs lhs_ty
+       ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
        ; let final_tvs = scopedSort qtvs
              -- This scopedSort is important: the qtvs may be /interleaved/ with
              -- the outer_tvs.  See Note [Generalising in tcTyFamInstEqnGuts]


=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -985,7 +985,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
   = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
        ; (tclvl, wanted, (wcs, (outer_bndrs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind))))
             <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
-               bindOuterFamEqnTKBndrs skol_info hs_outer_bndrs    $  -- Binds skolem TcTyVars
+               bindOuterFamEqnTKBndrs skol_info hs_outer_bndrs    $  -- Binds skolem TcTyVars or TauVars
                do { stupid_theta <- tcHsContext hs_ctxt
                   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
                   ; (lhs_applied_ty, lhs_applied_kind)
@@ -1029,8 +1029,8 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
        ; outer_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVarsMaybe $ outer_tvs ++ wcs
 
        -- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
-       ; dvs  <- candidateQTyVarsWithBinders outer_tvs lhs_ty
-       ; qtvs <- quantifyTyVars' outer_tvs skol_info dvs
+       ; (dvs, cqdvs)  <- candidateQTyVarsWithBinders outer_tvs lhs_ty
+       ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
                  -- Have to make a same defaulting choice for reuslt kind here
                  -- and the `kindGeneralizeAll` in `tcConDecl`.
                  -- see (GT4) in


=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -80,7 +80,7 @@ module GHC.Tc.Utils.TcMType (
   defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
   quantifyTyVars, doNotQuantifyTyVars,
   zonkAndSkolemise, skolemiseQuantifiedTyVar,
-  quantifyTyVars',
+  quantifyTyVarsWithBinders,
 
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -1375,6 +1375,14 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
        , dv_tvs = tvs `delDVarSetList` vars
        , dv_cvs = cvs `delVarSetList`  vars }
 
+boundedCandidates :: CandidatesQTvs -> [Var] -> [Var]
+boundedCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = _cvs }) vars
+  =  dVarSetElems $
+          (kvs `intersectDVarSet` dvars)
+          `unionDVarSet` (tvs `intersectDVarSet` dvars)
+  where dvars = extendDVarSetList emptyDVarSet vars
+
+
 partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs)
 -- The selected TyVars are returned as a non-deterministic TyVarSet
 partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
@@ -1384,20 +1392,25 @@ 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] -> Type -> TcM CandidatesQTvs
+candidateQTyVarsWithBinders :: [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
+
+-- 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 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) }
+       ; return (all_tvs `delCandidates` bound_tvs, boundedCandidates all_tvs bound_tvs) }
+
 
 -- | Gathers free variables to use as quantification candidates (in
--- 'quantifyTyVars'). This might output the same var
+-- 'quantifyTyVarsWithBinders). This might output the same var
 -- in both sets, if it's used in both a type and a kind.
 -- The variables to quantify must have a TcLevel strictly greater than
 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
@@ -1744,9 +1757,9 @@ quantifyTyVars :: SkolemInfo
                -> CandidatesQTvs   -- See Note [Dependent type variables]
                                    -- Already zonked
                -> TcM [TcTyVar]
-quantifyTyVars = quantifyTyVars' []
+quantifyTyVars = quantifyTyVarsWithBinders []
 
-quantifyTyVars' ::
+quantifyTyVarsWithBinders ::
                [TcTyVar]
                -> SkolemInfo
                -> CandidatesQTvs   -- See Note [Dependent type variables]
@@ -1759,7 +1772,7 @@ quantifyTyVars' ::
 -- 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' cvs skol_info dvs
+quantifyTyVarsWithBinders cvs skol_info dvs
        -- short-circuit common case
   | isEmptyCandidates dvs && null cvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
@@ -1767,7 +1780,10 @@ quantifyTyVars' cvs skol_info dvs
 
   | otherwise
   = do { traceTc "quantifyTyVars {"
-           ( vcat [ text "dvs =" <+> ppr dvs ])
+           ( vcat [
+            text "dvs =" <+> ppr dvs,
+            text "cvs =" <+> ppr cvs
+            ])
 
        ; undefaulted <- defaultTyVars dvs
        ; final_qtvs  <- liftZonkM $ mapMaybeM zonk_quant (undefaulted++cvs)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/def98f3c43922ad48d8e49b409033aa5e07b2821

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/def98f3c43922ad48d8e49b409033aa5e07b2821
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/20250310/145122ce/attachment-0001.html>