Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: 024c8349 by Simon Peyton Jones at 2025-06-15T23:43:40+01:00 Fix the solve-once business for quantified constraints ... so that we solve the resulting implication - - - - - 4bf402c6 by Simon Peyton Jones at 2025-06-15T23:43:54+01:00 Add missing zap-occ-info - - - - - 1d2f05d1 by Simon Peyton Jones at 2025-06-15T23:44:06+01:00 Tracing only - - - - - d82e2219 by Simon Peyton Jones at 2025-06-15T23:44:28+01:00 Buuild an implication for spec-prags This is subtle -- ensures there are bindings to decompose in prepareSpecLHS - - - - - 13a1fcec by Simon Peyton Jones at 2025-06-15T23:46:58+01:00 Better zonking for AbsBinds prags - - - - - 5 changed files: - compiler/GHC/Core/Opt/Specialise.hs - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/Type.hs Changes: ===================================== compiler/GHC/Core/Opt/Specialise.hs ===================================== @@ -1784,43 +1784,6 @@ alreadyCovered env bndrs fn args is_active rules where in_scope = substInScopeSet (se_subst env) -{- -specRhs :: SpecEnv -> [InVar] -> InExpr -> [OutExpr] - -> SpecM (OutExpr, UsageDetails) - -specRhs env bndrs body [] -- Like specExpr (Lam bndrs body) - = specLam env' bndrs' body - where - (env', bndrs') = substBndrs env bndrs - -specRhs _env [] body args - = -- The caller should have ensured that there are no more - -- args than we have binders on the RHS - pprPanic "specRhs:too many args" (ppr args $$ ppr body) - -specRhs env@(SE { se_subst = subst }) (bndr:bndrs) body (arg:args) - | exprIsTrivial arg - , let env' = env { se_subst = Core.extendSubst subst bndr arg } - = specRhs env' bndrs body args - - - | otherwise -- Non-trivial argument; it must be a dictionary - = do { fresh_id <- newIdBndr "dx" (exprType arg) - ; let fresh_id' = fresh_id `addDictUnfolding` arg - dict_bind = mkDB (NonRec fresh_id' arg) - env' = env { se_subst = Core.extendSubst subst bndr (Var fresh_id') - `Core.extendSubstInScope` fresh_id' } - -- Ensure the new unfolding is in the in-scope set - ; (body', uds) <- specRhs env' bndrs body args - ; return (body', dict_bind `consDictBind` uds) } - -consDictBind :: DictBind -> UsageDetails -> UsageDetails -consDictBind db uds@MkUD{ud_binds=FDB{fdb_binds = binds, fdb_bndrs = bs}} - = uds { ud_binds = FDB{ fdb_binds = db `consOL` binds - , fdb_bndrs = bs `extendVarSetList` bindersOfDictBind db } } - --} - -- Convenience function for invoking lookupRule from Specialise -- The SpecEnv's InScopeSet should include all the Vars in the [CoreExpr] specLookupRule :: HasDebugCallStack @@ -2611,7 +2574,7 @@ specHeader subst (bndr:bndrs) (UnspecType : args) specHeader subst (bndr:bndrs) (_ : args) | isDeadBinder bndr - , let (subst1, bndr') = Core.substBndr subst bndr + , let (subst1, bndr') = Core.substBndr subst (zapIdOccInfo bndr) , Just rubbish_lit <- mkLitRubbish (idType bndr') = -- See Note [Drop dead args from specialisations] do { (useful, subst2, rule_bs, rule_es, spec_bs, spec_args) <- specHeader subst1 bndrs args ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1100,6 +1100,7 @@ dsSpec_help poly_nm poly_id poly_rhs inl bndrs ds_call ; tracePm "dsSpec(new route)" $ vcat [ text "poly_id" <+> ppr poly_id + , text "unfolding" <+> ppr (realIdUnfolding poly_id) , text "bndrs" <+> ppr bndrs , text "ds_call" <+> ppr ds_call , text "core_call" <+> ppr core_call ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -1274,17 +1274,19 @@ solveForAllNC ev tvs theta body_pred -- 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 = - case ev of - CtGiven {} -> - -- See Note [Solving a Given forall-constraint] - do { addInertForAll qci - ; stopWith ev "Given forall-constraint" } - CtWanted wtd -> - -- See Note [Solving a Wanted forall-constraint] - runSolverStage $ - do { tryInertQCs qci - ; Stage $ solveWantedForAll wtd tvs theta body_pred } +solveForAll ev tvs theta body_pred fuel + = case ev of + CtGiven {} -> + -- See Note [Solving a Given forall-constraint] + do { addInertForAll qci + ; stopWith 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 } @@ -1312,82 +1314,78 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts = = Nothing -- | Solve a (canonical) Wanted quantified constraint by emitting an implication. --- -- See Note [Solving a Wanted forall-constraint] -solveWantedForAll :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType - -> TcS (StopOrContinue Void) -solveWantedForAll wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc - , ctev_rewriters = rewriters }) +solveWantedForAll_norm :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType + -> SolverStage Void +solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc + , ctev_rewriters = rewriters }) tvs theta body_pred - = -- We are about to do something irreversible (turning a quantified constraint - -- into an implication), so wrap the inner call in solveCompletelyIfRequired - -- to ensure we can roll back if we can't solve the implication fully. - -- See Note [TcSSpecPrag] in GHC.Tc.Solver.Monad. - do { mode <- getTcSMode - ; case mode of - TcSSpecPrag - -> do { traceTcS "solveWantedForAll {" (ppr wtd) - ; fully_solved <- tryTcS (setTcSMode TcSVanilla $ - solveSimpleWanteds (unitBag ct)) - ; if fully_solved - then do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd) - ; return $ Stop ev (text "Fully solved:" <+> ppr wtd) } - else do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd) - ; updInertIrreds (IrredCt ev IrredShapeReason) - -- Stash the unsolved quantified constraint in the irreds - ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } } - - _ -> do { solve_by_emitting_implic - ; stopWith ev "Wanted forall-constraint (implication)" } } + = Stage $ + TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $ + -- This setSrcSpan is important: the emitImplicationTcS uses that + -- TcLclEnv for the implication, and that in turn sets the location + -- for the Givens when solving the constraint (#21006) + + do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] + -- in GHC.Tc.Utils.TcType + -- Very like the code in tcSkolDFunType + rec { skol_info <- mkSkolemInfo skol_info_anon + ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs + ; let inst_pred = substTy subst body_pred + inst_theta = substTheta subst theta + skol_info_anon = InstSkol is_qc (get_size inst_pred) } + + ; given_ev_vars <- mapM newEvVar inst_theta + ; (lvl, (w_id, wanteds)) + <- pushLevelNoWorkList (ppr skol_info) $ + do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc) + -- Set the thing to prove to have a ScOrigin, so we are + -- careful about its termination checks. + -- See (QC-INV) in Note [Solving a Wanted forall-constraint] + ; wanted_ev <- newWantedNC loc' rewriters inst_pred + -- NB: inst_pred can be an equality + ; return ( wantedCtEvEvId wanted_ev + , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } + + ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) + ; 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)" } where - ev = CtWanted wtd - ct = mkNonCanonical ev is_qc = IsQC (ctLocOrigin loc) empty_subst = mkEmptySubst $ mkInScopeSet $ tyCoVarsOfTypes (body_pred:theta) `delVarSetList` tvs - -- This setSrcSpan is important: the emitImplicationTcS uses that - -- TcLclEnv for the implication, and that in turn sets the location - -- for the Givens when solving the constraint (#21006) - solve_by_emitting_implic - = TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $ - do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] - -- in GHC.Tc.Utils.TcType - -- Very like the code in tcSkolDFunType - rec { skol_info <- mkSkolemInfo skol_info_anon - ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs - ; let inst_pred = substTy subst body_pred - inst_theta = substTheta subst theta - skol_info_anon = InstSkol is_qc (get_size inst_pred) } - - ; given_ev_vars <- mapM newEvVar inst_theta - ; (lvl, (w_id, wanteds)) - <- pushLevelNoWorkList (ppr skol_info) $ - do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc) - -- Set the thing to prove to have a ScOrigin, so we are - -- careful about its termination checks. - -- See (QC-INV) in Note [Solving a Wanted forall-constraint] - ; wanted_ev <- newWantedNC loc' rewriters inst_pred - -- NB: inst_pred can be an equality - ; return ( wantedCtEvEvId wanted_ev - , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } - - ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) - ; 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 } - } - -- Getting the size of the head is a bit horrible -- because of the special treament for class predicates get_size pred = case classifyPredType pred of ClassPred cls tys -> pSizeClassPred cls tys _ -> pSizeType pred +solveWantedForAll_spec :: WantedCtEvidence -> TcS (StopOrContinue Void) +-- Solve this implication constraint completely or not at all +solveWantedForAll_spec wtd + = do { traceTcS "solveWantedForAll {" (ppr wtd) + ; fully_solved <- tryTcS (setTcSMode TcSVanilla $ + solveWanteds (mkSimpleWC [ev])) + -- It's crucial to call solveWanteds here, not solveSimpleWanteds, + -- because solving `ev` will land in solveWantedForAll_norm, + -- which emits an implication, which we must then solve + ; if fully_solved + then do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd) + ; return $ Stop ev (text "Fully solved:" <+> ppr wtd) } + else do { traceTcS "solveWantedForAll: not fully solved }" (ppr wtd) + ; updInertIrreds (IrredCt ev IrredShapeReason) + -- Stash the unsolved quantified constraint in the irreds + ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } } + where + ev = CtWanted wtd + + {- Note [Solving a Wanted forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Solving a wanted forall (quantified) constraint ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -581,6 +581,11 @@ implicationNeeded skol_info skol_tvs given alwaysBuildImplication :: SkolemInfoAnon -> Bool -- See Note [When to build an implication] +alwaysBuildImplication (SigSkol ctxt _ _) + = case ctxt of + FunSigCtxt {} -> True -- RHS of a binding with a signature + SpecInstCtxt -> True -- SpecInstCtxt: this is rather delicate + _ -> False alwaysBuildImplication _ = False {- Commmented out for now while I figure out about error messages. ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -746,8 +746,12 @@ zonk_bind (XHsBindsLR (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs runZonkBndrT (zonkTyBndrsX tyvars ) $ \ new_tyvars -> runZonkBndrT (zonkEvBndrsX evs ) $ \ new_evs -> runZonkBndrT (zonkTcEvBinds_s ev_binds) $ \ new_ev_binds -> - do { (new_val_bind, new_exports) <- mfix $ \ ~(new_val_binds, _) -> - runZonkBndrT (extendIdZonkEnvRec $ collectHsBindsBinders CollNoDictBinders new_val_binds) $ \ _ -> + do { (new_val_bind, new_exports) <- mfix $ \ ~(new_val_binds, new_exports) -> + let new_bndrs = collectHsBindsBinders CollNoDictBinders new_val_binds + ++ map abe_poly new_exports + -- Tie the knot with the `abe_poly` binders too, since they + -- may be mentioned in the `abe_prags` of the `exports` + in runZonkBndrT (extendIdZonkEnvRec new_bndrs) $ \ _ -> do { new_val_binds <- mapM zonk_val_bind val_binds ; new_exports <- mapM zonk_export exports ; return (new_val_binds, new_exports) @@ -854,6 +858,7 @@ zonkLTcSpecPrags ps ; skol_tvs_ref <- lift $ newTcRef [] ; setZonkType (SkolemiseFlexi skol_tvs_ref) $ -- SkolemiseFlexi: see Note [Free tyvars on rule LHS] + runZonkBndrT (zonkCoreBndrsX bndrs) $ \ bndrs' -> do { spec_e' <- zonkLExpr spec_e ; skol_tvs <- lift $ readTcRef skol_tvs_ref View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a1c855b41b89277393b8df4a5636e1e... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a1c855b41b89277393b8df4a5636e1e... You're receiving this email because of your account on gitlab.haskell.org.