Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 058b40f2 by Simon Peyton Jones at 2025-10-16T15:34:26+01:00 More tidying up of rewriter sets - - - - - 17 changed files: - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Runtime/Eval.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Irred.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Rewrite.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/TcType.hs - testsuite/tests/quantified-constraints/T15359.hs Changes: ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -42,10 +42,10 @@ 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, + -- CoHoleSet + -- CoHoleSet(..) is exported concretely only for zonkCoHoleSet + CoHoleSet(..), emptyCoHoleSet, isEmptyCoHoleSet, elemCoHoleSet, + addRewriter, unitCoHoleSet, unionCoHoleSet, delCoHoleSet, -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, @@ -1680,7 +1680,7 @@ holes `HoleCo`, which get filled in later. {- ********************************************************************** %* * - Coercion holes and RewriterSets + Coercion holes and CoHoleSets %* * %********************************************************************* -} @@ -1689,9 +1689,10 @@ data CoercionHole = CoercionHole { ch_co_var :: CoVar -- See Note [CoercionHoles and coercion free variables] - , ch_ref :: IORef (Maybe (Coercion, RewriterSet)) - -- The RewriterSet is (possibly a superset of) + , ch_ref :: IORef (Maybe (Coercion, CoHoleSet)) + -- The CoHoleSet is (possibly a superset of) -- the free coercion holes of the coercion + -- See Note [Want } coHoleCoVar :: CoercionHole -> CoVar @@ -1713,30 +1714,30 @@ 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 CoHoleSet 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) +newtype CoHoleSet = CoHoleSet (UniqSet CoercionHole) deriving newtype (Outputable, Semigroup, Monoid) -emptyRewriterSet :: RewriterSet -emptyRewriterSet = RewriterSet emptyUniqSet +emptyCoHoleSet :: CoHoleSet +emptyCoHoleSet = CoHoleSet emptyUniqSet -unitRewriterSet :: CoercionHole -> RewriterSet -unitRewriterSet = coerce (unitUniqSet @CoercionHole) +unitCoHoleSet :: CoercionHole -> CoHoleSet +unitCoHoleSet = coerce (unitUniqSet @CoercionHole) -elemRewriterSet :: CoercionHole -> RewriterSet -> Bool -elemRewriterSet = coerce (elementOfUniqSet @CoercionHole) +elemCoHoleSet :: CoercionHole -> CoHoleSet -> Bool +elemCoHoleSet = coerce (elementOfUniqSet @CoercionHole) -delRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet -delRewriterSet = coerce (delOneFromUniqSet @CoercionHole) +delCoHoleSet :: CoHoleSet -> CoercionHole -> CoHoleSet +delCoHoleSet = coerce (delOneFromUniqSet @CoercionHole) -unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet -unionRewriterSet = coerce (unionUniqSets @CoercionHole) +unionCoHoleSet :: CoHoleSet -> CoHoleSet -> CoHoleSet +unionCoHoleSet = coerce (unionUniqSets @CoercionHole) -isEmptyRewriterSet :: RewriterSet -> Bool -isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole) +isEmptyCoHoleSet :: CoHoleSet -> Bool +isEmptyCoHoleSet = coerce (isEmptyUniqSet @CoercionHole) -addRewriter :: RewriterSet -> CoercionHole -> RewriterSet +addRewriter :: CoHoleSet -> CoercionHole -> CoHoleSet addRewriter = coerce (addOneToUniqSet @CoercionHole) {- Note [Coercion holes] @@ -1821,14 +1822,14 @@ Why does a CoercionHole contain a CoVar, as well as reference to fill in? But nowadays this is all irrelevant because we don't float constraints. -Note [CoercionHoles and RewriterSets] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [CoercionHoles and CoHoleSets] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 +If C is an equality constraint and is solved, we track its CoHoleSet in the filled CoercionHole, so that it can be inherited by other constraints that have C in /their/ -rewriters. See zonkRewriterSet. +rewriters. See zonkCoHoleSet. -} ===================================== compiler/GHC/Runtime/Eval.hs ===================================== @@ -1118,7 +1118,7 @@ getDictionaryBindings theta = do ctev_pred = varType dict_var, ctev_dest = EvVarDest dict_var, ctev_loc = loc, - ctev_rewriters = emptyRewriterSet + ctev_rewriters = emptyCoHoleSet } -- Find instances where the head unifies with the provided type ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -462,7 +462,7 @@ mkErrorItem ct -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint CtGiven {} -> (False, Nothing) CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) - -> (not (isEmptyRewriterSet rws), Just dest) + -> (not (isEmptyCoHoleSet rws), Just dest) ; let m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason @@ -494,7 +494,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- Catch an awkward (and probably rare) case in which /all/ errors are -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty - -- RewriterSet] in GHC.Tc.Types.Constraint. + -- CoHoleSet] in GHC.Tc.Types.Constraint. -- -- Unless we are sure that an error will be reported some other way -- (details in the defn of tidy_items) un-suppress the lot. This makes @@ -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, emptyRewriterSet) } } + ; fillCoercionHole hole (mkCoVarCo co_var, emptyCoHoleSet) } } addDeferredBinding _ _ _ _ _ = return () -- Do not set any evidence for Given mkSolverErrorTerm :: CtLoc -> Type -- of the error term @@ -1650,7 +1650,7 @@ validHoleFits ctxt@(CEC { cec_encl = implics WantedCt { ctev_pred = pred , ctev_dest = dest , ctev_loc = loc - , ctev_rewriters = emptyRewriterSet } + , ctev_rewriters = emptyCoHoleSet } | otherwise = Nothing -- The ErrorItem was a Given ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -541,7 +541,7 @@ defaultEquality encl_eqs ct = do { traceTcS "defaultEquality success:" (ppr rhs_ty) ; unifyTyVar lhs_tv rhs_ty -- NB: unifyTyVar adds to the -- TcS unification counter - ; setEqIfWanted (ctEvidence ct) emptyRewriterSet (mkReflCo Nominal rhs_ty) + ; setEqIfWanted (ctEvidence ct) emptyCoHoleSet (mkReflCo Nominal rhs_ty) ; return True } @@ -566,7 +566,7 @@ defaultEquality encl_eqs ct -- See Note [Defaulting representational equalities]. ; if null new_eqs then do { traceTcS "defaultEquality ReprEq } (yes)" empty - ; setEqIfWanted (ctEvidence ct) emptyRewriterSet (mkSubCo co) + ; setEqIfWanted (ctEvidence ct) emptyCoHoleSet (mkSubCo co) ; return True } else do { traceTcS "defaultEquality ReprEq } (no)" empty ; return False } } ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -796,12 +796,15 @@ tryInstances dict_ct try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ()) -- Try to use type-class instance declarations to simplify the constraint -try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls - , di_tys = xis }) - | isGiven ev -- Never use instances for Given constraints - = continueWith () - -- See Note [No Given/Given fundeps] +-- Case for Givens +-- Never use instances for Given constraints +try_instances _ (DictCt { di_ev = CtGiven {} }) + = -- See Note [No Given/Given fundeps] + continueWith () + +-- Case for Wanteds +try_instances inerts work_item@(DictCt { di_ev = ev@(CtWanted wev), di_cls = cls, di_tys = xis }) | Just solved_ev <- lookupSolvedDict inerts cls xis -- Cached = do { setDictIfWanted ev EvCanonical (ctEvTerm solved_ev) ; stopWith ev "Dict/Top (cached)" } @@ -817,14 +820,16 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls then stopWith ev "shortCutSolver worked(2)" else do { insertSafeOverlapFailureTcS what work_item ; updSolvedDicts what work_item - ; chooseInstance ev lkup_res } } + ; chooseInstance wev lkup_res + ; stopWith ev "Dict/Top (solved wanted)" } } _ -> -- NoInstance or NotSure: we didn't solve it continueWith () } where dict_loc = ctEvLoc ev -chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue a) -chooseInstance work_item +chooseInstance :: WantedCtEvidence -> ClsInstResult -> TcS () +chooseInstance work_item@(WantedCt { ctev_dest = dest, ctev_rewriters = rws + , ctev_loc = loc, ctev_pred = pred }) (OneInst { cir_new_theta = theta , cir_what = what , cir_mk_ev = mk_ev @@ -834,13 +839,9 @@ chooseInstance work_item ; checkReductionDepth deeper_loc pred ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar) (ppr work_item) - ; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta - ; setDictIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars)) - ; emitWorkNC (map CtWanted $ freshGoals evc_vars) - ; stopWith work_item "Dict/Top (solved wanted)" } - where - pred = ctEvPred work_item - loc = ctEvLoc work_item + ; evc_vars <- mapM (newWanted deeper_loc rws) theta + ; setWantedDict dest canonical (mk_ev (map getEvExpr evc_vars)) + ; emitWorkNC (map CtWanted $ freshGoals evc_vars) } chooseInstance work_item lookup_res = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res) ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -372,7 +372,7 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ -- Literals can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ | l1 == l2 - = do { setEqIfWanted ev emptyRewriterSet (mkReflCo (eqRelRole eq_rel) ty1) + = do { setEqIfWanted ev emptyCoHoleSet (mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } -- Decompose FunTy: (s -> t) and (c => t) @@ -571,8 +571,8 @@ can_eq_nc_forall ev eq_rel s1 s2 -- CoercionHoles, from the nested solve, and we may miss the -- use of CoVars. Test T7196 showed this up - ; setWantedEq orig_dest emptyRewriterSet all_co - -- emptyRewriterSet: fully solved, so all_co has no holes + ; setWantedEq orig_dest emptyCoHoleSet all_co + -- emptyCoHoleSet: fully solved, so all_co has no holes ; stopWith ev "Polytype equality: solved" } else canEqSoftFailure IrredShapeReason ev s1 s2 } } @@ -792,7 +792,7 @@ can_eq_newtype_nc rdr_env envs ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 ; let redn1 = mkReduction co1 ty1' - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev' swapped redn1 (mkReflRedn Representational ps_ty2) ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 } @@ -872,7 +872,7 @@ canEqCast rewritten rdr_env envs ev eq_rel swapped ty1 co1 ty2 ps_ty2 = do { traceTcS "Decomposing cast" (vcat [ ppr ev , ppr ty1 <+> text "|>" <+> ppr co1 , ppr ps_ty2 ]) - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev swapped (mkGReflLeftRedn role ty1 co1) (mkReflRedn role ps_ty2) ; can_eq_nc rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 } @@ -1678,7 +1678,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 kind_loc = mkKindEqLoc xi1 xi2 loc ; kind_ev <- newGivenEv kind_loc (pred_ty, evCoercion kind_co) ; emitWorkNC [CtGiven kind_ev] - ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) } + ; finish emptyCoHoleSet (givenCtEvCoercion kind_ev) } CtWanted {} -> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $ @@ -1830,7 +1830,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco finish_with_swapping = do { let lhs1_redn = mkGReflRightMRedn role lhs1_ty sym_mco lhs2_redn = mkGReflLeftMRedn role lhs2_ty mco - ; new_ev <-rewriteEqEvidence emptyRewriterSet ev swapped lhs1_redn lhs2_redn + ; new_ev <-rewriteEqEvidence emptyCoHoleSet ev swapped lhs1_redn lhs2_redn ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) } put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq @@ -1967,7 +1967,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- ContinueWith, to allow using this constraint for -- rewriting (e.g. alpha[2] ~ beta[3]). do { let role = eqRelRole eq_rel - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev swapped (mkReflRedn role (canEqLHSType lhs)) (mkReflRedn role rhs) ; continueWith $ Right $ @@ -2010,9 +2010,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- co' = <Int> new_ev <- if isReflCo (reductionCoercion rhs_redn) then return ev - else rewriteEqEvidence emptyRewriterSet ev swapped + else rewriteEqEvidence emptyCoHoleSet ev swapped (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn - -- emptyRewriterSet: rhs_redn has no CoercionHoles + -- emptyCoHoleSet: rhs_redn has no CoercionHoles ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn @@ -2028,7 +2028,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- Provide Refl evidence for the constraint -- Ignore 'swapped' because it's Refl! - ; setEqIfWanted new_ev emptyRewriterSet (mkNomReflCo final_rhs) + ; setEqIfWanted new_ev emptyCoHoleSet (mkNomReflCo final_rhs) -- Kick out any constraints that can now be rewritten ; kickOutAfterUnification (unitVarSet tv) @@ -2062,7 +2062,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs | reason `cterHasOnlyProblems` do_not_prevent_rewriting -> do { let role = eqRelRole eq_rel - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev swapped (mkReflRedn role (canEqLHSType lhs)) (mkReflRedn role rhs) ; continueWith $ Right $ @@ -2074,7 +2074,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -> tryIrredInstead reason ev eq_rel swapped lhs rhs PuOK _ rhs_redn - -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + -> do { new_ev <- rewriteEqEvidence emptyCoHoleSet ev swapped (mkReflRedn (eqRelRole eq_rel) lhs_ty) rhs_redn @@ -2108,7 +2108,7 @@ swapAndFinish :: CtEvidence -> EqRel -> SwapFlag -- We want to flip it to (F tys ~ a), whereupon it is canonical swapAndFinish ev eq_rel swapped lhs_ty can_rhs = do { let role = eqRelRole eq_rel - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped) + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev (flipSwap swapped) (mkReflRedn role (canEqLHSType can_rhs)) (mkReflRedn role lhs_ty) ; continueWith $ Right $ @@ -2127,7 +2127,7 @@ tryIrredInstead :: CheckTyEqResult -> CtEvidence tryIrredInstead reason ev eq_rel swapped lhs rhs = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs) ; let role = eqRelRole eq_rel - ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + ; new_ev <- rewriteEqEvidence emptyCoHoleSet ev swapped (mkReflRedn role (canEqLHSType lhs)) (mkReflRedn role rhs) ; finishCanWithIrred (NonCanonicalReason reason) new_ev } @@ -2148,7 +2148,7 @@ canEqReflexive :: CtEvidence -- ty ~ ty -> TcType -- ty -> TcS (StopOrContinue a) -- always Stop canEqReflexive ev eq_rel ty - = do { setEqIfWanted ev emptyRewriterSet (mkReflCo (eqRelRole eq_rel) ty) + = do { setEqIfWanted ev emptyCoHoleSet (mkReflCo (eqRelRole eq_rel) ty) ; stopWith ev "Solved by reflexivity" } {- Note [Equalities with heterogeneous kinds] @@ -2171,7 +2171,7 @@ k2 and use this to cast. To wit, from Wrinkles: (EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by - the kind-level one. We thus include the kind-level wanted in the RewriterSet + the kind-level one. We thus include the kind-level wanted in the CoHoleSet for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. This is done in canEqCanLHSHetero. @@ -2199,7 +2199,7 @@ Wrinkles: the kind of the parent type-equality. See the calls to `mkKindEqLoc` in `canEqCanLHSHetero`. - * We /also/ add these unsolved kind equalities to the `RewriterSet` of the + * We /also/ add these unsolved kind equalities to the `CoHoleSet` of the parent constraint; see the call to `rewriteEqEvidence` in `finish` in `canEqCanLHSHetero`. @@ -2611,7 +2611,7 @@ More details: ********************************************************************** -} -rewriteEqEvidence :: RewriterSet -- New rewriters +rewriteEqEvidence :: CoHoleSet -- New rewriters -- See GHC.Tc.Types.Constraint -- Note [Wanteds rewrite Wanteds] -> CtEvidence -- Old evidence :: olhs ~ orhs (not swapped) @@ -2653,7 +2653,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio ; let co = maybeSymCo swapped $ lhs_co `mkTransCo` mkHoleCo hole `mkTransCo` mkSymCo rhs_co -- new_rewriters has all the holes from lhs_co and rhs_co - ; setWantedEq dest (new_rewriters `mappend` unitRewriterSet hole) co + ; setWantedEq dest (new_rewriters `mappend` unitCoHoleSet hole) co ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev , ppr nlhs , ppr nrhs @@ -2723,7 +2723,7 @@ But it's not so simple: TL;DR: Better to hang on to `g1` (with no rewriters), in preference to `g2` (which has a rewriter). - See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. + See (WRW11) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. -} tryInertEqs :: EqCt -> SolverStage () @@ -2731,7 +2731,7 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel }) = Stage $ do { inerts <- getInertCans ; if | Just (ev_i, swapped) <- inertsEqsCanDischarge inerts work_item - -> do { setEqIfWanted ev (ctEvRewriterSet ev_i) $ + -> do { setEqIfWanted ev (ctEvCoHoleSet ev_i) $ maybeSymCo swapped $ downgradeRole (eqRelRole eq_rel) (ctEvRewriteRole ev_i) @@ -2769,7 +2769,7 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w loc_w = ctEvLoc ev_w flav_w = ctEvFlavour ev_w fr_w = (flav_w, eq_rel) - empty_rw_w = isEmptyRewriterSet (ctEvRewriters ev_w) + empty_rw_w = isEmptyCoHoleSet (ctEvRewriters ev_w) inert_beats_wanted ev_i eq_rel = -- eqCanRewriteFR: see second bullet of Note [Combining equalities] @@ -2786,7 +2786,7 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w prefer_wanted ev_i = (loc_w `strictly_more_visible` ctEvLoc ev_i) -- strictly_more_visible: see (CE3) in Note [Combining equalities] - || (empty_rw_w && not (isEmptyRewriterSet (ctEvRewriters ev_i))) + || (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i))) -- Prefer the one that has no rewriters -- See (CE4) in Note [Combining equalities] @@ -2862,7 +2862,7 @@ Wrinkles: However the solver prioritises equalities with an empty rewriter set, to try to avoid unnecessary kick-out. See GHC.Tc.Types.Constraint - Note [Prioritise Wanteds with empty RewriterSet] esp (PER1) + Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1) Note [Solve by unification] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2914,9 +2914,9 @@ See -------------------- tryQCsIrredEqCt :: IrredCt -> SolverStage () -tryQCsIrredEqCt irred@(IrredCt { ir_ev = ev }) +tryQCsIrredEqCt (IrredCt { ir_ev = ev }) | EqPred eq_rel t1 t2 <- classifyPredType (ctEvPred ev) - = lookup_eq_in_qcis (CIrredCan irred) eq_rel t1 t2 + = lookup_eq_in_qcis ev eq_rel t1 t2 | otherwise -- All the calls come from in this module, where we deal only with -- equalities, so ctEvPred ev) must be an equality. Indeed, we could @@ -2926,62 +2926,61 @@ tryQCsIrredEqCt irred@(IrredCt { ir_ev = ev }) -------------------- tryQCsEqCt :: EqCt -> SolverStage () -tryQCsEqCt work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel }) - = lookup_eq_in_qcis (CEqCan work_item) eq_rel (canEqLHSType lhs) rhs +tryQCsEqCt (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel }) + = lookup_eq_in_qcis ev eq_rel (canEqLHSType lhs) rhs -------------------- -lookup_eq_in_qcis :: Ct -> EqRel -> TcType -> TcType -> SolverStage () +lookup_eq_in_qcis :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage () -- The "final QCI check" checks to see if we have -- [W] t1 ~# t2 -- and a Given quantified contraint like (forall a b. blah => a ~ b) -- Why? See Note [Looking up primitive equalities in quantified constraints] -- See also GHC.Tc.Solver.Dict -- Note [Equality superclasses in quantified constraints] -lookup_eq_in_qcis work_ct eq_rel lhs rhs - = Stage $ - do { ev_binds_var <- getTcEvBindsVar - ; ics <- getInertCans - ; if isWanted ev -- Never look up Givens in quantified constraints - && not (null (inert_qcis ics)) -- Shortcut common case - && not (isCoEvBindsVar ev_binds_var) -- See Note [Instances in no-evidence implications] - then try_for_qci - else continueWith () } +lookup_eq_in_qcis (CtGiven {}) _ _ _ + = nopStage () + +lookup_eq_in_qcis ev@(CtWanted (WantedCt { ctev_dest = dest, ctev_loc = loc })) eq_rel lhs rhs + = do { ev_binds_var <- simpleStage getTcEvBindsVar + ; ics <- simpleStage getInertCans + ; if null (inert_qcis ics) + || isCoEvBindsVar ev_binds_var -- See Note [Instances in no-evidence implications] + then -- Shortcut common case + nopStage () + else -- Try looking for both (lhs~rhs) anr (rhs~lhs); see #23333 + do { try NotSwapped; try IsSwapped } } where - ev = ctEvidence work_ct - loc = ctEvLoc ev - role = eqRelRole eq_rel - - try_for_qci -- First try looking for (lhs ~ rhs) - | Just (cls, tys) <- boxEqPred eq_rel lhs rhs - = do { res <- matchLocalInst (mkClassPred cls tys) loc - ; traceTcS "lookup_irred_in_qcis:1" (ppr (mkClassPred cls tys)) + hole = case dest of + HoleDest hole -> hole -- Equality constraints have HoleDest + _ -> pprPanic "lookup_eq_in_qcis" (ppr dest) + + try :: SwapFlag -> SolverStage () + try swap -- First try looking for (lhs ~ rhs) + | Just (cls, tys) <- unSwap swap (boxEqPred eq_rel) lhs rhs + = Stage $ + do { let cls_pred = mkClassPred cls tys + ; res <- matchLocalInst cls_pred loc + ; traceTcS "lookup_eq_in_qcis:1" (ppr cls_pred) ; case res of - OneInst { cir_mk_ev = mk_ev } - -> chooseInstance ev (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) - _ -> try_swapping } - | otherwise - = continueWith () + OneInst {} + -> do { dict_ev <- newWantedEvVarNC loc emptyCoHoleSet cls_pred + ; chooseInstance dict_ev res + ; let co_var = coHoleCoVar hole + ; setEvBind (mkWantedEvBind co_var EvCanonical (mk_sc_sel cls tys dict_ev)) + ; fillCoercionHole hole emptyCoHoleSet $ + maybeSymCo swap (mkCoVarCo co_var) + ; stopWith ev "lookup_eq_in_qcis" } + _ -> continueWith () } - try_swapping -- Now try looking for (rhs ~ lhs) (see #23333) - | Just (cls, tys) <- boxEqPred eq_rel rhs lhs - = do { res <- matchLocalInst (mkClassPred cls tys) loc - ; traceTcS "lookup_irred_in_qcis:2" (ppr (mkClassPred cls tys)) - ; case res of - OneInst { cir_mk_ev = mk_ev } - -> do { ev' <- rewriteEqEvidence emptyRewriterSet ev IsSwapped - (mkReflRedn role rhs) (mkReflRedn role lhs) - ; chooseInstance ev' (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) } - _ -> do { traceTcS "lookup_irred_in_qcis:3" (ppr work_ct) - ; continueWith () }} | otherwise - = continueWith () - - mk_eq_ev cls tys mk_ev evs - | sc_id : rest <- classSCSelIds cls -- Just one superclass for this - = assert (null rest) $ case (mk_ev evs) of - EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e) - ev -> pprPanic "mk_eq_ev" (ppr ev) - | otherwise = pprPanic "finishEqCt" (ppr work_ct) + = nopStage () + + mk_sc_sel cls tys dict_ev + | [sc_id] <- classSCSelIds cls -- Just one superclass for this + = EvExpr (Var sc_id `mkTyApps` tys `App` Var (wantedCtEvEvId dict_ev)) + | otherwise + = pprPanic "looup_eq_in_qcis" (ppr dict_ev) + {- Note [Instances in no-evidence implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -171,7 +171,7 @@ data WorkList , wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that may have a non-empty -- rewriter set -- We prioritise wl_eqs over wl_rw_eqs; - -- see Note [Prioritise Wanteds with empty RewriterSet] + -- see Note [Prioritise Wanteds with empty CoHoleSet] -- in GHC.Tc.Types.Constraint for more details. , wl_rest :: [Ct] @@ -200,11 +200,11 @@ workListSize :: WorkList -> Int workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest }) = length eqs_N + length eqs_X + length rw_eqs + length rest -extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList +extendWorkListEq :: CoHoleSet -> Ct -> WorkList -> WorkList extendWorkListEq rewriters ct wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs }) - | isEmptyRewriterSet rewriters -- A wanted that has not been rewritten - -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + | isEmptyCoHoleSet rewriters -- A wanted that has not been rewritten + -- isEmptyCoHoleSet: see Note [Prioritise Wanteds with empty CoHoleSet] -- in GHC.Tc.Types.Constraint = if isNominalEqualityCt ct then wl { wl_eqs_N = ct : eqs_N } @@ -223,8 +223,8 @@ extendWorkListChildEqs :: CtEvidence -> Bag Ct -> WorkList -> WorkList -- Precondition: new_eqs is non-empty extendWorkListChildEqs parent_ev new_eqs wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs }) - | isEmptyRewriterSet (ctEvRewriters parent_ev) - -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + | isEmptyCoHoleSet (ctEvRewriters parent_ev) + -- isEmptyCoHoleSet: see Note [Prioritise Wanteds with empty CoHoleSet] -- in GHC.Tc.Types.Constraint -- If the rewriter set is empty, add to wl_eqs_X and wl_eqs_N = case partitionBag isNominalEqualityCt new_eqs of @@ -244,7 +244,7 @@ extendWorkListChildEqs parent_ev new_eqs push_on_front new_eqs eqs = foldr (:) eqs new_eqs extendWorkListRewrittenEqs :: [EqCt] -> WorkList -> WorkList --- Don't bother checking the RewriterSet: just pop them into wl_rw_eqs +-- Don't bother checking the CoHoleSet: just pop them into wl_rw_eqs extendWorkListRewrittenEqs new_eqs wl@(WL { wl_rw_eqs = rw_eqs }) = wl { wl_rw_eqs = foldr ((:) . CEqCan) rw_eqs new_eqs } @@ -2007,7 +2007,7 @@ solveOneFromTheOther ct_i ct_w -- If only one has an empty rewriter set, use it -- c.f. GHC.Tc.Solver.Equality.inertsCanDischarge, and especially -- (CE4) in Note [Combining equalities] - | Just res <- better (isEmptyRewriterSet rw_i) (isEmptyRewriterSet rw_w) + | Just res <- better (isEmptyCoHoleSet rw_i) (isEmptyCoHoleSet rw_w) -> res -- If only one is a WantedSuperclassOrigin (arising from expanding ===================================== compiler/GHC/Tc/Solver/Irred.hs ===================================== @@ -1,3 +1,4 @@ +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RecursiveDo #-} @@ -85,7 +86,7 @@ setIrredIfWanted :: CtEvidence -> SwapFlag -> CtEvidence -> TcS () setIrredIfWanted ev_dest swap ev_source | CtWanted (WantedCt { ctev_dest = dest }) <- ev_dest = case dest of - HoleDest {} -> setWantedEq dest (ctEvRewriterSet ev_source) + HoleDest {} -> setWantedEq dest (ctEvCoHoleSet ev_source) (maybeSymCo swap (ctEvCoercion ev_source)) EvVarDest {} -> assertPpr (swap==NotSwapped) (ppr ev_dest $$ ppr ev_source) $ @@ -133,14 +134,12 @@ tryQCsIrredCt :: IrredCt -> SolverStage () -- Try local quantified constraints for -- and CIrredCan e.g. (c a) tryQCsIrredCt (IrredCt { ir_ev = ev }) - | isGiven ev - = Stage $ continueWith () - - | otherwise - = Stage $ do { res <- matchLocalInst pred loc - ; case res of - OneInst {} -> chooseInstance ev res - _ -> continueWith () } - where - loc = ctEvLoc ev - pred = ctEvPred ev + = Stage $ case ev of + CtGiven {} + -> continueWith () + CtWanted wev@(WantedCt { ctev_loc = loc, ctev_pred = pred }) + -> do { res <- matchLocalInst pred loc + ; case res of + OneInst {} -> do { chooseInstance wev res + ; stopWith ev "Irred (solved wanted)" } + _ -> continueWith () } ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -56,6 +56,7 @@ module GHC.Tc.Solver.Monad ( newBoundEvVarId, unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications, setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted, + fillCoercionHole, newEvVar, newGivenEv, emitNewGivens, emitChildEqs, checkReductionDepth, @@ -456,7 +457,7 @@ kickOutAfterUnification tv_set ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked) ; return n_kicked } -kickOutAfterFillingCoercionHole :: CoercionHole -> RewriterSet -> TcS () +kickOutAfterFillingCoercionHole :: CoercionHole -> CoHoleSet -> TcS () -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty] -- in GHC.Tc.Solver.Equality -- @@ -488,10 +489,10 @@ kickOutAfterFillingCoercionHole hole new_holes | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev , TyVarLHS tv <- lhs , isMetaTyVar tv - , hole `elemRewriterSet` rewriters - , let holes' = (rewriters `delRewriterSet` hole) `mappend` new_holes + , hole `elemCoHoleSet` rewriters + , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) } - = if isEmptyRewriterSet holes' + = if isEmptyCoHoleSet holes' then Left eq_ct' -- Kick out else Right eq_ct' -- Keep, but with trimmed holes | otherwise @@ -1736,7 +1737,7 @@ selectNextWorkItem :: TcS (Maybe Ct) -- -- Suppose a constraint c1 is rewritten by another, c2. When c2 -- gets solved, c1 has no rewriters, and can be prioritised; see --- Note [Prioritise Wanteds with empty RewriterSet] in +-- Note [Prioritise Wanteds with empty CoHoleSet] in -- GHC.Tc.Types.Constraint wrinkle (PER1) -- ToDo: if wl_rw_eqs is long, we'll re-zonk it each time we pick @@ -1761,7 +1762,7 @@ selectNextWorkItem -- try_rws looks through rw_eqs to find one that has an empty -- rewriter set, after zonking. If none such, call try_rest. try_rws acc (ct:cts) - = do { ct' <- liftZonkTcS (TcM.zonkCtRewriterSet ct) + = do { ct' <- liftZonkTcS (TcM.zonkCtCoHoleSet ct) ; if ctHasNoRewriters ct' then pick_me ct' (wl { wl_rw_eqs = cts ++ acc }) else try_rws (ct':acc) cts } @@ -1959,14 +1960,14 @@ addUsedCoercion co = do { ev_binds_var <- getTcEvBindsVar ; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) } -setEqIfWanted :: CtEvidence -> RewriterSet -> TcCoercion -> TcS () +setEqIfWanted :: CtEvidence -> CoHoleSet -> TcCoercion -> TcS () setEqIfWanted ev rewriters co = case ev of CtWanted (WantedCt { ctev_dest = dest }) -> setWantedEq dest rewriters co _ -> return () -setWantedEq :: HasDebugCallStack => TcEvDest -> RewriterSet -> TcCoercion -> TcS () +setWantedEq :: HasDebugCallStack => TcEvDest -> CoHoleSet -> TcCoercion -> TcS () -- ^ Equalities only setWantedEq dest rewriters co = case dest of @@ -1987,7 +1988,7 @@ setWantedDict dest canonical tm EvVarDest ev_id -> setEvBind (mkWantedEvBind ev_id canonical tm) HoleDest h -> pprPanic "setWantedEq: HoleDest" (ppr h) -fillCoercionHole :: CoercionHole -> RewriterSet -> Coercion -> TcS () +fillCoercionHole :: CoercionHole -> CoHoleSet -> Coercion -> TcS () fillCoercionHole hole rewriters co = do { addUsedCoercion co ; wrapTcS $ TcM.fillCoercionHole hole (co, rewriters) @@ -2046,7 +2047,7 @@ emitChildEqs ev eqs -- | Create a new Wanted constraint holding a coercion hole -- for an equality between the two types at the given 'Role'. -newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType +newWantedEq :: CtLoc -> CoHoleSet -> Role -> TcType -> TcType -> TcS (WantedCtEvidence, CoercionHole) newWantedEq loc rewriters role ty1 ty2 = do { hole <- wrapTcS $ TcM.newCoercionHole pty @@ -2061,7 +2062,7 @@ newWantedEq loc rewriters role ty1 ty2 -- | Create a new Wanted constraint holding an evidence variable. -- -- Don't use this for equality constraints: use 'newWantedEq' instead. -newWantedEvVarNC :: CtLoc -> RewriterSet +newWantedEvVarNC :: CtLoc -> CoHoleSet -> TcPredType -> TcS WantedCtEvidence -- Don't look up in the solved/inerts; we know it's not there newWantedEvVarNC loc rewriters pty @@ -2085,7 +2086,7 @@ newWantedEvVarNC loc rewriters pty -- -- Don't use this for equality constraints: this function is only for -- constraints with 'EvVarDest'. -newWantedEvVar :: CtLoc -> RewriterSet +newWantedEvVar :: CtLoc -> CoHoleSet -> TcPredType -> TcS MaybeNew newWantedEvVar loc rewriters pty = case classifyPredType pty of @@ -2105,7 +2106,7 @@ newWantedEvVar loc rewriters pty -- a new one from scratch. -- -- Deals with both equality and non-equality constraints. -newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew +newWanted :: CtLoc -> CoHoleSet -> PredType -> TcS MaybeNew newWanted loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty = Fresh . fst <$> newWantedEq loc rewriters role ty1 ty2 @@ -2118,7 +2119,7 @@ newWanted loc rewriters pty -- -- Does not attempt to re-use non-equality constraints that already -- exist in the inert set. -newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS WantedCtEvidence +newWantedNC :: CtLoc -> CoHoleSet -> PredType -> TcS WantedCtEvidence newWantedNC loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty = fst <$> newWantedEq loc rewriters role ty1 ty2 @@ -2194,11 +2195,11 @@ uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns wrapUnifierAndEmit :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -- Some calls to uType - -> TcS (a, RewriterSet) + -> TcS (a, CoHoleSet) -- Like wrapUnifier, but -- emits any unsolved equalities into the work-list -- kicks out any inert constraints that mention unified variables --- returns a RewriterSet describing the new unsolved goals +-- returns a CoHoleSet describing the new unsolved goals wrapUnifierAndEmit ev role do_unifications = do { (unifs, (res, eqs)) <- reportFineGrainUnifications $ wrapUnifier ev role do_unifications ===================================== compiler/GHC/Tc/Solver/Rewrite.hs ===================================== @@ -80,16 +80,16 @@ liftTcS thing_inside -- convenient wrapper when you have a CtEvidence describing -- the rewriting operation -runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet) +runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, CoHoleSet) runRewriteCtEv ev = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvRewriteEqRel ev) -- Run thing_inside (which does the rewriting) -- Also returns the set of Wanteds which rewrote a Wanted; -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint -runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) +runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, CoHoleSet) runRewrite loc flav eq_rel thing_inside - = do { rewriters_ref <- newTcRef emptyRewriterSet + = do { rewriters_ref <- newTcRef emptyCoHoleSet ; let fmode = RE { re_loc = loc , re_flavour = flav , re_eq_rel = eq_rel @@ -226,7 +226,7 @@ a better error message anyway.) -- `rewriters` is the set of coercion holes that have been used to rewrite -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewrite :: CtEvidence -> TcType - -> TcS (Reduction, RewriterSet) + -> TcS (Reduction, CoHoleSet) rewrite ev ty = do { traceTcS "rewrite {" (ppr ty) ; result@(redn, _) <- runRewriteCtEv ev (rewrite_one ty) @@ -239,7 +239,7 @@ rewrite ev ty -- for error messages. (This was important when we flirted with rewriting -- newtypes but perhaps less so now.) rewriteForErrors :: CtEvidence -> TcType - -> TcS (Reduction, RewriterSet) + -> TcS (Reduction, CoHoleSet) rewriteForErrors ev ty = do { traceTcS "rewriteForErrors {" (ppr ty) ; result@(redn, rewriters) <- @@ -251,7 +251,7 @@ rewriteForErrors ev ty -- See Note [Rewriting] rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] - -> TcS (Reductions, RewriterSet) + -> TcS (Reductions, CoHoleSet) -- Externally-callable, hence runRewrite -- Rewrite a vector of types all at once; in fact they are -- always the arguments of type family or class, so ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -1702,19 +1702,19 @@ rewriteDictEvidence ev finish_rewrite :: CtEvidence -- ^ old evidence -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate - -> RewriterSet -- ^ See Note [Wanteds rewrite Wanteds] + -> CoHoleSet -- ^ See Note [Wanteds rewrite Wanteds] -- in GHC.Tc.Types.Constraint -> TcS (StopOrContinue CtEvidence) finish_rewrite old_ev (Reduction co new_pred) rewriters | isReflCo co -- See Note [Rewriting with Refl] - = assert (isEmptyRewriterSet rewriters) $ + = assert (isEmptyCoHoleSet rewriters) $ continueWith (setCtEvPredType old_ev new_pred) finish_rewrite ev@(CtGiven (GivenCt { ctev_evar = old_evar })) (Reduction co new_pred) rewriters - = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted + = assert (isEmptyCoHoleSet rewriters) $ -- this is a Given, not a wanted do { let loc = ctEvLoc ev -- mkEvCast optimises ReflCo ev_rw_role = ctEvRewriteRole ev @@ -1810,7 +1810,7 @@ setPluginEv (tm,ct) -> case dest of EvVarDest {} -> setWantedDict dest EvCanonical tm -- TODO: plugins should be able to signal non-canonicity - HoleDest {} -> setWantedEq dest emptyRewriterSet (evTermCoercion tm) + HoleDest {} -> setWantedEq dest emptyCoHoleSet (evTermCoercion tm) -- TODO: should we try to track rewriters? CtGiven {} -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!" ===================================== compiler/GHC/Tc/Types.hs ===================================== @@ -334,7 +334,7 @@ data RewriteEnv -- ^ At what role are we rewriting? -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite - , re_rewriters :: !(TcRef RewriterSet) -- ^ See Note [Wanteds rewrite Wanteds] + , re_rewriters :: !(TcRef CoHoleSet) -- ^ See Note [Wanteds rewrite Wanteds] } -- RewriteEnv is mostly used in @GHC.Tc.Solver.Rewrite@, but it is defined -- here so that it can also be passed to rewriting plugins. ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -80,7 +80,7 @@ module GHC.Tc.Types.Constraint ( ctEvExpr, ctEvTerm, ctEvCoercion, givenCtEvCoercion, ctEvEvId, wantedCtEvEvId, - ctEvRewriters, ctEvRewriterSet, setWantedCtEvRewriters, + ctEvRewriters, ctEvCoHoleSet, setWantedCtEvRewriters, ctEvUnique, tcEvDestUnique, ctEvRewriteRole, ctEvRewriteEqRel, setCtEvPredType, setCtEvLoc, tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList, @@ -88,10 +88,10 @@ module GHC.Tc.Types.Constraint ( -- CtEvidence constructors GivenCtEvidence(..), WantedCtEvidence(..), - -- RewriterSet - -- RewriterSet(..) is exported concretely only for zonkRewriterSet - RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet, - addRewriter, unitRewriterSet, unionRewriterSet, delRewriterSet, + -- CoHoleSet + -- CoHoleSet(..) is exported concretely only for zonkCoHoleSet + CoHoleSet(..), emptyCoHoleSet, isEmptyCoHoleSet, elemCoHoleSet, + addRewriter, unitCoHoleSet, unionCoHoleSet, delCoHoleSet, rewriterSetFromCts, wrapType, @@ -706,7 +706,7 @@ ctPred :: Ct -> PredType -- See Note [Ct/evidence invariant] ctPred ct = ctEvPred (ctEvidence ct) -ctRewriters :: Ct -> RewriterSet +ctRewriters :: Ct -> CoHoleSet ctRewriters = ctEvRewriters . ctEvidence ctEvId :: HasDebugCallStack => Ct -> EvVar @@ -1210,7 +1210,7 @@ insolubleWantedCt ct -- It's a Wanted , insolubleCt ct -- It's insoluble - , isEmptyRewriterSet rewriters + , isEmptyCoHoleSet rewriters -- It has no rewriters – see (IW1) in Note [Insoluble Wanteds] , not (isGivenLoc loc) -- isGivenLoc: see (IW2) in Note [Insoluble Wanteds] @@ -2341,7 +2341,7 @@ data WantedCtEvidence = { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] , ctev_dest :: TcEvDest -- See Note [CtEvidence invariants] , ctev_loc :: CtLoc - , ctev_rewriters :: RewriterSet } -- See Note [Wanteds rewrite Wanteds] + , ctev_rewriters :: CoHoleSet } -- See Note [Wanteds rewrite Wanteds] ctEvPred :: CtEvidence -> TcPredType -- The predicate of a flavor @@ -2377,9 +2377,9 @@ ctEvTerm ev = EvExpr (ctEvExpr ev) -- See Note [Wanteds rewrite Wanteds] -- If the provided CtEvidence is not for a Wanted, just -- return an empty set. -ctEvRewriters :: CtEvidence -> RewriterSet +ctEvRewriters :: CtEvidence -> CoHoleSet ctEvRewriters (CtWanted (WantedCt { ctev_rewriters = rws })) = rws -ctEvRewriters (CtGiven {}) = emptyRewriterSet +ctEvRewriters (CtGiven {}) = emptyCoHoleSet ctHasNoRewriters :: Ct -> Bool ctHasNoRewriters ev @@ -2389,22 +2389,22 @@ ctHasNoRewriters ev wantedCtHasNoRewriters :: WantedCtEvidence -> Bool wantedCtHasNoRewriters (WantedCt { ctev_rewriters = rws }) - = isEmptyRewriterSet rws + = isEmptyCoHoleSet rws -- | Set the rewriter set of a Wanted constraint. -setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence +setWantedCtEvRewriters :: WantedCtEvidence -> CoHoleSet -> WantedCtEvidence setWantedCtEvRewriters ev rs = ev { ctev_rewriters = rs } -ctEvRewriterSet :: CtEvidence -> RewriterSet +ctEvCoHoleSet :: CtEvidence -> CoHoleSet -- Returns the set of holes (empty or singleton) for the evidence itself -- Note the difference from ctEvRewriters! -ctEvRewriterSet (CtWanted (WantedCt { ctev_dest = HoleDest hole })) = unitRewriterSet hole -ctEvRewriterSet _ = emptyRewriterSet +ctEvCoHoleSet (CtWanted (WantedCt { ctev_dest = HoleDest hole })) = unitCoHoleSet hole +ctEvCoHoleSet _ = emptyCoHoleSet -rewriterSetFromCts :: Bag Ct -> RewriterSet --- Take a bag of Wanted equalities, and collect them as a RewriterSet +rewriterSetFromCts :: Bag Ct -> CoHoleSet +-- Take a bag of Wanted equalities, and collect them as a CoHoleSet rewriterSetFromCts cts - = foldr add emptyRewriterSet cts + = foldr add emptyCoHoleSet cts where add ct rw_set = case ctEvidence ct of @@ -2440,16 +2440,19 @@ ctEvEvId (CtWanted wtd) = wantedCtEvEvId wtd ctEvEvId (CtGiven (GivenCt { ctev_evar = ev })) = ev wantedCtEvEvId :: WantedCtEvidence -> EvVar -wantedCtEvEvId (WantedCt { ctev_dest = EvVarDest ev }) = ev -wantedCtEvEvId (WantedCt { ctev_dest = HoleDest h }) = coHoleCoVar h +wantedCtEvEvId (WantedCt { ctev_dest = dest }) = tcEvDestVar dest ctEvUnique :: CtEvidence -> Unique ctEvUnique (CtGiven (GivenCt { ctev_evar = ev })) = varUnique ev ctEvUnique (CtWanted (WantedCt { ctev_dest = dest })) = tcEvDestUnique dest +tcEvDestVar :: TcEvDest -> EvVar +tcEvDestVar (EvVarDest ev_var) = ev_var +tcEvDestVar (HoleDest co_hole) = coHoleCoVar co_hole + tcEvDestUnique :: TcEvDest -> Unique -tcEvDestUnique (EvVarDest ev_var) = varUnique ev_var -tcEvDestUnique (HoleDest co_hole) = varUnique (coHoleCoVar co_hole) +tcEvDestUnique dest = varUnique (tcEvDestVar dest) + setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence setCtEvLoc (CtGiven (GivenCt pred evar _)) loc = CtGiven (GivenCt pred evar loc) @@ -2493,7 +2496,7 @@ instance Outputable CtEvidence where CtWanted ev -> ppr (ctev_dest ev) rewriters = ctEvRewriters ev - pp_rewriters | isEmptyRewriterSet rewriters = empty + pp_rewriters | isEmptyCoHoleSet rewriters = empty | otherwise = semi <> ppr rewriters isWanted :: CtEvidence -> Bool @@ -2593,39 +2596,52 @@ We thus want Wanteds to rewrite Wanteds in order to accept more programs, but we don't want Wanteds to rewrite Wanteds because doing so can create inscrutable error messages. To solve this dilemma: -* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds - it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters - field of the CtWanted constructor of CtEvidence. (Only Wanteds have - RewriterSets.) +(WRW1) The rewriters of a Wanted. We do allow Wanteds to rewrite Wanteds, but each + unsolved Wanted tracks + the set of Wanteds that it has been rewritten by + in its CoHoleSet, stored in the `ctev_rewriters` field of the CtWanted + constructor of CtEvidence. (Only Wanteds have CoHoleSets.) -* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient - because only equalities (evidenced by coercion holes) are used for rewriting; - other (dictionary) constraints cannot ever rewrite. + If the rewriter set is empty, then the constaint has been not been rewritten + by any unsolved constraint. -* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, +(WRW2) A CoHoleSet is just a set of CoercionHoles. This is sufficient because only + equalities (evidenced by coercion holes) are used for rewriting; other + (dictionary) constraints cannot ever rewrite. + +(WRW3) The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a CoHoleSet, consisting of the evidence (a CoercionHole) for any Wanted equalities used in rewriting. -* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence - add this RewriterSet to the rewritten constraint's rewriter set. +(WRW4) Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence + add this CoHoleSet to the rewritten constraint's rewriter set. + +(WRW5) We prevent the unifier from unifying any equality with a non-empty rewriter + set; unification effectively turns a Wanted into a Given, and we lose all + tracking. See (REWRITERS) in Note [Unification preconditions] in + GHC.Tc.Utils.Unify and Note [Unify only if the rewriter set is empty] in + GHC.Solver.Equality. -* We prevent the unifier from unifying any equality with a non-empty rewriter set; - unification effectively turns a Wanted into a Given, and we lose all tracking. - See (REWRITERS) in Note [Unification preconditions] in GHC.Tc.Utils.Unify and - Note [Unify only if the rewriter set is empty] in GHC.Solver.Equality. +(WRW6) Filling a coercion hole. When filling a coercion hole we store, in the filled + hole `ch_ref`, a CoHoleSet that is a superset of the CoercionHoles in the coercion. e.g. + suppose we fill a coercion hole + co_hole0 := co_hole1 ; Maybe co_hole2 + Another constraint D may have been written by this constraint, and thus have co_hole0 + in D's `ctev_rewriters` When zonking the rewriters of D, we want to record that + it has been rewritten by `co_hole1` and `co_hole2 -* In error reporting, we simply suppress any errors that have been rewritten +(WRW7) In error reporting, we simply suppress any errors that have been rewritten by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, - which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled + which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` to look through any filled coercion holes. The idea is that we wish to report the "root cause" -- the error that rewrote all the others. -* In `selectNextWorkItem`, priorities equalities with no rewiters. See - Note [Prioritise Wanteds with empty RewriterSet] in GHC.Tc.Types.Constraint +(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters. See + Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint wrinkle (PER1). -* In error reporting, we prioritise Wanteds that have an empty RewriterSet: - see Note [Prioritise Wanteds with empty RewriterSet]. +(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet: + see Note [Prioritise Wanteds with empty CoHoleSet]. Let's continue our first example above: @@ -2637,25 +2653,25 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding inert: [W] w1 :: a ~ Char [W] w2 {w1}:: Char ~ Bool -The {w1} in the second line of output is the RewriterSet of w1. +The {w1} in the second line of output is the CoHoleSet of w1. Wrinkles: -(WRW1) When we find a constraint identical to one already in the inert set, +(WRW10) When we find a constraint identical to one already in the inert set, we solve one from the other. Other things being equal, keep the one that has fewer (better still no) rewriters. See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality. - To this accurately we should use `zonkRewriterSet` during canonicalisation, + To do this accurately we should use `zonkCoHoleSet` during canonicalisation, to eliminate rewriters that have now been solved. Currently we only do so during error reporting; but perhaps we should change that. -(WRW2) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take - the opportunity to zonk its `RewriterSet`, which eliminates solved ones. - This doesn't guarantee that rewriter sets are always up to date -- see - (WRW1) -- but it helps, and it de-clutters debug output. +(WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take + the opportunity to zonk its `CoHoleSet`, which eliminates solved ones. + This doesn't guarantee that rewriter sets are always up to date -- c.f. + (WRW10) -- but it helps, and it de-clutters debug output. -Note [Prioritise Wanteds with empty RewriterSet] +Note [Prioritise Wanteds with empty CoHoleSet] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq, we prioritise constraints that have no rewriters. Here's why. @@ -2702,8 +2718,8 @@ is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`. Wrinkles -(PER1) When picking the next work item, before checking for an empty RewriterSet - in GHC.Tc.Solver.Monad.selectNextWorkItem, we zonk the RewriterSet, because +(PER1) When picking the next work item, before checking for an empty CoHoleSet + in GHC.Tc.Solver.Monad.selectNextWorkItem, we zonk the CoHoleSet, because some of those CoercionHoles may have been filled in since we last looked. (PER2) Despite the prioritisation, it is hard to be /certain/ that we can't end up ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -202,7 +202,7 @@ newWantedWithLoc loc pty WantedCt { ctev_dest = dst , ctev_pred = pty , ctev_loc = loc - , ctev_rewriters = emptyRewriterSet } + , ctev_rewriters = emptyCoHoleSet } -- | Create a new Wanted constraint with the given 'CtOrigin', and -- location information taken from the 'TcM' environment. @@ -278,7 +278,7 @@ emitWantedEq origin t_or_k role ty1 ty2 WantedCt { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = loc - , ctev_rewriters = emptyRewriterSet } + , ctev_rewriters = emptyCoHoleSet } ; return (HoleCo hole) } where pty = mkEqPredRole role ty1 ty2 @@ -292,7 +292,7 @@ emitWantedEvVar origin ty ; let ctev = WantedCt { ctev_pred = ty , ctev_dest = EvVarDest new_cv , ctev_loc = loc - , ctev_rewriters = emptyRewriterSet } + , ctev_rewriters = emptyCoHoleSet } ; emitSimple $ mkNonCanonical $ CtWanted ctev ; return new_cv } @@ -360,7 +360,7 @@ newCoercionHole pred_ty ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } -- | Put a value in a coercion hole -fillCoercionHole :: CoercionHole -> (Coercion, RewriterSet) -> TcM () +fillCoercionHole :: CoercionHole -> (Coercion, CoHoleSet) -> TcM () fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co = do { when debugIsOn $ do { cts <- readTcRef ref ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -2297,7 +2297,7 @@ unifyTypeAndEmit t_or_k orig ty1 ty2 -- /any/ level outside this one as untouchable. Hence cur_lvl. ; let env = UE { u_loc = loc, u_role = Nominal , u_given_eq_lvl = cur_lvl - , u_rewriters = emptyRewriterSet -- ToDo: check this + , u_rewriters = emptyCoHoleSet -- ToDo: check this , u_defer = ref, u_what = WU_None } -- The hard work happens here @@ -2444,7 +2444,7 @@ A job for the future. data UnifyEnv = UE { u_role :: Role , u_loc :: CtLoc - , u_rewriters :: RewriterSet + , u_rewriters :: CoHoleSet -- `u_given_eq_lvl` is just like the `inert_given_eq_lvl` -- field of GHC.Tc.Solver.InertSet.InertCans @@ -4597,7 +4597,7 @@ makeTypeConcrete occ_fs conc_orig ty = $ WantedCt { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = loc - , ctev_rewriters = emptyRewriterSet } + , ctev_rewriters = emptyCoHoleSet } ; return (kind_cts S.<> unitBag ct, HoleCo hole) } ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -39,7 +39,7 @@ module GHC.Tc.Zonk.TcType , zonkCt, zonkWC, zonkSimples, zonkImplication -- * Rewriter sets - , zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet + , zonkCoHoleSet, zonkCtCoHoleSet, zonkCtEvCoHoleSet -- * Coercion holes , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe @@ -507,13 +507,13 @@ zonkCt ct zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence -- Zonks the ctev_pred and the ctev_rewriters; but not ctev_evar --- For ctev_rewriters, see (WRW2) in Note [Wanteds rewrite Wanteds] +-- For ctev_rewriters, see (WRW11) in Note [Wanteds rewrite Wanteds] zonkCtEvidence (CtGiven (GivenCt { ctev_pred = pred, ctev_evar = var, ctev_loc = loc })) = do { pred' <- zonkTcType pred ; return (CtGiven (GivenCt { ctev_pred = pred', ctev_evar = var, ctev_loc = loc })) } zonkCtEvidence (CtWanted wanted@(WantedCt { ctev_pred = pred, ctev_rewriters = rws })) = do { pred' <- zonkTcType pred - ; rws' <- zonkRewriterSet rws + ; rws' <- zonkCoHoleSet rws ; return (CtWanted (wanted { ctev_pred = pred', ctev_rewriters = rws' })) } zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo @@ -555,33 +555,33 @@ But c.f Note [Sharing when zonking to Type] in GHC.Tc.Zonk.Type. ************************************************************************ -} -zonkCtRewriterSet :: Ct -> ZonkM Ct -zonkCtRewriterSet ct +zonkCtCoHoleSet :: Ct -> ZonkM Ct +zonkCtCoHoleSet ct | isGivenCt ct = return ct | otherwise = case ct of - CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvCoHoleSet ev ; return (CEqCan (eq { eq_ev = ev' })) } - CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvCoHoleSet ev ; return (CIrredCan (ir { ir_ev = ev' })) } - CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvCoHoleSet ev ; return (CDictCan (di { di_ev = ev' })) } CQuantCan {} -> return ct - CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev + CNonCanonical ev -> do { ev' <- zonkCtEvCoHoleSet ev ; return (CNonCanonical ev') } -zonkCtEvRewriterSet :: CtEvidence -> ZonkM CtEvidence -zonkCtEvRewriterSet ev@(CtGiven {}) +zonkCtEvCoHoleSet :: CtEvidence -> ZonkM CtEvidence +zonkCtEvCoHoleSet ev@(CtGiven {}) = return ev -zonkCtEvRewriterSet ev@(CtWanted wtd) - = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) +zonkCtEvCoHoleSet ev@(CtWanted wtd) + = do { rewriters' <- zonkCoHoleSet (ctEvRewriters ev) ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } -- | Zonk a rewriter set; if a coercion hole in the set has been filled, -- find all the free un-filled coercion holes in the coercion that fills it -zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet -zonkRewriterSet (RewriterSet set) +zonkCoHoleSet :: CoHoleSet -> ZonkM CoHoleSet +zonkCoHoleSet (CoHoleSet set) = unUCHM (nonDetStrictFoldUniqSet go mempty set) -- This does not introduce non-determinism, because the only -- monadic action is to read, and the combining function is @@ -594,16 +594,16 @@ freeHolesOfHole :: CoercionHole -> UnfilledCoercionHoleMonoid freeHolesOfHole hole = UCHM $ do { m_co <- unpackCoercionHole_maybe hole ; case m_co of - Nothing -> return (unitRewriterSet hole) -- Not filled - Just (_co,holes) -> zonkRewriterSet holes } + Nothing -> return (unitCoHoleSet hole) -- Not filled + Just (_co,holes) -> zonkCoHoleSet holes } -newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet } +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM CoHoleSet } instance Semigroup UnfilledCoercionHoleMonoid where - UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) + UCHM l <> UCHM r = UCHM (unionCoHoleSet <$> l <*> r) instance Monoid UnfilledCoercionHoleMonoid where - mempty = UCHM (return emptyRewriterSet) + mempty = UCHM (return emptyCoHoleSet) {- @@ -629,7 +629,7 @@ unpackCoercionHole hole Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } -- | Retrieve the contents of a coercion hole, if it is filled -unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe (Coercion,RewriterSet)) +unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe (Coercion,CoHoleSet)) unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref ===================================== testsuite/tests/quantified-constraints/T15359.hs ===================================== @@ -11,3 +11,10 @@ data Dict c where foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b foo Dict x = x +-- This is a terrible test. If we are trying to solve +-- [W] t1 ~ t2 +-- the quantified constraint will fire, producing +-- [W] C t1 t2 +-- But it would also fire the other way round producing +-- [W] C t2 t1 +-- So it's a coincidence whether or not it typechecks! View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/058b40f2f7d5c04256e81d4a6fdd5a9d... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/058b40f2f7d5c04256e81d4a6fdd5a9d... You're receiving this email because of your account on gitlab.haskell.org.