[Git][ghc/ghc][wip/T24359] WIP: another approach to 'fully solving' for tcSpecPrag
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Jan 31 15:49:08 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
8d333bcc by sheaf at 2025-01-31T16:48:59+01:00
WIP: another approach to 'fully solving' for tcSpecPrag
- - - - -
2 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -39,7 +39,7 @@ import GHC.Tc.Gen.HsType
import GHC.Tc.Solver( reportUnsolvedEqualities, pushLevelAndSolveEqualitiesX
, emitResidualConstraints )
import GHC.Tc.Solver.Solve( solveWanteds )
-import GHC.Tc.Solver.Monad( runTcS, runTcSSpecPragWithEvBinds )
+import GHC.Tc.Solver.Monad( runTcS, runTcSWithEvBinds )
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Monad
@@ -57,6 +57,7 @@ import GHC.Tc.Zonk.TcType
import GHC.Tc.Zonk.Type
import GHC.Core( hasSomeUnfolding )
+import GHC.Core.FVs (exprSomeFreeVarsList)
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.Predicate
@@ -80,12 +81,15 @@ import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.Bag
-import GHC.Data.Maybe( orElse, whenIsJust )
+import GHC.Data.Maybe( orElse, whenIsJust, expectJust )
import Control.Monad( unless )
import Data.Foldable ( toList )
+import qualified Data.Graph as Graph
+import Data.List ((\\), nub)
import qualified Data.List.NonEmpty as NE
import Data.Maybe( mapMaybe )
+import qualified Data.Semigroup as S
{- -------------------------------------------------------------
@@ -976,27 +980,67 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
let skol_info_anon = SpecESkol nm
; traceTc "tcSpecPrag SpecSigE 1" (ppr nm $$ ppr spec_e)
; skol_info <- mkSkolemInfo skol_info_anon
- ; (rhs_tclvl, wanted, (rule_bndrs', (tc_spec_e, _rho)))
+ ; (rhs_tclvl, spec_e_wanted, (rule_bndrs', (tc_spec_e, _rho)))
<- tcRuleBndrs skol_info rule_bndrs $
tcInferRho spec_e
- -- (2) Simplify the constraints, in special TcSSpecPrag mode
+ -- (2) Solve the Wanteds that arose from typechecking spec_e, but
+ -- in a special way: every original Wanted should be either fully solved
+ -- or left untouched.
+ --
+ -- We achieve this by:
+ --
+ -- 2.1. Clone the wanteds that arose from typechecking spec_e.
+ --
+ -- 2.2 Try to solve them, and look through the evidence to see which
+ -- ones we could fully solve.
+ --
+ -- 2.3 Separate the original Wanteds into two groups, those that
+ -- we could fully solve and those that we couldn't
+ --
+ -- The fully soluble ones get solved again (a bit wasteful).
+ -- The other ones either get quantified or emitted as residuals,
+ -- depending on whether they can be quantified (see 'getRuleQuantCts'.)
+ ; ev_binds_var_clone <- newTcEvBinds
+ ; spec_e_wanted_clone <- cloneWC spec_e_wanted
+ ; simpl_spec_e_wanted_clone <- setTcLevel rhs_tclvl $
+ runTcSWithEvBinds ev_binds_var_clone $
+ solveWanteds spec_e_wanted_clone
+ ; not_fully_solved <-
+ notFullySolvedWanteds ev_binds_var_clone simpl_spec_e_wanted_clone
+
+ ; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted
+
+ ; let (fully_soluble1, other1) =
+ partitionWC
+ (\ ev_id -> not (ev_id `elemVarSet` not_fully_solved))
+ spec_e_wanted
+
; ev_binds_var <- newTcEvBinds
- ; wanted <- setTcLevel rhs_tclvl $
- runTcSSpecPragWithEvBinds ev_binds_var $
- solveWanteds wanted
+ ; simpl_fully_soluble1 <- setTcLevel rhs_tclvl $
+ runTcSWithEvBinds ev_binds_var $
+ solveWanteds fully_soluble1
+ ; massertPpr (isSolvedWC simpl_fully_soluble1) $
+ vcat [ text "tcSpecPrag: fully soluble Wanteds couldn't be fully solved?"
+ , text "spec_e_wanted:" <+> ppr spec_e_wanted
+ , text "spec_e_wanted_clone:" <+> ppr spec_e_wanted_clone
+ , text "simpl_spec_e_wanted_clone:" <+> ppr simpl_spec_e_wanted_clone
+ , text "not_fully_solved:" <+> ppr not_fully_solved
+ , text "fully_soluble1:" <+> ppr fully_soluble1
+ , text "other1:" <+> ppr other1
+ , text "simpl_fully_soluble1:" <+> ppr simpl_fully_soluble1
+ ]
-- (3) Quantify over the constraints
- ; qevs <- mapM newEvVar $
- ctsPreds $
- approximateWC False wanted
+ ; (quant_cts, residual) <- getRuleQuantCts other1
+ ; let qevs = map ctEvId $ bagToList quant_cts
-- (4) Emit the residual (non-quantified) constraints,
-- and wrap the expression in the evidence let bindings
; let tv_bndrs = filter isTyVar rule_bndrs'
; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var
emptyVarSet tv_bndrs qevs
- wanted
+ residual
; let lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var)) tc_spec_e
; traceTc "tcSpecPrag:SpecSigE" $
@@ -1004,7 +1048,19 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
, text "rule_bndrs':" <+> ppr rule_bndrs'
, text "qevs:" <+> ppr qevs
, text "spec_e:" <+> ppr tc_spec_e
- , text "inl:" <+> ppr inl ]
+ , text "inl:" <+> ppr inl
+ , text (replicate 40 '=')
+ , text "spec_e_wanted:" <+> ppr spec_e_wanted
+ , text "spec_e_wanted_clone:" <+> ppr spec_e_wanted_clone
+ , text "simpl_spec_e_wanted_clone:" <+> ppr simpl_spec_e_wanted_clone
+ , text "not_fully_solved:" <+> ppr not_fully_solved
+ , text "fully_soluble1:" <+> ppr fully_soluble1
+ , text "other1:" <+> ppr other1
+ , text "simpl_fully_soluble1:" <+> ppr simpl_fully_soluble1
+ , text (replicate 40 '-')
+ , text "quant_cts:" <+> ppr quant_cts
+ , text "residual:" <+> ppr residual
+ ]
; return [SpecPragE { spe_fn_nm = nm
, spe_fn_id = poly_id
@@ -1015,6 +1071,67 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
+-- | Figure out the 'EvId's of all the Wanted constraints that
+-- are not fully solved, by inspecting their evidence terms.
+notFullySolvedWanteds :: EvBindsVar -> WantedConstraints -> TcM VarSet
+notFullySolvedWanteds ev_binds_var wc
+ = do { (unsolved_ids, ev_deps_edges) <- ev_binds_edges ev_binds_var wc
+ ; let (ev_graph, node_from_vertex, vertex_from_key) = Graph.graphFromEdges ev_deps_edges
+ evid_from_vertex v = case node_from_vertex v of ( ev_id, _, _ ) -> ev_id
+ reachable = mkVarSet
+ $ concatMap (map evid_from_vertex . toList)
+ $ Graph.dfs
+ (Graph.transposeG ev_graph)
+ (map (expectJust "tcSpecPrag (computing fully solved)" . vertex_from_key) unsolved_ids)
+ ; return reachable
+ }
+
+ev_binds_edges :: EvBindsVar -> WantedConstraints -> TcM ([EvId], [(EvId, EvId, [EvId])])
+ev_binds_edges ev_binds_var0 ( WC { wc_simple = cts, wc_impl = implics } )
+ = do { ev_binds <- getTcEvBindsMap ev_binds_var0
+ ; edges1 <- foldMapM ev_bind_edges (evBindMapBinds ev_binds)
+ ; let edges2 = foldMap (\ ct -> let i = ctEvId ct in ([i], [(i,i,[])])) cts
+ ; (insols3, edges3) <- foldMapM go_implic implics
+ ; return $
+ edges2 S.<> ( insols3, edges1 S.<> edges3 )
+ }
+ where
+ ev_bind_edges :: EvBind -> TcM [(EvId, EvId, [EvId])]
+ ev_bind_edges (EvBind { eb_lhs = ev_id, eb_rhs = body }) = do
+ ev_deps <- evVarsOfTermList body
+ return [(ev_id, ev_id, ev_deps)]
+ go_implic :: Implication -> TcM ([EvId], [(EvId, EvId, [EvId])])
+ go_implic ( Implic { ic_binds = ev_binds_var, ic_wanted = wc }) =
+ ev_binds_edges ev_binds_var wc
+
+evVarsOfTermList :: EvTerm -> TcM [EvId]
+evVarsOfTermList (EvExpr e) = return $ exprSomeFreeVarsList isEvVar e
+evVarsOfTermList (EvTypeable _ ev) =
+ case ev of
+ EvTypeableTyCon _ e -> concatMapM evVarsOfTermList e
+ EvTypeableTyApp e1 e2 -> concatMapM evVarsOfTermList [e1,e2]
+ EvTypeableTrFun e1 e2 e3 -> concatMapM evVarsOfTermList [e1,e2,e3]
+ EvTypeableTyLit e -> evVarsOfTermList e
+evVarsOfTermList (EvFun { et_given = givens, et_binds = tcev_binds, et_body = body_id }) = do
+ ev_binds <-
+ case tcev_binds of
+ TcEvBinds var -> evBindMapBinds <$> getTcEvBindsMap var
+ EvBinds binds -> return binds
+ return $
+ nub $
+ ( body_id : map evBindVar ( bagToList ev_binds ) ) \\ givens
+
+partitionWC :: (EvId -> Bool) -> WantedConstraints -> (WantedConstraints, WantedConstraints)
+partitionWC f wc@(WC { wc_simple = cts, wc_impl = implics }) =
+ let (yes_cts, no_cts) = partitionBag (f . ctEvId) cts
+ (yes_impls, no_impls) = unzipBag $ mapBag f_impl implics
+ in ( wc { wc_simple = yes_cts, wc_impl = yes_impls }
+ , wc { wc_simple = no_cts, wc_impl = no_impls } )
+ where
+ f_impl i@(Implic { ic_wanted = wc' }) =
+ let (yes, no) = partitionWC f wc'
+ in (i { ic_wanted = yes }, i { ic_wanted = no })
+
--------------
tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- A simpler variant of tcSubType, used for SPECIALISE pragmas
=====================================
testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
=====================================
@@ -78,6 +78,6 @@ f6 z = z == z
-- Quantify over this same quantified constraint, but discharge the
-- other dictionary constraints.
-{-# SPECIALISE f6 :: ( forall x. ( Eq x, Eq ( T x ) ) => Eq ( f x ) ) => f Int -> Bool #-}
+{-# SPECIALISE f6 :: ( forall y. ( Eq y, Eq ( T y ) ) => Eq ( g y ) ) => g Int -> Bool #-}
--------------------------------------------------------------------------------
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8d333bcc657ec63845ab5098f882f8af3fc1964a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8d333bcc657ec63845ab5098f882f8af3fc1964a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20250131/299b39ec/attachment-0001.html>
More information about the ghc-commits
mailing list