Simon Peyton Jones pushed to branch wip/T26315 at Glasgow Haskell Compiler / GHC Commits: 6a93a288 by Simon Peyton Jones at 2025-09-04T13:08:04+01:00 Wibbles - - - - - 8 changed files: - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Solver/Solve.hs-boot - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Tc/Gen/Sig.hs ===================================== @@ -741,7 +741,7 @@ Note that the same (Eq p) dictionary. Reason: we don't want to force them to be visibly equal at the call site. -* The `spec_bnrs`, which are lambda-bound in the specialised function `$sf`, +* The `spec_bndrs`, which are lambda-bound in the specialised function `$sf`, are a subset of `rule_bndrs`. spec_bndrs = @p (d2::Eq p) (x::Int) (y::p) @@ -759,7 +759,8 @@ This is done in three parts. (1) Typecheck the expression, capturing its constraints - (2) Solve these constraints + (2) Solve these constraints. When doing so, switch on `tcsmFullySolveQCIs`; + see wrinkle (NFS1) below. (3) Compute the constraints to quantify over, using `getRuleQuantCts` on the unsolved constraints returned by (2). @@ -795,6 +796,28 @@ This is done in three parts. of the form: forall @a @b d1 d2 d3. f d1 d2 d3 = $sf d1 d2 d3 +(NFS1) Consider + f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a + {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-} + This SPECIALISE is treated like an expression with a type signature, so + we instantiate the constraints, simplify them and re-generalise. From the + instantiation we get [W] d :: (forall x. Eq a => Eq (f x)) + and we want to generalise over that. We do not want to attempt to solve it + and then get stuck, and emit an error message. If we can't solve it, it is + much, much better to leave it alone. + + We still need to simplify quantified constraints that can be /fully solved/ + from instances, otherwise we would never be able to specialise them + away. Example: {-# SPECIALISE f @[] @a #-}. So: + + * The constraint solver has a mode flag `tcsmFullySolveQCIs` that says + "fully solve quantified constraint, or leave them alone + * When simplifying constraints in a SPECIALISE pragma, we switch on this + flag the `SpecPragE` case of `tcSpecPrag`. + + You might worry about the wasted work from failed attempts to fully-solve, but + it is seldom repeated (because the constraint solver seldom iterates much). + Note [Handling old-form SPECIALISE pragmas] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ NB: this code path is deprecated, and is scheduled to be removed in GHC 9.18, as per #25440. @@ -976,12 +999,11 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl) tcInferRho spec_e -- (2) Solve the resulting wanteds - -- When doing so, switch on `tcsmFullySolveQCIs`; see (WFA4) in - -- Note [Solving a Wanted forall-constraint] in GHC.Tc.Solver.Solve ; ev_binds_var <- newTcEvBinds ; spec_e_wanted <- setTcLevel rhs_tclvl $ runTcSWithEvBinds ev_binds_var $ setTcSMode (vanillaTcSMode { tcsmFullySolveQCIs = True }) $ + -- tcsmFullySolveQCIs: see (NFS1)a solveWanteds spec_e_wanted ; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -1028,15 +1028,15 @@ findInferredDiff annotated_theta inferred_theta ; let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) (mkCtLocEnv lcl_env) given_cts = mkGivens given_loc given_ids - ; (residual, _) <- runTcS $ - do { _ <- solveSimpleGivens given_cts - ; solveSimpleWanteds (listToBag (map mkNonCanonical wanteds)) } + ; (residual_wc, _) <- runTcS $ + do { _ <- solveSimpleGivens given_cts + ; solveSimpleWanteds (listToBag (map mkNonCanonical wanteds)) } -- NB: There are no meta tyvars fromn this level annotated_theta -- because we have either promoted them or unified them -- See `Note [Quantification and partial signatures]` Wrinkle 2 ; return (map (box_pred . ctPred) $ - bagToList residual) } + bagToList (wc_simple residual_wc)) } where box_pred :: PredType -> PredType box_pred pred = case classifyPredType pred of ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -1189,7 +1189,7 @@ tryDefaultGroup wanteds (Proposal assignments) | CtWanted wtd <- map ctEvidence wanteds ] ; residual <- solveSimpleWanteds (listToBag new_wanteds) - ; return $ if isEmptyBag residual then Just (tvs, subst) else Nothing } + ; return $ if isEmptyWC residual then Just (tvs, subst) else Nothing } | otherwise = return Nothing ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -834,7 +834,7 @@ tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w }) -> tryShortCutTcS $ -- tryTcS tries to completely solve some contraints do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w)) - ; return (isEmptyBag residual) } + ; return (isEmptyWC residual) } | otherwise -> return False } ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -196,9 +196,11 @@ import GHC.Types.Unique.Set( elementOfUniqSet ) import GHC.Types.Id import GHC.Types.Basic (allImportLevels) import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel) +import GHC.Types.SrcLoc import GHC.Unit.Module import qualified GHC.Rename.Env as TcM +import GHC.Rename.Env import GHC.Utils.Outputable import GHC.Utils.Panic @@ -213,12 +215,11 @@ import GHC.Exts (oneShot) import Control.Monad import Data.Foldable hiding ( foldr1 ) import Data.IORef +import Data.Maybe( catMaybes ) import Data.List ( mapAccumL ) import Data.List.NonEmpty ( nonEmpty ) import qualified Data.List.NonEmpty as NE import qualified Data.Semigroup as S -import GHC.Types.SrcLoc -import GHC.Rename.Env import GHC.LanguageExtensions as LangExt #if defined(DEBUG) @@ -920,11 +921,14 @@ vanillaTcSMode = TcSMode { tcsmPmCheck = False instance Outputable TcSMode where ppr (TcSMode { tcsmPmCheck = pm, tcsmEarlyAbort = ea , tcsmSkipOverlappable = so, tcsmFullySolveQCIs = fs }) - = text "TcSMode" <> (braces $ - text "pm=" <> ppr pm <> comma <> - text "ea=" <> ppr ea <> comma <> - text "so=" <> ppr so <> comma <> - text "fs=" <> ppr fs) + = text "TcSMode" <> (braces $ cat $ punctuate comma $ catMaybes $ + [ pp_one pm "PmCheck", pp_one ea "EarlyAbort" + , pp_one so "SkipOverlappable", pp_one fs "FullySolveQCIs" ]) + -- We get something like TcSMode{EarlyAbort,FullySolveQCIs}, + -- mentioning just the flags that are on + where + pp_one True s = Just (text s) + pp_one False _ = Nothing {- Note [TcSMode] ~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -119,22 +119,18 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (unifs1, simples1) <- reportUnifications $ -- See Note [Superclass iteration] - solveSimpleWanteds simples + ; (unifs1, wc1) <- reportUnifications $ -- See Note [Superclass iteration] + solveSimpleWanteds simples -- Any insoluble constraints are in 'simples' and so get rewritten -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet - -- Now try to solve any Wanted QCInsts in `simples1` - ; (simples', implics_from_qcis) <- solveWantedQCIs simples1 - -- Next, solve implications from wc_impl ; implics' <- if not definitely_redo_implications -- See Note [Superclass iteration] && unifs1 == 0 -- for this conditional then return implics else solveNestedImplications implics - ; let wc' = wc { wc_simple = simples' - , wc_impl = implics' `unionBags` implics_from_qcis } + ; let wc' = wc1 { wc_impl = wc_impl wc1 `unionBags` implics' } ; unif_happened <- resetUnificationFlag ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened @@ -1020,7 +1016,9 @@ solveSimpleGivens givens ; when (notNull new_givens) $ go new_givens } -solveSimpleWanteds :: Cts -> TcS Cts +solveSimpleWanteds :: Cts -> TcS WantedConstraints +-- Returns unsolved constraints, mostly just flat ones (Cts), +-- but also any unsolved implications arising from forall-constraints -- The result is not necessarily zonked solveSimpleWanteds simples = do { mode <- getTcSMode @@ -1032,43 +1030,59 @@ solveSimpleWanteds simples , text "Inerts:" <+> ppr inerts , text "Wanteds to solve:" <+> ppr simples ] - ; (n,wc) <- go 1 (solverIterations dflags) simples + ; (n,simples',implics') <- go (solverIterations dflags) 1 emptyBag simples + + ; let unsolved_wc = emptyWC { wc_simple = simples', wc_impl = implics' } ; traceTcS "solveSimpleWanteds end }" $ vcat [ text "iterations =" <+> ppr n - , text "residual =" <+> ppr wc ] - ; return wc } + , text "residual =" <+> ppr unsolved_wc ] + + ; return unsolved_wc } where - go :: Int -> IntWithInf -> Cts -> TcS (Int, Cts) + go :: IntWithInf -- Limit + -> Int -- Iteration number + -> Bag Implication -- Accumulating parameter: unsolved implications + -> Cts -- Try to solve these + -> TcS (Int, Cts, Bag Implication) -- See Note [The solveSimpleWanteds loop] - go n limit wc + go limit n implics wanted | n `intGtLimit` limit = failTcS $ TcRnSimplifierTooManyIterations - simples limit (emptyWC { wc_simple = wc }) - | isEmptyBag wc - = return (n,wc) + simples limit + (emptyWC { wc_simple = wanted, wc_impl = implics }) + + | isEmptyBag wanted + = return (n, wanted, implics) + | otherwise = do { -- Solve - wc1 <- solve_simple_wanteds wc + (wanted1, implics1) <- solve_one wanted + ; let implics2 = implics `unionBags` implics1 -- Run plugins - -- NB: runTcPluginsWanted has a fast path for empty wc1, - -- which is the common case - ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1 + -- NB: runTcPluginsWanted has a fast path for + -- empty wanted1, which is the common case + ; (rerun_plugin, wanted2) <- runTcPluginsWanted wanted1 ; if rerun_plugin then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin) - ; go (n+1) limit wc2 } -- Loop - else return (n, wc2) } -- Done + ; go limit (n+1) implics2 wanted2 } -- Loop + else return (n, wanted2, implics2) } -- Done -solve_simple_wanteds :: Cts -> TcS Cts --- Try solving these constraints --- Affects the unification state (of course) but not the inert set --- The result is not necessarily zonked -solve_simple_wanteds simples - = nestTcS $ do { solveSimples simples - ; getUnsolvedInerts } + solve_one :: Cts -> TcS (Cts, Bag Implication) + -- Try solving these constraints + -- Affects the unification state (of course) but not the inert set + -- The result is not necessarily zonked + solve_one simples + = nestTcS $ + do { solveSimples simples + ; simples' <- getUnsolvedInerts + -- Now try to solve any Wanted quantified + -- constraints (i.e. QCInsts) in `simples1` + ; solveWantedQCIs simples' } + {- Note [The solveSimpleWanteds loop] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1320,25 +1334,24 @@ where <binds> is filled in by solving the implication constraint. What we actually do is this: * In `solveForAll` we see if we have an identical quantified constraint - to solve it (using tryInertQCs), and then just add it to `inert_qcis :: [QCInst]` - See Note [Solving Wanted QCs from Given QCs] + to solve it (using tryInertQCs). In particular, solve a Wanted QCI + from an identical Given. This is more than a simple optimisation: + see Note [Solving Wanted QCs from Given QCs] -* In the main solver loop, `GHC.Tc.Solver.Solve.simplify_loop`: + If not, just stash it in `inert_qcis :: [QCInst]`. (If it's a Given + we can use it to solve other constraints; if a Wanted we will solve + it later using `solveWantedQCIs`.) - - We attempt to solve the `wc_simple` constraints with `solveSimpleWanteds` - Unsolved quantified constraints just accumulate in the `inert_qcis` field - of the `InertSet`. +* In the main `solveSimpleWanteds` (specifically `solve_one`): - - Then we use `solveWantedQCIs` to solve any quantified constraints. It usually - turns the `QCInst` into an `Implication`; but not invariably (WFA4) + - We attempt to solve the `wc_simple` constraints with `solveSimples` + Unsolved quantified constraints just accumulate in the `inert_qcis` field + of the `InertSet`. -Wrinkles: + - Then we use `solveWantedQCIs` to solve any quantified constraints. That + often turns the `QCInst` into an `Implication`; but not invariably (WFA4) -(WFA1) We can take a more straightforward path when there is a matching Given, e.g. - [W] dg :: forall c d. (Eq c, Ord d) => C x c d - In this case, it's better to directly solve the Wanted from the Given, instead - of building an implication. This is more than a simple optimisation; see - Note [Solving Wanted QCs from Given QCs]. +Wrinkles: (WFA2) Termination: see #19690. We want to maintain the invariant (QC-INV): @@ -1364,27 +1377,9 @@ Wrinkles: So the `IsQC` origin carries that info, and `GHC.Tc.Errors.Ppr.pprQCOriginExtra` prints the extra info. -(WFA4) Consider - f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a - {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-} - This SPECIALISE is treated like an expression with a type signature, so - we instantiate the constraints, simplify them and re-generalise. From the - instantiation we get [W] d :: (forall x. Eq a => Eq (f x)) - and we want to generalise over that. We do not want to attempt to solve it - and then get stuck, and emit an error message. If we can't solve it, it is - much, much better to leave it alone. - - We still need to simplify quantified constraints that can be /fully solved/ - from instances, otherwise we would never be able to specialise them - away. Example: {-# SPECIALISE f @[] @a #-}. So: - - * The constraint solver has a mode flag `tcsmFullySolveQCIs` that says - "fully solve quantified constraint, or leave them alone - * When simplifying constraints in a SPECIALISE pragma, we switch on this - flag (see `GHC.Tc.Gen.Sig.tcSpecPrag`, the `SpecSigE` case). - - You might worry about the wasted work from failed attempts to fully-solve, but - it is seldom repeated (because the constraint solver seldom iterates much). +(WFA4) When `tcsmFullySolveQCIs` is on, we adopt an all-or-nothing strategy: + either solve the forall-constraint /fully/ or do nothing at all. + Why? See (NFS1) in Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig (WFA5) Why not /always/ us the all-or-nothing strategy, so we don't need a flag? Several reasons: @@ -1579,7 +1574,7 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev = ev, qci_tvs = tvs return (Left ct) | otherwise - -> -- Commit to the (partuly or fully solved) implication + -> -- Commit to the (partly or fully solved) implication -- See (WFA5) in Note [Solving a Wanted forall-constraint] -- Record evidence and return residual implication -- NB: even if it is fully solved we must return it, because it is ===================================== compiler/GHC/Tc/Solver/Solve.hs-boot ===================================== @@ -2,7 +2,7 @@ module GHC.Tc.Solver.Solve where import Prelude( Bool ) import GHC.Tc.Solver.Monad( TcS ) -import GHC.Tc.Types.Constraint( Cts, Implication ) +import GHC.Tc.Types.Constraint( Cts, Implication, WantedConstraints ) -solveSimpleWanteds :: Cts -> TcS Cts +solveSimpleWanteds :: Cts -> TcS WantedConstraints trySolveImplication :: Implication -> TcS Bool ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -956,7 +956,14 @@ nestedEvIdsOfTerm tm = fvVarSet (filterFV isNestedEvId (evTermFVs tm)) evTermFVs :: EvTerm -> FV evTermFVs (EvExpr e) = exprFVs e evTermFVs (EvTypeable _ ev) = evFVsOfTypeable ev -evTermFVs (EvFun {}) = emptyFV -- See Note [Free vars of EvFun] +evTermFVs (EvFun { et_tvs = tvs, et_given = given + , et_binds = tc_ev_binds, et_body = v }) + = case tc_ev_binds of + TcEvBinds {} -> emptyFV -- See Note [Free vars of EvFun] + EvBinds binds -> addBndrsFV bndrs fvs + where + fvs = foldr (unionFV . evTermFVs . eb_rhs) (unitFV v) binds + bndrs = foldr ((:) . eb_lhs) (tvs ++ given) binds evTermFVss :: [EvTerm] -> FV evTermFVss = mapUnionFV evTermFVs @@ -975,12 +982,15 @@ Finding the free vars of an EvFun is made tricky by the fact the bindings et_binds may be a mutable variable. Fortunately, we can just squeeze by. Here's how. -* evTermFVs is used only by GHC.Tc.Solver.neededEvVars. -* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the - ic_binds field of an Implication -* So we can track usage via the processing for that implication, - (see Note [Tracking redundant constraints] in GHC.Tc.Solver). - We can ignore usage from the EvFun altogether. +* /During/ typechecking, `evTermFVs` is used only by `GHC.Tc.Solver.neededEvVars` + * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the + ic_binds field of an Implication + * So we can track usage via the processing for that implication, + (see Note [Tracking redundant constraints] in GHC.Tc.Solver). + We can ignore usage from the EvFun altogether. + +* /After/ typechecking `evTermFVs` is used by `GHC.Iface.Ext.Ast`, but by + then it has been zonked so we can get at the bindings. -} {- ********************************************************************* View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6a93a2883a2fba1653de0ea71ea57c68... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6a93a2883a2fba1653de0ea71ea57c68... You're receiving this email because of your account on gitlab.haskell.org.