Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 5eea3311 by Simon Peyton Jones at 2025-07-06T23:09:47+01:00 We need wanted/wanted fundeps too ...and some other refactors - - - - - 4 changed files: - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs Changes: ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -413,7 +413,7 @@ solveEqualityDict ev cls tys do { let loc = ctEvLoc ev sc_pred = classMethodInstTy sel_id tys ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id - ; given_ev <- newGivenEvVar loc (sc_pred, ev_expr) + ; given_ev <- newGivenEv loc (sc_pred, ev_expr) ; startAgainWith (mkNonCanonical $ CtGiven given_ev) } | otherwise = pprPanic "solveEqualityDict" (ppr cls) @@ -1403,8 +1403,8 @@ now!). Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary -and top-level instances) for functional dependencies, and implicit -parameters, is that we simply produce new Wanted equalities. So for example +and top-level instances) for functional dependencies (including implicit +parameters), is that we simply produce new Wanted equalities. So for example class D a b | a -> b where ... Inert: @@ -1663,43 +1663,46 @@ doTopFunDepImprovement cts inst_pred inst_loc doLocalFunDepImprovement :: Bag DictCt -> TcS (Cts,Bool) --- Add wanted constraints from type-class functional dependencies --- against Givens -doLocalFunDepImprovement cts +-- Using functional dependencies, interact the unsolved Wanteds +-- against each other and the inert Givens, to produce new equalities +doLocalFunDepImprovement wanted = do { inerts <- getInertCans -- The inert_dicts are all Givens - ; do_dict_fundeps (do_one (inert_dicts inerts)) cts } + ; let all_dicts :: DictMap DictCt -- Both Givens and Wanteds + all_dicts = foldr addDict (inert_dicts inerts) wanted + ; do_dict_fundeps (do_one all_dicts) wanted } where - do_one givens (DictCt { di_cls = cls, di_ev = wanted_ev }) - = do_dict_fundeps do_one_given (findDictsByClass givens cls) + -- all_dicts are all the Givens and all the Wanteds + do_one all_dicts (DictCt { di_cls = cls, di_ev = wanted_ev }) + = do_dict_fundeps do_interaction (findDictsByClass all_dicts cls) where wanted_pred = ctEvPred wanted_ev wanted_loc = ctEvLoc wanted_ev - do_one_given :: DictCt -> TcS (Cts,Bool) - do_one_given (DictCt { di_ev = given_ev }) + do_interaction :: DictCt -> TcS (Cts,Bool) + do_interaction (DictCt { di_ev = all_ev }) -- This can be Given or Wanted = do { traceTcS "doLocalFunDepImprovement" $ vcat [ ppr wanted_ev , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc) - , pprCtLoc given_loc, ppr (isGivenLoc given_loc) + , pprCtLoc all_loc, ppr (isGivenLoc all_loc) , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ] ; unifyFunDepWanteds wanted_ev $ - improveFromAnother (deriv_loc, given_rewriters) - given_pred wanted_pred } + improveFromAnother (deriv_loc, all_rewriters) + all_pred wanted_pred } where - given_pred = ctEvPred given_ev - given_loc = ctEvLoc given_ev - given_rewriters = ctEvRewriters given_ev + all_pred = ctEvPred all_ev + all_loc = ctEvLoc all_ev + all_rewriters = ctEvRewriters all_ev deriv_loc = wanted_loc { ctl_depth = deriv_depth , ctl_origin = deriv_origin } deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth` - ctl_depth given_loc + ctl_depth all_loc deriv_origin = FunDepOrigin1 wanted_pred (ctLocOrigin wanted_loc) (ctLocSpan wanted_loc) - given_pred - (ctLocOrigin given_loc) - (ctLocSpan given_loc) + all_pred + (ctLocOrigin all_loc) + (ctLocSpan all_loc) do_dict_fundeps :: (DictCt -> TcS (Cts,Bool)) -> Bag DictCt -> TcS (Cts,Bool) do_dict_fundeps do_dict_fundep cts @@ -2047,7 +2050,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven (GivenCt { ctev_evar = evar })) = -- See Note [Equality superclasses in quantified constraints] return [] | otherwise - = do { given_ev <- newGivenEvVar sc_loc $ + = do { given_ev <- newGivenEv sc_loc $ mk_given_desc sel_id sc_pred ; assertFuelPrecondition fuel $ mk_superclasses fuel rec_clss (CtGiven given_ev) tvs theta sc_pred } ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -780,12 +780,12 @@ can_eq_app ev s1 t1 s2 t2 = do { let co = mkCoVarCo evar co_s = mkLRCo CLeft co co_t = mkLRCo CRight co - ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2 - , evCoercion co_s ) - ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2 - , evCoercion co_t ) - ; emitWorkNC [CtGiven evar_t] - ; startAgainWith (mkNonCanonical $ CtGiven evar_s) } + ; ev_s <- newGivenEv loc ( mkTcEqPredLikeEv ev s1 s2 + , evCoercion co_s ) + ; ev_t <- newGivenEv loc ( mkTcEqPredLikeEv ev t1 t2 + , evCoercion co_t ) + ; emitWorkNC [CtGiven ev_t] + ; startAgainWith (mkNonCanonical $ CtGiven ev_s) } where loc = ctEvLoc ev @@ -1632,7 +1632,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -> do { let kind_co = mkKindCo (mkCoVarCo evar) pred_ty = unSwap swapped mkNomEqPred ki1 ki2 kind_loc = mkKindEqLoc xi1 xi2 loc - ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co) + ; kind_ev <- newGivenEv kind_loc (pred_ty, evCoercion kind_co) ; emitWorkNC [CtGiven kind_ev] ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) } @@ -2597,7 +2597,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio = do { let new_tm = evCoercion ( mkSymCo lhs_co `mkTransCo` maybeSymCo swapped (mkCoVarCo old_evar) `mkTransCo` rhs_co) - ; CtGiven <$> newGivenEvVar loc (new_pred, new_tm) } + ; CtGiven <$> newGivenEv loc (new_pred, new_tm) } | CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) <- old_ev = do { let rewriters' = rewriters S.<> new_rewriters @@ -3044,6 +3044,7 @@ equality with the template on the left. Delicate, but it works. -} -------------------- + tryFunDeps :: EqCt -> SolverStage () tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) | NomEq <- eq_rel @@ -3253,7 +3254,7 @@ improveWantedLocalFunEqs -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted) -> TcS Bool -- True <=> some unifications -- Emit improvement equalities for a Wanted constraint, by comparing --- the current work item with inert CFunEqs (boh Given and Wanted) +-- the current work item with inert CFunEqs (both Given and Wanted) -- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' -- -- See Note [FunDep and implicit parameter reactions] ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -57,7 +57,7 @@ module GHC.Tc.Solver.Monad ( unifyTyVar, reportUnifications, setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, - newEvVar, newGivenEvVar, emitNewGivens, + newEvVar, newGivenEv, emitNewGivens, checkReductionDepth, getSolvedDicts, setSolvedDicts, @@ -2081,12 +2081,12 @@ newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds newEvVar :: TcPredType -> TcS EvVar newEvVar pred = wrapTcS (TcM.newEvVar pred) -newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence +newGivenEv :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence -- Make a new variable of the given PredType, -- immediately bind it to the given term -- and return its CtEvidence -- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint -newGivenEvVar loc (pred, rhs) +newGivenEv loc (pred, rhs) = do { new_ev <- newBoundEvVarId pred rhs ; return $ GivenCt { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc } } @@ -2101,7 +2101,7 @@ newBoundEvVarId pred rhs emitNewGivens :: CtLoc -> [(Role,TcCoercion)] -> TcS () emitNewGivens loc pts = do { traceTcS "emitNewGivens" (ppr pts) - ; gs <- mapM (newGivenEvVar loc) $ + ; gs <- mapM (newGivenEv loc) $ [ (mkEqPredRole role ty1 ty2, evCoercion co) | (role, co) <- pts , let Pair ty1 ty2 = coercionKind co @@ -2484,7 +2484,7 @@ checkTypeEq ev eq_rel lhs rhs = --------------------------- mk_new_given :: (TcTyVar, TcType) -> TcS Ct mk_new_given (new_tv, fam_app) - = mkNonCanonical . CtGiven <$> newGivenEvVar cb_loc (given_pred, given_term) + = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) where new_ty = mkTyVarTy new_tv given_pred = mkNomEqPred fam_app new_ty ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -1563,7 +1563,7 @@ finish_rewrite new_tm = assert (coercionRole co == ev_rw_role) mkEvCast (evId old_evar) (downgradeRole Representational ev_rw_role co) - ; new_ev <- newGivenEvVar loc (new_pred, new_tm) + ; new_ev <- newGivenEv loc (new_pred, new_tm) ; continueWith $ CtGiven new_ev } finish_rewrite View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5eea331167b1352565067e4680fc2e81... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5eea331167b1352565067e4680fc2e81... You're receiving this email because of your account on gitlab.haskell.org.