Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 5cf99a78 by Simon Peyton Jones at 2025-10-14T21:28:29+01:00 Improve tracking of RewriterSets A bit experimental. Avoids taking the free coercion holes of a coercion, which can be expensive if the coercion is the result of a huge rewrite. The rewriter returns the RewriterSet! - - - - - 12 changed files: - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs Changes: ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1,3 +1,4 @@ +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_HADDOCK not-home #-} @@ -41,6 +42,11 @@ module GHC.Core.TyCo.Rep ( CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, KindMCoercion, + -- RewriterSet + -- RewriterSet(..) is exported concretely only for zonkRewriterSet + RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet, + addRewriter, unitRewriterSet, unionRewriterSet, delRewriterSet, + -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, @@ -78,6 +84,7 @@ import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstr -- friends: import GHC.Types.Var import GHC.Types.Var.Set( elemVarSet ) +import GHC.Types.Unique.Set import GHC.Core.TyCon import GHC.Core.Coercion.Axiom @@ -93,6 +100,7 @@ import GHC.Utils.Binary -- libraries import qualified Data.Data as Data hiding ( TyCon ) +import Data.Coerce import Data.IORef ( IORef ) -- for CoercionHole import Control.DeepSeq @@ -1672,7 +1680,7 @@ holes `HoleCo`, which get filled in later. {- ********************************************************************** %* * - Coercion holes + Coercion holes and RewriterSets %* * %********************************************************************* -} @@ -1681,7 +1689,7 @@ data CoercionHole = CoercionHole { ch_co_var :: CoVar -- See Note [CoercionHoles and coercion free variables] - , ch_ref :: IORef (Maybe Coercion) + , ch_ref :: IORef (Maybe (Coercion, RewriterSet)) } coHoleCoVar :: CoercionHole -> CoVar @@ -1702,6 +1710,33 @@ instance Outputable CoercionHole where instance Uniquable CoercionHole where getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv + +-- | A RewriterSet stores a set of CoercionHoles that have been used to rewrite +-- a constraint. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint +newtype RewriterSet = RewriterSet (UniqSet CoercionHole) + deriving newtype (Outputable, Semigroup, Monoid) + +emptyRewriterSet :: RewriterSet +emptyRewriterSet = RewriterSet emptyUniqSet + +unitRewriterSet :: CoercionHole -> RewriterSet +unitRewriterSet = coerce (unitUniqSet @CoercionHole) + +elemRewriterSet :: CoercionHole -> RewriterSet -> Bool +elemRewriterSet = coerce (elementOfUniqSet @CoercionHole) + +delRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet +delRewriterSet = coerce (delOneFromUniqSet @CoercionHole) + +unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet +unionRewriterSet = coerce (unionUniqSets @CoercionHole) + +isEmptyRewriterSet :: RewriterSet -> Bool +isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole) + +addRewriter :: RewriterSet -> CoercionHole -> RewriterSet +addRewriter = coerce (addOneToUniqSet @CoercionHole) + {- Note [Coercion holes] ~~~~~~~~~~~~~~~~~~~~~~~~ During typechecking, constraint solving for type classes works by @@ -1777,6 +1812,15 @@ constraint from floating] in GHC.Tc.Solver, item (4): Here co2 is a CoercionHole. But we /must/ know that it is free in co1, because that's all that stops it floating outside the implication. + +Note [CoercionHoles and RewriterSets] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A constraint C carries a set of "rewriters", a set of Wanted CoercionHoles that have been +used to rewrite C; see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. + +If C is an equality constraint and is solved, we track its RewriterSet in the filled +CoercionHole, so that it can be inherited by other constraints that have C in /their/ +rewriters. See zonkRewriterSet. -} ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -1327,7 +1327,7 @@ addDeferredBinding ctxt supp hints msg (EI { ei_evdest = Just dest -> do { -- See Note [Deferred errors for coercion holes] let co_var = coHoleCoVar hole ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var EvNonCanonical err_tm - ; fillCoercionHole hole (mkCoVarCo co_var) } } + ; fillCoercionHole hole (mkCoVarCo co_var, emptyRewriterSet) } } addDeferredBinding _ _ _ _ _ = return () -- Do not set any evidence for Given mkSolverErrorTerm :: CtLoc -> Type -- of the error term ===================================== compiler/GHC/Tc/Gen/Sig.hs ===================================== @@ -1481,7 +1481,7 @@ in `getRuleQuantCts`. Why not? do { ev_id <- newEvVar pred ; fillCoercionHole hole (mkCoVarCo ev_id) ; return ev_id } - But that led to new complications becuase of the side effect on the coercion + But that led to new complications because of the side effect on the coercion hole. Much easier just to side-step the issue entirely by not quantifying over equalities. ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -296,7 +296,7 @@ solveImplicationUsingUnsatGiven go_simple ct = case ctEvidence ct of CtWanted (WantedCt { ctev_pred = pty, ctev_dest = dest }) -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty - ; setWantedEvTerm dest EvNonCanonical $ EvExpr ev_expr } + ; setWantedDict dest EvNonCanonical $ EvExpr ev_expr } _ -> return () -- | Create an evidence expression for an arbitrary constraint using ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -476,7 +476,7 @@ solveEqualityDict ev cls tys ; co <- wrapUnifierAndEmit ev role $ \uenv -> uType uenv t1 t2 -- Set d :: (t1~t2) = Eq# co - ; setWantedEvTerm dest EvCanonical $ + ; setWantedDict dest EvCanonical $ evDictApp cls tys [Coercion co] ; stopWith ev "Solved wanted lifted equality" } ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -485,7 +485,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel -- See Note [Solving forall equalities] can_eq_nc_forall ev eq_rel s1 s2 - | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_loc = loc }) <- ev + | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_rewriters = rws, ctev_loc = loc }) <- ev = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2 flags1 = binderFlags bndrs1 flags2 = binderFlags bndrs2 @@ -567,9 +567,9 @@ can_eq_nc_forall ev eq_rel s1 s2 , ic_wanted = emptyWC { wc_simple = wanteds } } ; if solved - then do { zonked_all_co <- zonkCo all_co - -- ToDo: explain this zonk - ; setWantedEq orig_dest zonked_all_co + then do { -- all_co <- zonkCo all_co + -- -- ToDo: explain this zonk + setWantedEq orig_dest rws all_co ; stopWith ev "Polytype equality: solved" } else canEqSoftFailure IrredShapeReason ev s1 s2 } } @@ -809,7 +809,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -- to an irreducible constraint; see typecheck/should_compile/T10494 -- See Note [Decomposing AppTy equalities] can_eq_app ev s1 t1 s2 t2 - | CtWanted (WantedCt { ctev_dest = dest }) <- ev + | CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws }) <- ev = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1 , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2 , text "vis:" <+> ppr (isNextArgVisible s1) ]) @@ -824,7 +824,7 @@ can_eq_app ev s1 t1 s2 t2 ; co_t <- uType arg_env t1 t2 ; co_s <- uType uenv s1 s2 ; return (mkAppCo co_s co_t) } - ; setWantedEq dest co + ; setWantedEq dest rws co ; stopWith ev "Decomposed [W] AppTy" } -- If there is a ForAll/(->) mismatch, the use of the Left coercion @@ -1374,7 +1374,7 @@ canDecomposableTyConAppOK ev eq_rel tc (ty1,tys1) (ty2,tys2) do { traceTcS "canDecomposableTyConAppOK" (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) ; case ev of - CtWanted (WantedCt { ctev_dest = dest }) + CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws }) -- new_locs and tc_roles are both infinite, so we are -- guaranteed that cos has the same length as tys1 and tys2 -- See Note [Fast path when decomposing TyConApps] @@ -1382,7 +1382,7 @@ canDecomposableTyConAppOK ev eq_rel tc (ty1,tys1) (ty2,tys2) do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2 -- zipWith4M: see Note [Work-list ordering] ; return (mkTyConAppCo role tc cos) } - ; setWantedEq dest co } + ; setWantedEq dest rws co } CtGiven (GivenCt { ctev_evar = evar }) | let pred_ty = mkEqPred eq_rel ty1 ty2 @@ -1432,7 +1432,7 @@ canDecomposableFunTy ev eq_rel af f1@(ty1,m1,a1,r1) f2@(ty2,m2,a2,r2) = do { traceTcS "canDecomposableFunTy" (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2) ; case ev of - CtWanted (WantedCt { ctev_dest = dest }) + CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws }) -> do { co <- wrapUnifierAndEmit ev Nominal $ \ uenv -> do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc InvisibleMultiplicity `setUEnvRole` funRole role SelMult @@ -1443,7 +1443,7 @@ canDecomposableFunTy ev eq_rel af f1@(ty1,m1,a1,r1) f2@(ty2,m2,a2,r2) ; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2 ; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2 ; return (mkNakedFunCo role af mult arg res) } - ; setWantedEq dest co } + ; setWantedEq dest rws co } CtGiven (GivenCt { ctev_evar = evar }) | let pred_ty = mkEqPred eq_rel ty1 ty2 @@ -2652,7 +2652,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio ; (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRewriteRole old_ev) nlhs nrhs ; let co = maybeSymCo swapped $ lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co - ; setWantedEq dest co + ; setWantedEq dest rewriters' co ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev , ppr nlhs , ppr nrhs ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad ( newWantedNC, newWantedEvVarNC, newBoundEvVarId, unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications, - setEvBind, setWantedEq, + setEvBind, setWantedEq, setWantedDict, setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEv, emitNewGivens, emitChildEqs, checkReductionDepth, @@ -457,16 +457,15 @@ kickOutAfterUnification tv_set ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked) ; return n_kicked } -kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS () +kickOutAfterFillingCoercionHole :: CoercionHole -> RewriterSet -> TcS () -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty] -- in GHC.Tc.Solver.Equality -- -- It's possible that this could just go ahead and unify, but could there -- be occurs-check problems? Seems simpler just to kick out. -kickOutAfterFillingCoercionHole hole co +kickOutAfterFillingCoercionHole hole new_holes = do { ics <- getInertCans - ; new_holes <- liftZonkTcS $ TcM.freeHolesOfCoercion co - ; let (kicked_out, ics') = kick_out new_holes ics + ; let (kicked_out, ics') = kick_out ics n_kicked = length kicked_out ; unless (n_kicked == 0) $ @@ -479,14 +478,14 @@ kickOutAfterFillingCoercionHole hole co ; setInertCans ics' } where - kick_out :: RewriterSet -> InertCans -> ([EqCt], InertCans) - kick_out new_holes ics@(IC { inert_eqs = eqs }) + kick_out :: InertCans -> ([EqCt], InertCans) + kick_out ics@(IC { inert_eqs = eqs }) = (eqs_to_kick, ics { inert_eqs = eqs_to_keep }) where - (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs (kick_out_eq new_holes) eqs + (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs - kick_out_eq :: RewriterSet -> EqCt -> Either EqCt EqCt - kick_out_eq new_holes eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs }) + kick_out_eq :: EqCt -> Either EqCt EqCt + kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs }) | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev , TyVarLHS tv <- lhs , isMetaTyVar tv @@ -1951,27 +1950,32 @@ addUsedCoercion co = do { ev_binds_var <- getTcEvBindsVar ; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) } --- | Equalities only -setWantedEq :: HasDebugCallStack => TcEvDest -> TcCoercion -> TcS () -setWantedEq (HoleDest hole) co +setWantedEq :: HasDebugCallStack => TcEvDest -> RewriterSet -> TcCoercion -> TcS () +-- ^ Equalities only +setWantedEq (HoleDest hole) rewriters co = do { addUsedCoercion co - ; fillCoercionHole hole co } -setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev) + ; fillCoercionHole hole rewriters co } +setWantedEq (EvVarDest ev) _ _ = pprPanic "setWantedEq: EvVarDest" (ppr ev) --- | Good for both equalities and non-equalities -setWantedEvTerm :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS () -setWantedEvTerm (HoleDest hole) _canonical tm +setWantedDict :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS () +-- ^ Dictionaries only +setWantedDict (EvVarDest ev_id) canonical tm + = setEvBind (mkWantedEvBind ev_id canonical tm) +setWantedDict (HoleDest h) _ _ = pprPanic "setWantedEq: HoleDest" (ppr h) + +setWantedEvTerm :: TcEvDest -> RewriterSet -> CanonicalEvidence -> EvTerm -> TcS () +-- ^ Good for both equalities and non-equalities +setWantedEvTerm (EvVarDest ev_id) _rewriters canonical tm + = setEvBind (mkWantedEvBind ev_id canonical tm) +setWantedEvTerm (HoleDest hole) rewriters _canonical tm | Just co <- evTermCoercion_maybe tm = do { addUsedCoercion co - ; fillCoercionHole hole co } + ; fillCoercionHole hole rewriters co } | otherwise = -- See Note [Yukky eq_sel for a HoleDest] do { let co_var = coHoleCoVar hole ; setEvBind (mkWantedEvBind co_var EvCanonical tm) - ; fillCoercionHole hole (mkCoVarCo co_var) } - -setWantedEvTerm (EvVarDest ev_id) canonical tm - = setEvBind (mkWantedEvBind ev_id canonical tm) + ; fillCoercionHole hole rewriters (mkCoVarCo co_var) } {- Note [Yukky eq_sel for a HoleDest] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1992,16 +1996,17 @@ We even re-use the CoHole's Id for this binding! Yuk! -} -fillCoercionHole :: CoercionHole -> Coercion -> TcS () -fillCoercionHole hole co - = do { wrapTcS $ TcM.fillCoercionHole hole co - ; kickOutAfterFillingCoercionHole hole co } +fillCoercionHole :: CoercionHole -> RewriterSet -> Coercion -> TcS () +fillCoercionHole hole rewriters co + = do { wrapTcS $ TcM.fillCoercionHole hole (co, rewriters) + ; kickOutAfterFillingCoercionHole hole rewriters } setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS () setEvBindIfWanted ev canonical tm = case ev of - CtWanted (WantedCt { ctev_dest = dest }) -> setWantedEvTerm dest canonical tm - _ -> return () + CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) + -> setWantedEvTerm dest rewriters canonical tm + _ -> return () newTcEvBinds :: TcS EvBindsVar newTcEvBinds = wrapTcS TcM.newTcEvBinds ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -1666,7 +1666,7 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev = ev, qci_tvs = tvs -- NB: even if it is fully solved we must return it, because it is -- carrying a record of which evidence variables are used -- See Note [Free vars of EvFun] in GHC.Tc.Types.Evidence - do { setWantedEvTerm dest EvCanonical $ + do { setWantedDict dest EvCanonical $ EvFun { et_tvs = skol_tvs, et_given = given_ev_vars , et_binds = TcEvBinds ev_binds_var , et_body = wantedCtEvEvId wanted_ev } @@ -1761,7 +1761,7 @@ finish_rewrite ev_rw_role = ctEvRewriteRole ev ; mb_new_ev <- newWanted loc rewriters' new_pred ; massert (coercionRole co == ev_rw_role) - ; setWantedEvTerm dest EvCanonical $ + ; setWantedEvTerm dest rewriters' EvCanonical $ evCast (getEvExpr mb_new_ev) $ downgradeRole Representational ev_rw_role (mkSymCo co) ; case mb_new_ev of @@ -1833,7 +1833,8 @@ runTcPluginsWanted wanted where setEv :: (EvTerm,Ct) -> TcS () setEv (ev,ct) = case ctEvidence ct of - CtWanted (WantedCt { ctev_dest = dest }) -> setWantedEvTerm dest EvCanonical ev + CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) + -> setWantedEvTerm dest rewriters EvCanonical ev -- TODO: plugins should be able to signal non-canonicity _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!" ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -90,8 +90,8 @@ module GHC.Tc.Types.Constraint ( -- RewriterSet -- RewriterSet(..) is exported concretely only for zonkRewriterSet RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet, - addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts, - delRewriterSet, + addRewriter, unitRewriterSet, unionRewriterSet, delRewriterSet, + rewriterSetFromCts, wrapType, @@ -128,7 +128,6 @@ import GHC.Tc.Types.CtLoc import GHC.Builtin.Names import GHC.Types.Var.Set -import GHC.Types.Unique.Set import GHC.Types.Name.Reader import GHC.Utils.FV @@ -140,7 +139,6 @@ import GHC.Utils.Constants (debugIsOn) import GHC.Data.Bag import Control.Monad ( when ) -import Data.Coerce import Data.List ( intersperse ) import Data.Maybe ( mapMaybe, isJust ) import GHC.Data.Maybe ( firstJust, firstJusts ) @@ -2395,6 +2393,16 @@ wantedCtHasNoRewriters (WantedCt { ctev_rewriters = rws }) setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence setWantedCtEvRewriters ev rs = ev { ctev_rewriters = rs } +rewriterSetFromCts :: Bag Ct -> RewriterSet +-- Take a bag of Wanted equalities, and collect them as a RewriterSet +rewriterSetFromCts cts + = foldr add emptyRewriterSet cts + where + add ct rw_set = + case ctEvidence ct of + CtWanted (WantedCt { ctev_dest = HoleDest hole }) -> rw_set `addRewriter` hole + _ -> rw_set + ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr ctEvExpr (CtWanted ev@(WantedCt { ctev_dest = HoleDest _ })) = Coercion $ ctEvCoercion (CtWanted ev) @@ -2488,50 +2496,6 @@ isGiven :: CtEvidence -> Bool isGiven (CtGiven {}) = True isGiven _ = False -{- -************************************************************************ -* * - RewriterSet -* * -************************************************************************ --} - --- | Stores a set of CoercionHoles that have been used to rewrite a constraint. --- See Note [Wanteds rewrite Wanteds]. -newtype RewriterSet = RewriterSet (UniqSet CoercionHole) - deriving newtype (Outputable, Semigroup, Monoid) - -emptyRewriterSet :: RewriterSet -emptyRewriterSet = RewriterSet emptyUniqSet - -unitRewriterSet :: CoercionHole -> RewriterSet -unitRewriterSet = coerce (unitUniqSet @CoercionHole) - -elemRewriterSet :: CoercionHole -> RewriterSet -> Bool -elemRewriterSet = coerce (elementOfUniqSet @CoercionHole) - -delRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet -delRewriterSet = coerce (delOneFromUniqSet @CoercionHole) - -unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet -unionRewriterSet = coerce (unionUniqSets @CoercionHole) - -isEmptyRewriterSet :: RewriterSet -> Bool -isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole) - -addRewriter :: RewriterSet -> CoercionHole -> RewriterSet -addRewriter = coerce (addOneToUniqSet @CoercionHole) - -rewriterSetFromCts :: Bag Ct -> RewriterSet --- Take a bag of Wanted equalities, and collect them as a RewriterSet -rewriterSetFromCts cts - = foldr add emptyRewriterSet cts - where - add ct rw_set = - case ctEvidence ct of - CtWanted (WantedCt { ctev_dest = HoleDest hole }) -> rw_set `addRewriter` hole - _ -> rw_set - {- ************************************************************************ * * ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -360,15 +360,14 @@ newCoercionHole pred_ty ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } -- | Put a value in a coercion hole -fillCoercionHole :: CoercionHole -> Coercion -> TcM () -fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co = do - when debugIsOn $ do - cts <- readTcRef ref - whenIsJust cts $ \old_co -> - pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) - traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) - writeTcRef ref (Just co) - +fillCoercionHole :: CoercionHole -> (Coercion, RewriterSet) -> TcM () +fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co + = do { when debugIsOn $ + do { cts <- readTcRef ref + ; whenIsJust cts $ \old_co -> + pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) } + ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) + ; writeTcRef ref (Just co) } {- ********************************************************************** * @@ -1546,8 +1545,8 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co go_co dv (HoleCo hole) = do m_co <- liftZonkM (unpackCoercionHole_maybe hole) case m_co of - Just co -> go_co dv co - Nothing -> go_cv dv (coHoleCoVar hole) + Just (co,_) -> go_co dv co + Nothing -> go_cv dv (coHoleCoVar hole) go_co dv (CoVarCo cv) = go_cv dv cv ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -43,8 +43,6 @@ module GHC.Tc.Zonk.TcType -- * Coercion holes , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe - , freeHolesOfCoercion - -- * Tidying , tcInitTidyEnv, tcInitOpenTidyEnv @@ -241,8 +239,8 @@ zonkCo :: Coercion -> ZonkM Coercion hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) = do { contents <- readTcRef ref ; case contents of - Just co -> do { co' <- zonkCo co - ; checkCoercionHole cv co' } + Just (co,_) -> do { co' <- zonkCo co + ; checkCoercionHole cv co' } Nothing -> do { cv' <- zonkCoVar cv ; return $ HoleCo (hole { ch_co_var = cv' }) } } @@ -592,26 +590,12 @@ zonkRewriterSet (RewriterSet set) go :: CoercionHole -> UnfilledCoercionHoleMonoid -> UnfilledCoercionHoleMonoid go hole m_acc = freeHolesOfHole hole `mappend` m_acc -freeHolesOfCoercion :: Coercion -> ZonkM RewriterSet -freeHolesOfCoercion co = unUCHM (freeHolesOfCo co) - freeHolesOfHole :: CoercionHole -> UnfilledCoercionHoleMonoid freeHolesOfHole hole = UCHM $ do { m_co <- unpackCoercionHole_maybe hole ; case m_co of Nothing -> return (unitRewriterSet hole) -- Not filled - Just co -> unUCHM (freeHolesOfCo co) } -- Filled: look inside - -freeHolesOfTy :: Type -> UnfilledCoercionHoleMonoid -freeHolesOfCo :: Coercion -> UnfilledCoercionHoleMonoid -(freeHolesOfTy, _, freeHolesOfCo, _) = foldTyCo freeHolesFolder () - -freeHolesFolder :: TyCoFolder () UnfilledCoercionHoleMonoid -freeHolesFolder = TyCoFolder { tcf_view = noView - , tcf_tyvar = \ _ tv -> freeHolesOfTy (tyVarKind tv) - , tcf_covar = \ _ cv -> freeHolesOfTy (varType cv) - , tcf_hole = \ _ h -> freeHolesOfHole h - , tcf_tycobinder = \ _ _ _ -> () } + Just (_co,holes) -> zonkRewriterSet holes } newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet } @@ -641,11 +625,11 @@ unpackCoercionHole :: CoercionHole -> ZonkM Coercion unpackCoercionHole hole = do { contents <- unpackCoercionHole_maybe hole ; case contents of - Just co -> return co + Just (co,_) -> return co Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } -- | Retrieve the contents of a coercion hole, if it is filled -unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe Coercion) +unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe (Coercion,RewriterSet)) unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -488,8 +488,8 @@ zonkCoHole :: CoercionHole -> ZonkTcM Coercion zonkCoHole hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) = do { contents <- readTcRef ref ; case contents of - Just co -> do { co' <- zonkCoToCo co - ; lift $ liftZonkM $ checkCoercionHole cv co' } + Just (co,_) -> do { co' <- zonkCoToCo co + ; lift $ liftZonkM $ checkCoercionHole cv co' } -- This next case should happen only in the presence of -- (undeferred) type errors. Originally, I put in a panic View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5cf99a788eb64bf7289aa4fa0546a955... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5cf99a788eb64bf7289aa4fa0546a955... You're receiving this email because of your account on gitlab.haskell.org.