Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 135152ba by Simon Peyton Jones at 2025-09-30T23:11:19+01:00 Build implicaiton for constraints from (static e) This commit addresses #26466, by buiding an implication for the constraints arising from a (static e) form. The implication has a special ic_info field of StaticFormSkol, which tells the constraint solver to use an empty set of Givens. See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable This commit also reinstates an `assert` in GHC.Tc.Solver.Equality. The test `StaticPtrTypeFamily` was failing with an assertion failure, but it now works. - - - - - 11 changed files: - compiler/GHC/Iface/Tidy/StaticPtrTable.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Monad.hs Changes: ===================================== compiler/GHC/Iface/Tidy/StaticPtrTable.hs ===================================== @@ -62,25 +62,35 @@ Here is a running example: f x = let k = map toUpper in ...(static k)... -* The renamer looks for out-of-scope names in the body of the static +(SF1) The renamer looks for out-of-scope names in the body of the static form, as always. If all names are in scope, the free variables of the body are stored in AST at the location of the static form. -* The typechecker verifies that all free variables occurring in the +(SF2) The typechecker verifies that all free variables occurring in the static form are floatable to top level (see Note [Meaning of IdBindingInfo] in GHC.Tc.Types). In our example, 'k' is floatable. Even though it is bound in a nested let, we are fine. See the call to `checkClosedInStaticForm` in the HsStatic case of `tcExpr`. -* The desugarer replaces the static form with an application of the +(SF3) The typechecker also wraps the constraints from a static form in an + implication, with ic_info = StaticFormSkol. When we try to solve such an + implication, we do so with /no Givens/; see `nestImplicTcS`. For example: + g :: Show a => StaticPtr (a -> String) + g = static show + If the @Show a0@ constraint that the body of the static form produces was + resolved in the context of the enclosing expression, then the body of the + static form wouldn't be closed because the Show dictionary would come from + g's context instead of coming from the top level. + +(SF4) The desugarer replaces the static form with an application of the function 'makeStatic' (defined in module GHC.StaticPtr.Internal of base). So we get f x = let k = map toUpper in ...fromStaticPtr (makeStatic location k)... -* The simplifier runs the FloatOut pass which moves the calls to 'makeStatic' +(SF5) The simplifier runs the FloatOut pass which moves the calls to 'makeStatic' to the top level. Thus the FloatOut pass is always executed, even when optimizations are disabled. So we get @@ -106,7 +116,7 @@ Here is a running example: Making the binding exported also has a necessary effect during the CoreTidy pass. -* The CoreTidy pass replaces all bindings of the form +(SF6) The CoreTidy pass replaces all bindings of the form b = /\ ... -> makeStatic location value @@ -116,12 +126,12 @@ Here is a running example: where a distinct key is generated for each binding. -* If we are compiling to object code we insert a C stub (generated by +(SF7) If we are compiling to object code we insert a C stub (generated by sptModuleInitCode) into the final object which runs when the module is loaded, inserting the static forms defined by the module into the RTS's static pointer table. -* If we are compiling for the byte-code interpreter, we instead explicitly add +(SF8) If we are compiling for the byte-code interpreter, we instead explicitly add the SPT entries (recorded in CgGuts' cg_spt_entries field) to the interpreter process' SPT table using the addSptEntry interpreter message. This happens in upsweep after we have compiled the module (see GHC.Driver.Make.upsweep'). ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -568,26 +568,30 @@ tcExpr (HsProc x pat cmd) res_ty tcExpr (HsStatic fvs expr) res_ty = do { res_ty <- expTypeToType res_ty ; (co, (p_ty, expr_ty)) <- matchExpectedAppTy res_ty - ; (expr', lie) <- captureConstraints $ - addErrCtxt (StaticFormCtxt expr) $ - tcCheckPolyExprNC expr expr_ty + ; (expr', lie) <- captureConstraints $ + addErrCtxt (StaticFormCtxt expr) $ + tcCheckPolyExprNC expr expr_ty + + -- Emit an implication that captures the constraints of `expr`, + -- but with a `ic_info` of StaticFormSkol + -- See #13499 for an explanation of why this is the right thing to do: + -- the enclosing skolems must be in scope. + ; tc_lvl <- getTcLevel -- No need to bump the level + ; (implic, ev_binds) <- buildImplicationFor tc_lvl StaticFormSkol [] [] lie + ; emitImplications implic + ; let expr'' = mkLHsWrap (mkWpLet ev_binds) expr' -- Check that the free variables of the static form are closed. -- It's OK to use nonDetEltsUniqSet here as the only side effects of -- checkClosedInStaticForm are error messages. + -- See (SF2) Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable ; mapM_ checkClosedInStaticForm $ nonDetEltsUniqSet fvs -- Require the type of the argument to be Typeable. ; typeableClass <- tcLookupClass typeableClassName ; typeable_ev <- emitWantedEvVar StaticOrigin $ - mkTyConApp (classTyCon typeableClass) - [liftedTypeKind, expr_ty] - - -- Insert the constraints of the static form in a global list for later - -- validation. See #13499 for an explanation of why this really isn't the - -- right thing to do: the enclosing skolems aren't in scope any more! - -- Static forms really aren't well worked out yet. - ; emitStaticConstraints lie + mkTyConApp (classTyCon typeableClass) + [liftedTypeKind, expr_ty] -- Wrap the static form with the 'fromStaticPtr' call. ; fromStaticPtr <- newMethodFromName StaticOrigin fromStaticPtrName @@ -595,9 +599,11 @@ tcExpr (HsStatic fvs expr) res_ty ; let wrap = mkWpEvVarApps [typeable_ev] <.> mkWpTyApps [expr_ty] ; loc <- getSrcSpanM ; static_ptr_ty_con <- tcLookupTyCon staticPtrTyConName - ; return $ mkHsWrapCo co $ HsApp noExtField - (L (noAnnSrcSpan loc) $ mkHsWrap wrap fromStaticPtr) - (L (noAnnSrcSpan loc) (HsStatic (fvs, mkTyConApp static_ptr_ty_con [expr_ty]) expr')) + ; return $ mkHsWrapCo co $ + HsApp noExtField + (L (noAnnSrcSpan loc) $ mkHsWrap wrap fromStaticPtr) + (L (noAnnSrcSpan loc) (HsStatic (fvs, mkTyConApp static_ptr_ty_con [expr_ty]) + expr'')) } tcExpr (HsEmbTy _ _) _ = failWith (TcRnIllegalTypeExpr TypeKeywordSyntax) ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -102,17 +102,14 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) -- calling this, so that the reportUnsolved has access to the most -- complete GlobalRdrEnv captureTopConstraints thing_inside - = do { static_wc_var <- TcM.newTcRef emptyWC ; - ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $ - TcM.tryCaptureConstraints thing_inside - ; stWC <- TcM.readTcRef static_wc_var + = do { (mb_res, lie) <- TcM.tryCaptureConstraints thing_inside -- See GHC.Tc.Utils.Monad Note [Constraints and errors] -- If the thing_inside threw an exception, but generated some insoluble -- constraints, report the latter before propagating the exception -- Otherwise they will be lost altogether ; case mb_res of - Just res -> return (res, lie `andWC` stWC) + Just res -> return (res, lie) Nothing -> do { _ <- simplifyTop lie; failM } } -- This call to simplifyTop is the reason -- this function is here instead of GHC.Tc.Utils.Monad ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -275,13 +275,13 @@ solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implicati solveImplicationUsingUnsatGiven unsat_given@(given_ev,_) impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var - , ic_need_implic = inner }) + , ic_need_implic = inner, ic_info = skol_info }) | isCoEvBindsVar ev_binds_var -- We can't use Unsatisfiable evidence in kinds. -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence. = return impl | otherwise - = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd + = do { wcs <- nestImplicTcS skol_info ev_binds_var tclvl $ go_wc wtd ; setImplicationStatus $ impl { ic_wanted = wcs , ic_need_implic = inner `extendEvNeedSet` given_ev } } @@ -1135,7 +1135,7 @@ disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent ; tclvl <- TcS.getTcLevel -- Step (3) in Note [How type-class constraints are defaulted] ; successes <- fmap catMaybes $ - nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) $ + nestImplicTcS DefaultSkol fake_ev_binds_var (pushTcLevel tclvl) $ mapM firstSuccess proposalSequences ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds , ppr proposalSequences ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1681,7 +1681,6 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 in unSwap swapped (uType uenv') ki1 ki2 -- mkKindEqLoc: any new constraints, arising from the kind -- unification, say they thay come from unifying xi1~xi2 - -- ...AndEmit: emit any unsolved equalities -- Kick out any inert constraints mentioning the unified variables ; kickOutAfterUnification unifs @@ -1697,14 +1696,13 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -- Emit the deferred constraints do { emitChildEqs ev eqs --- This assert is commented out because of #26453. Reinstate it when #26453 is fixed --- ; assertPpr (not (isEmptyCts eqs)) --- (vcat [ppr ev, ppr ki1, ppr ki2, ppr unifs, ppr eqs]) $ --- -- assert: the constraints won't be empty because the two kinds differ, --- -- and there are no unifications, so we must have emitted one or --- -- more constraints + ; assertPpr (not (isEmptyCts eqs)) + (vcat [ppr ev, ppr ki1, ppr ki2, ppr unifs, ppr eqs]) $ + -- assert: the constraints won't be empty because the two kinds differ, + -- and there are no unifications, so we must have emitted one or + -- more constraints - ; finish (rewriterSetFromCts eqs) kind_co }} + finish (rewriterSetFromCts eqs) kind_co }} -- rewriterSetFromCts: record in the /type/ unification xi1~xi2 that -- it has been rewritten by any (unsolved) constraints in `cts`; that -- stops xi1~xi2 from unifying until `cts` are solved. See (EIK2). ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1199,20 +1199,12 @@ setTcLevelTcS :: TcLevel -> TcS a -> TcS a setTcLevelTcS lvl (TcS thing_inside) = TcS $ \ env -> TcM.setTcLevel lvl (thing_inside env) -nestImplicTcS :: EvBindsVar +nestImplicTcS :: SkolemInfoAnon -> EvBindsVar -> TcLevel -> TcS a -> TcS a -nestImplicTcS ev_binds_var inner_tclvl (TcS thing_inside) +nestImplicTcS skol_info ev_binds_var inner_tclvl (TcS thing_inside) = TcS $ \ env@(TcSEnv { tcs_inerts = old_inert_var }) -> - do { inerts <- TcM.readTcRef old_inert_var - - -- resetInertcans: initialise the inert_cans from the inert_givens of the - -- parent so that the child is not polluted with the parent's inert Wanteds - -- See Note [trySolveImplication] in GHC.Tc.Solver.Solve - -- All other InertSet fields are inherited - ; let nest_inert = pushCycleBreakerVarStack $ - resetInertCans $ - inerts + do { nest_inert <- mk_nested_inert_set skol_info old_inert_var ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList ; let nest_env = env { tcs_ev_binds = ev_binds_var @@ -1230,6 +1222,25 @@ nestImplicTcS ev_binds_var inner_tclvl (TcS thing_inside) ; checkForCyclicBinds ev_binds #endif ; return res } + where + mk_nested_inert_set skol_info old_inert_var + -- For an implication that comes from a static form (static e), + -- start with a completely empty inert set; in particular, no Givens + -- See (SF3) in Note [Grand plan for static forms] + -- in GHC.Iface.Tidy.StaticPtrTable + | StaticFormSkol <- skol_info + = return (emptyInertSet inner_tclvl) + + | otherwise + = do { inerts <- TcM.readTcRef old_inert_var + + -- resetInertCans: initialise the inert_cans from the inert_givens of the + -- parent so that the child is not polluted with the parent's inert Wanteds + -- See Note [trySolveImplication] in GHC.Tc.Solver.Solve + -- All other InertSet fields are inherited + ; return (pushCycleBreakerVarStack $ + resetInertCans $ + inerts) } nestFunDepsTcS :: TcS a -> TcS a nestFunDepsTcS (TcS thing_inside) ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -394,7 +394,7 @@ trySolveImplication (Implic { ic_tclvl = tclvl , ic_wanted = wanteds , ic_env = ct_loc_env , ic_info = info }) - = nestImplicTcS ev_binds_var tclvl $ + = nestImplicTcS info ev_binds_var tclvl $ do { let loc = mkGivenLoc tclvl info ct_loc_env givens = mkGivens loc given_ids ; solveSimpleGivens givens @@ -427,7 +427,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; (has_given_eqs, given_insols, residual_wanted) - <- nestImplicTcS ev_binds_var tclvl $ + <- nestImplicTcS info ev_binds_var tclvl $ do { let loc = mkGivenLoc tclvl info ct_loc_env givens = mkGivens loc given_ids ; solveSimpleGivens givens ===================================== compiler/GHC/Tc/Types.hs ===================================== @@ -689,9 +689,6 @@ data TcGblEnv tcg_top_loc :: RealSrcSpan, -- ^ The RealSrcSpan this module came from - tcg_static_wc :: TcRef WantedConstraints, - -- ^ Wanted constraints of static forms. - -- See Note [Constraints in static forms]. tcg_complete_matches :: !CompleteMatches, -- ^ Complete matches defined in this module. @@ -706,27 +703,6 @@ data TcGblEnv -- Definition sites of orphan identities will be identity modules, not semantic -- modules. --- Note [Constraints in static forms] --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --- --- When a static form produces constraints like --- --- f :: StaticPtr (Bool -> String) --- f = static show --- --- we collect them in tcg_static_wc and resolve them at the end --- of type checking. They need to be resolved separately because --- we don't want to resolve them in the context of the enclosing --- expression. Consider --- --- g :: Show a => StaticPtr (a -> String) --- g = static show --- --- If the @Show a0@ constraint that the body of the static form produces was --- resolved in the context of the enclosing expression, then the body of the --- static form wouldn't be closed because the Show dictionary would come from --- g's context instead of coming from the top level. - tcVisibleOrphanMods :: TcGblEnv -> ModuleSet tcVisibleOrphanMods tcg_env = mkModuleSet (tcg_mod tcg_env : imp_orphs (tcg_imports tcg_env)) ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -1447,6 +1447,9 @@ data Implication ic_info :: SkolemInfoAnon, -- See Note [Skolems in an implication] -- See Note [Shadowing in a constraint] + -- NB: Mostly ic_info is just there to help with error messages + -- but StaticFormSkol has a deeper significance; see (SF3) in + -- Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable ic_skols :: [TcTyVar], -- Introduced skolems; always skolem TcTyVars -- Their level numbers should be precisely ic_tclvl ===================================== compiler/GHC/Tc/Types/Origin.hs ===================================== @@ -334,6 +334,11 @@ data SkolemInfoAnon | UnkSkol CallStack + | DefaultSkol -- Used (only) during defaulting + + | StaticFormSkol -- Attached to an implication constraint that captures + -- the constraints from (static e) + -- | Use this when you can't specify a helpful origin for -- some skolem type variable. @@ -393,6 +398,8 @@ pprSkolInfo ReifySkol = text "the type being reified" pprSkolInfo RuntimeUnkSkol = text "Unknown type from GHCi runtime" pprSkolInfo ArrowReboundIfSkol = text "the expected type of a rebound if-then-else command" +pprSkolInfo StaticFormSkol = text "a static expression" +pprSkolInfo DefaultSkol = text "a constraint being defaulted" -- unkSkol -- For type variables the others are dealt with by pprSkolTvBinding. ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -108,7 +108,7 @@ module GHC.Tc.Utils.Monad( getTcEvBindsMap, setTcEvBindsMap, updTcEvBinds, getTcEvTyCoVars, chooseUniqueOccTc, getConstraintVar, setConstraintVar, - emitConstraints, emitStaticConstraints, emitSimple, emitSimples, + emitConstraints, emitSimple, emitSimples, emitImplication, emitImplications, ensureReflMultiplicityCo, emitDelayedErrors, emitHole, emitHoles, emitNotConcreteError, discardConstraints, captureConstraints, tryCaptureConstraints, @@ -296,7 +296,6 @@ initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc = ; zany_n_var <- newIORef 0 ; dependent_files_var <- newIORef [] ; dependent_dirs_var <- newIORef [] - ; static_wc_var <- newIORef emptyWC ; cc_st_var <- newIORef newCostCentreState ; th_topdecls_var <- newIORef [] ; th_foreign_files_var <- newIORef [] @@ -396,7 +395,6 @@ initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc = , tcg_defaulting_plugins = [] , tcg_hf_plugins = [] , tcg_top_loc = loc - , tcg_static_wc = static_wc_var , tcg_complete_matches = [] , tcg_cc_st = cc_st_var , tcg_next_wrapper_num = next_wrapper_num @@ -1984,11 +1982,6 @@ getConstraintVar = do { env <- getLclEnv; return (tcl_lie env) } setConstraintVar :: TcRef WantedConstraints -> TcM a -> TcM a setConstraintVar lie_var = updLclEnv (\ env -> env { tcl_lie = lie_var }) -emitStaticConstraints :: WantedConstraints -> TcM () -emitStaticConstraints static_lie - = do { gbl_env <- getGblEnv - ; updTcRef (tcg_static_wc gbl_env) (`andWC` static_lie) } - emitConstraints :: WantedConstraints -> TcM () emitConstraints ct | isEmptyWC ct View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/135152ba2b0d9cac0eb7944d355674c2... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/135152ba2b0d9cac0eb7944d355674c2... You're receiving this email because of your account on gitlab.haskell.org.