Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: 174ebaae by Simon Peyton Jones at 2025-06-23T17:34:51+01:00 Solve implications right away [skip ci] .. a very nice simplification if we can really do it - - - - - 6 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 - compiler/GHC/Tc/Solver/Solve.hs-boot - compiler/GHC/Tc/Types/Constraint.hs Changes: ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -2130,7 +2130,8 @@ mk_superclasses_of fuel rec_clss ev tvs theta cls tys -- NB: If there is a loop, we cut off, so we have not -- added the superclasses, hence cc_pend_sc = fuel | otherwise - = CQuantCan (QCI { qci_tvs = tvs, qci_body = mkClassPred cls tys + = CQuantCan (QCI { qci_tvs = tvs, qci_theta = theta + , qci_body = mkClassPred cls tys , qci_ev = ev, qci_pend_sc = fuel }) ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -10,6 +10,8 @@ module GHC.Tc.Solver.Equality( import GHC.Prelude +import {-# SOURCE #-} GHC.Tc.Solver.Solve( trySolveImplication ) + import GHC.Tc.Solver.Irred( solveIrred ) import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance ) import GHC.Tc.Solver.Rewrite @@ -468,7 +470,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 }) <- ev + | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_loc = loc }) <- ev = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2 flags1 = binderFlags bndrs1 flags2 = binderFlags bndrs2 @@ -481,9 +483,10 @@ can_eq_nc_forall ev eq_rel s1 s2 else do { traceTcS "Creating implication for polytype equality" (ppr ev) - ; let free_tvs = tyCoVarsOfTypes [s1,s2] - empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs - ; skol_info <- mkSkolemInfo (UnifyForAllSkol phi1) + ; let free_tvs = tyCoVarsOfTypes [s1,s2] + empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs + skol_info_anon = UnifyForAllSkol phi1 + ; skol_info <- mkSkolemInfo skol_info_anon ; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $ binderVars bndrs1 @@ -528,10 +531,21 @@ can_eq_nc_forall ev eq_rel s1 s2 unifyForAllBody ev (eqRelRole eq_rel) $ \uenv -> go uenv skol_tvs init_subst2 bndrs1 bndrs2 - ; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds - - ; setWantedEq orig_dest all_co - ; stopWith ev "Deferred polytype equality" } } + ; ev_binds_var <- newNoTcEvBinds + ; solved <- trySolveImplication $ + (implicationPrototype (ctLocEnv loc)) + { ic_tclvl = lvl + , ic_binds = ev_binds_var + , ic_info = skol_info_anon + , ic_warn_inaccessible = False + , ic_skols = skol_tvs + , ic_given = [] + , ic_wanted = emptyWC { wc_simple = wanteds } } + + ; if solved + then do { setWantedEq orig_dest all_co + ; stopWith ev "Polytype equality: solved" } + else canEqSoftFailure IrredShapeReason ev s1 s2 } } | otherwise = do { traceTcS "Omitting decomposition of given polytype equality" $ @@ -834,18 +848,26 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) = do { inerts <- getInertSet ; if can_decompose inerts then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) - else canEqSoftFailure ev eq_rel ty1 ty2 } + else assert (eq_rel == ReprEq) $ + canEqSoftFailure ReprEqReason ev ty1 ty2 } -- See Note [Skolem abstract data] in GHC.Core.Tycon | tyConSkolem tc1 || tyConSkolem tc2 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2) ; finishCanWithIrred AbstractTyConReason ev } - | otherwise -- Different TyCons - = if both_generative -- See (TC2) and (TC3) in - -- Note [Canonicalising TyCon/TyCon equalities] - then canEqHardFailure ev ty1 ty2 - else canEqSoftFailure ev eq_rel ty1 ty2 + -- Different TyCons + | NomEq <- eq_rel + = canEqHardFailure ev ty1 ty2 + + -- Different TyCons, eq_rel = ReprEq + -- See (TC2) and (TC3) in + -- Note [Canonicalising TyCon/TyCon equalities] + | both_generative + = canEqHardFailure ev ty1 ty2 + + | otherwise + = canEqSoftFailure ReprEqReason ev ty1 ty2 where -- See Note [Decomposing TyConApp equalities] -- and Note [Decomposing newtype equalities] @@ -1417,20 +1439,18 @@ canDecomposableFunTy ev eq_rel af f1@(ty1,m1,a1,r1) f2@(ty2,m2,a2,r2) -- | Call canEqSoftFailure when canonicalizing an equality fails, but if the -- equality is representational, there is some hope for the future. -canEqSoftFailure :: CtEvidence -> EqRel -> TcType -> TcType +canEqSoftFailure :: CtIrredReason -> CtEvidence -> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a)) -canEqSoftFailure ev NomEq ty1 ty2 - = canEqHardFailure ev ty1 ty2 -canEqSoftFailure ev ReprEq ty1 ty2 +canEqSoftFailure reason ev ty1 ty2 = do { (redn1, rewriters1) <- rewrite ev ty1 ; (redn2, rewriters2) <- rewrite ev ty2 -- We must rewrite the types before putting them in the -- inert set, so that we are sure to kick them out when -- new equalities become available - ; traceTcS "canEqSoftFailure with ReprEq" $ + ; traceTcS "canEqSoftFailure" $ vcat [ ppr ev, ppr redn1, ppr redn2 ] ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 - ; finishCanWithIrred ReprEqReason new_ev } + ; finishCanWithIrred reason new_ev } -- | Call when canonicalizing an equality fails with utterly no hope. canEqHardFailure :: CtEvidence -> TcType -> TcType ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -758,12 +758,14 @@ getUnsolvedInerts , inert_funeqs = fun_eqs , inert_irreds = irreds , inert_dicts = idicts + , inert_insts = qcis } <- getInertCans ; let unsolved_tv_eqs = foldTyEqs (add_if_unsolved CEqCan) tv_eqs emptyCts unsolved_fun_eqs = foldFunEqs (add_if_unsolved CEqCan) fun_eqs emptyCts unsolved_irreds = foldr (add_if_unsolved CIrredCan) emptyCts irreds unsolved_dicts = foldDicts (add_if_unsolved CDictCan) idicts emptyCts + unsolved_qcis = foldr (add_if_unsolved CQuantCan) emptyCts qcis ; implics <- getWorkListImplics @@ -774,10 +776,11 @@ getUnsolvedInerts , text "irreds =" <+> ppr unsolved_irreds , text "implics =" <+> ppr implics ] - ; return ( implics, unsolved_tv_eqs `unionBags` + ; return ( implics, unsolved_tv_eqs `unionBags` unsolved_fun_eqs `unionBags` - unsolved_irreds `unionBags` - unsolved_dicts ) } + unsolved_irreds `unionBags` + unsolved_dicts `unionBags` + unsolved_qcis ) } where add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts add_if_unsolved mk_ct thing cts ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -7,6 +7,7 @@ module GHC.Tc.Solver.Solve ( solveWanteds, -- Solves WantedConstraints solveSimpleGivens, -- Solves [Ct] solveSimpleWanteds, -- Solves Cts + trySolveImplication, setImplicationStatus ) where @@ -1114,14 +1115,15 @@ solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel , eq_lhs = lhs, eq_rhs = rhs })) = solveEquality ev eq_rel (canEqLHSType lhs) rhs -solveCt (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) - = do { ev <- rewriteEvidence ev +solveCt (CQuantCan qci@(QCI { qci_ev = ev })) + = do { ev' <- rewriteEvidence ev -- It is (much) easier to rewrite and re-classify than to -- rewrite the pieces and build a Reduction that will rewrite -- the whole constraint - ; case classifyPredType (ctEvPred ev) of - ForAllPred tvs theta body_pred -> - Stage $ solveForAll ev tvs theta body_pred pend_sc + ; case classifyPredType (ctEvPred ev') of + ForAllPred tvs theta body_pred + -> solveForAll (qci { qci_ev = ev', qci_tvs = tvs + , qci_theta = theta, qci_body = body_pred }) _ -> pprPanic "SolveCt" (ppr ev) } solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc })) @@ -1155,7 +1157,7 @@ solveNC ev -- And then re-classify ; case classifyPredType (ctEvPred ev) of ClassPred cls tys -> solveDictNC ev cls tys - ForAllPred tvs th p -> Stage $ solveForAllNC ev tvs th p + ForAllPred tvs th p -> solveForAllNC ev tvs th p IrredPred {} -> solveIrred (IrredCt { ir_ev = ev, ir_reason = IrredShapeReason }) EqPred eq_rel ty1 ty2 -> solveEquality ev eq_rel ty1 ty2 -- EqPred only happens if (say) `c` is unified with `a ~# b`, @@ -1246,51 +1248,49 @@ type signature. -- -- Precondition: the constraint has already been rewritten by the inert set. solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType - -> TcS (StopOrContinue Void) + -> SolverStage Void solveForAllNC ev tvs theta body_pred - | Just (cls,tys) <- getClassPredTys_maybe body_pred - , classHasSCs cls - = do { dflags <- getDynFlags - -- Either expand superclasses (Givens) or provide fuel to do so (Wanteds) - ; if isGiven ev - then - -- See Note [Eagerly expand given superclasses] - -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - do { sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys - ; emitWork (listToBag sc_cts) - ; solveForAll ev tvs theta body_pred doNotExpand } - else - -- See invariants (a) and (b) in QCI.qci_pend_sc - -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - -- See Note [Quantified constraints] - do { solveForAll ev tvs theta body_pred (qcsFuel dflags) } - } + = do { fuel <- simpleStage mk_super_classes + ; solveForAll (QCI { qci_ev = ev, qci_tvs = tvs, qci_theta = theta + , qci_body = body_pred, qci_pend_sc = fuel }) } - | otherwise - = solveForAll ev tvs theta body_pred doNotExpand + where + mk_super_classes :: TcS ExpansionFuel + mk_super_classes + | Just (cls,tys) <- getClassPredTys_maybe body_pred + , classHasSCs cls + = do { dflags <- getDynFlags + -- Either expand superclasses (Givens) or provide fuel to do so (Wanteds) + ; if isGiven ev + then + -- See Note [Eagerly expand given superclasses] + -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + do { sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys + ; emitWork (listToBag sc_cts) + ; return doNotExpand } + else + -- See invariants (a) and (b) in QCI.qci_pend_sc + -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + -- See Note [Quantified constraints] + return (qcsFuel dflags) + } + + | otherwise + = return doNotExpand -- | Solve a canonical quantified constraint. -- -- Precondition: the constraint has already been rewritten by the inert set. -solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel - -> TcS (StopOrContinue Void) -solveForAll ev tvs theta body_pred fuel +solveForAll :: QCInst -> SolverStage Void +solveForAll qci@(QCI { qci_ev = ev, qci_tvs = tvs, qci_theta = theta, qci_body = pred }) = case ev of CtGiven {} -> -- See Note [Solving a Given forall-constraint] - do { addInertForAll qci - ; stopWith ev "Given forall-constraint" } + do { simpleStage (addInertForAll qci) + ; stopWithStage ev "Given forall-constraint" } CtWanted wtd -> - do { mode <- getTcSMode - ; case mode of -- See Note [TcSSpecPrag] in GHC.Tc.Solver.Monad. - TcSSpecPrag -> solveWantedForAll_spec wtd - _ -> runSolverStage $ - do { tryInertQCs qci - ; solveWantedForAll_norm wtd tvs theta body_pred } } - where - qci = QCI { qci_ev = ev, qci_tvs = tvs - , qci_body = body_pred, qci_pend_sc = fuel } - + do { tryInertQCs qci + ; solveWantedForAll qci tvs theta pred wtd } tryInertQCs :: QCInst -> SolverStage () tryInertQCs qc @@ -1316,11 +1316,11 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts = -- | Solve a (canonical) Wanted quantified constraint by emitting an implication. -- See Note [Solving a Wanted forall-constraint] -solveWantedForAll_norm :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType - -> SolverStage Void -solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc - , ctev_rewriters = rewriters }) - tvs theta body_pred +solveWantedForAll :: QCInst -> [TcTyVar] -> TcThetaType -> PredType + -> WantedCtEvidence -> SolverStage Void +solveWantedForAll qci tvs theta body_pred + wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc + , ctev_rewriters = rewriters }) = Stage $ TcS.setSrcSpan (getCtLocEnvLoc loc_env) $ -- This setSrcSpan is important: the emitImplicationTcS uses that @@ -1349,27 +1349,25 @@ solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) - ; ev_binds_var <- newTcEvBinds + ; ev_binds_var <- TcS.newTcEvBinds ; solved <- trySolveImplication $ - implicationPrototype loc_env + (implicationPrototype loc_env) { ic_tclvl = lvl , ic_binds = ev_binds_var , ic_info = skol_info_anon - , ic_warn_inacessible = False + , ic_warn_inaccessible = False , ic_skols = skol_tvs , ic_given = given_ev_vars , ic_wanted = emptyWC { wc_simple = wanteds } } ; if not solved - then updInertIrreds ( - else - do { ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds - - ; setWantedEvTerm dest EvCanonical $ - EvFun { et_tvs = skol_tvs, et_given = given_ev_vars - , et_binds = ev_binds, et_body = w_id } - ; stopWith (CtWanted wtd) "Wanted forall-constraint (implication)" } + then do { addInertForAll qci + ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" } + else do { setWantedEvTerm dest EvCanonical $ + EvFun { et_tvs = skol_tvs, et_given = given_ev_vars + , et_binds = TcEvBinds ev_binds_var, et_body = w_id } + ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } } where - loc_env = ctLocEnv loc + loc_env = ctLocEnv ct_loc is_qc = IsQC (ctLocOrigin ct_loc) empty_subst = mkEmptySubst $ mkInScopeSet $ @@ -1381,6 +1379,14 @@ solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc ClassPred cls tys -> pSizeClassPred cls tys _ -> pSizeType pred +trySolveImplication :: Implication -> TcS Bool +trySolveImplication imp + = tryTcS $ + do { imp' <- solveImplication imp + ; return (emptyWC { wc_impl = unitBag imp' }) } + -- ToDo: this emptyWC bit is somewhat clumsy + +{- solveWantedForAll_spec :: WantedCtEvidence -> TcS (StopOrContinue Void) -- Solve this implication constraint completely or not at all solveWantedForAll_spec wtd @@ -1399,7 +1405,7 @@ solveWantedForAll_spec wtd ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } } where ev = CtWanted wtd - +-} {- Note [Solving a Wanted forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Solver/Solve.hs-boot ===================================== @@ -1,6 +1,8 @@ module GHC.Tc.Solver.Solve where +import Prelude( Bool ) import GHC.Tc.Solver.Monad( TcS ) -import GHC.Tc.Types.Constraint( WantedConstraints, Cts ) +import GHC.Tc.Types.Constraint( WantedConstraints, Cts, Implication ) -solveSimpleWanteds :: Cts -> TcS WantedConstraints \ No newline at end of file +solveSimpleWanteds :: Cts -> TcS WantedConstraints +trySolveImplication :: Implication -> TcS Bool ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -351,9 +351,10 @@ instance Outputable IrredCt where -- See Note [Quantified constraints] in GHC.Tc.Solver.Solve data QCInst -- | A quantified constraint, of type @forall tvs. context => ty@ - = QCI { qci_ev :: CtEvidence - , qci_tvs :: [TcTyVar] -- ^ @tvs@ - , qci_body :: TcPredType -- ^ the body of the @forall@, i.e. @ty@ + = QCI { qci_ev :: CtEvidence -- See Note [Ct/evidence invariant] + , qci_tvs :: [TcTyVar] -- ^ @tvs@ + , qci_theta :: TcThetaType + , qci_body :: TcPredType -- ^ the body of the @forall@, i.e. @ty@ , qci_pend_sc :: ExpansionFuel -- ^ Invariants: qci_pend_sc > 0 => -- @@ -990,8 +991,8 @@ pendingScDict_maybe _ = Nothing pendingScInst_maybe :: QCInst -> Maybe QCInst -- Same as isPendingScDict, but for QCInsts -pendingScInst_maybe qci@(QCI { qci_flav = flav, qci_pend_sc = f }) - | Given <- flav -- Do not expand Wanted QCIs +pendingScInst_maybe qci@(QCI { qci_ev = ev, qci_pend_sc = f }) + | isGiven ev -- Do not expand Wanted QCIs , pendingFuel f = Just (qci { qci_pend_sc = doNotExpand }) | otherwise = Nothing View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/174ebaae7fff80dbf5f313e8702fb036... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/174ebaae7fff80dbf5f313e8702fb036... You're receiving this email because of your account on gitlab.haskell.org.