[Git][ghc/ghc][wip/T24359] 2 commits: approach from Feb 10
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Tue Feb 11 15:25:27 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
6a9aee22 by sheaf at 2025-02-11T16:20:57+01:00
approach from Feb 10
- - - - -
62a55f97 by sheaf at 2025-02-11T16:25:06+01:00
account for skolem escape in mightEqualLater
- - - - -
4 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Solve.hs
- testsuite/tests/typecheck/should_compile/TcSpecPragmas.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -57,7 +57,6 @@ import GHC.Tc.Zonk.TcType
import GHC.Tc.Zonk.Type
import GHC.Core( hasSomeUnfolding )
-import GHC.Core.FVs (exprSomeFreeVars)
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.Predicate
@@ -72,7 +71,6 @@ import GHC.Types.Basic
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.SrcLoc
-import GHC.Types.Unique.Set
import GHC.Builtin.Names( mkUnboundName )
import GHC.Unit.Module( Module, getModule )
@@ -82,15 +80,12 @@ import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.Bag
-import GHC.Data.Maybe( orElse, whenIsJust, expectJust )
+import GHC.Data.Maybe( orElse, whenIsJust )
import Control.Monad( unless )
import Data.Foldable ( toList )
-import qualified Data.Graph as Graph
import qualified Data.List.NonEmpty as NE
import Data.Maybe( mapMaybe )
-import qualified Data.Semigroup as S
-
{- -------------------------------------------------------------
Note [Overview of type signatures]
@@ -1048,57 +1043,41 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
<- tcRuleBndrs skol_info rule_bndrs $
tcInferRho spec_e
- -- (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.
+ -- (2) Clone these Wanteds, solve them, and zonk the original
+ -- Wanteds, in order to benefit from any unifications.
--
- -- See Note [Fully solving constraints for specialisation].
+ -- SLD TODO: write short note about this, including possible
+ -- shortcoming of too many unifications from instances.
- -- (2.1) Clone the Wanteds.
; ev_binds_var_clone <- newTcEvBinds
; spec_e_wanted_clone <- cloneWC spec_e_wanted
-
- -- (2.2) Solve the cloned Wanteds.
- ; simpl_spec_e_wanted_clone <- setTcLevel rhs_tclvl $
- runTcSWithEvBinds ev_binds_var_clone $
- solveWanteds spec_e_wanted_clone
-
- -- (2.3) Determine which cloned Wanteds were fully solved.
- ; not_fully_solved_ev_ids <-
- notFullySolvedWanteds ev_binds_var_clone simpl_spec_e_wanted_clone
-
- -- (2.4) Zonk the original Wanteds to benefit from any unifications in (2.2)
+ ; _ <- setTcLevel rhs_tclvl $
+ runTcSWithEvBinds ev_binds_var_clone $
+ solveWanteds spec_e_wanted_clone
; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted
- -- (2.5) Partition the original Wanteds into fully soluble Wanteds and the rest.
- ; let (other_wanteds, fully_soluble_wanteds) =
- partitionWC (`elemVarSet` not_fully_solved_ev_ids) spec_e_wanted
-
- -- (2.6) Fully solve the fully-soluble Wanteds.
+ -- (3) Compute which constraints we can plausibly quantify over.
; ev_binds_var <- newTcEvBinds
- ; simpl_fully_soluble <- setTcLevel rhs_tclvl $
- runTcSWithEvBinds ev_binds_var $
- solveWanteds fully_soluble_wanteds
- ; massertPpr (isSolvedWC simpl_fully_soluble) $
- vcat [ text "tcSpecPrag (SpecSigE): unexpected unsolved constraints for" <+> quotes (ppr nm) <> colon
- , ppr simpl_fully_soluble
- , text "original Wanteds:" <+> ppr spec_e_wanted
- , text "supposedly soluble Wanteds:" <+> ppr fully_soluble_wanteds
- , text "not_fully_solved_ev_ids:" <+> ppr not_fully_solved_ev_ids
- , text "spec_e:" <+> ppr spec_e
- ]
-
- -- (3) Quantify other constraints. The quantification candidates
- -- are the non-fully-soluble constraints computed in (2.5).
- ; (quant_cts, residual_wc) <- getRuleQuantCts other_wanteds
- ; let qevs = map ctEvId $ bagToList quant_cts
-
- -- (4) Emit the residual constraints, and wrap the expression
- -- in the evidence let bindings
+ ; (simple_cts, residual_wc) <- getRuleQuantCts spec_e_wanted
+
+ -- (4) Figure out which of the simple_cts we can fully solve using
+ -- instances (and thus specialise away)
+ ; traceTc "tcSpecPrag SpecSigE: computing fully soluble Wanteds {" empty
+ ; fully_soluble_evids <-
+ setTcLevel rhs_tclvl $
+ mkVarSet <$>
+ mapMaybeM fullySolveCt_maybe (bagToList simple_cts)
+ ; let (fully_soluble_cts, other_cts) = partitionBag ((`elemVarSet` fully_soluble_evids) . ctEvId) simple_cts
+ quant_cts = mkMinimalBySCs ctPred $ bagToList other_cts
+ qevs = map ctEvId quant_cts
+ non_quant_cts = filterBag (not . (`elemVarSet` mkVarSet qevs) . ctEvId) other_cts
+ ; traceTc "tcSpecPrag SpecSigE: computed fully soluble Wanteds }" (ppr fully_soluble_cts)
+
+ -- (5) Emit the residual constraints (that we are not quantifying over)
; let tv_bndrs = filter isTyVar rule_bndrs'
; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var
emptyVarSet tv_bndrs qevs
- residual_wc
+ (residual_wc `addSimples` fully_soluble_cts `addSimples` non_quant_cts)
; let lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var)) tc_spec_e
; traceTc "tcSpecPrag SpecSigE }" $
@@ -1107,14 +1086,14 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
, text "qevs:" <+> ppr qevs
, text "spec_e:" <+> ppr tc_spec_e
, text "inl:" <+> ppr inl
- , text "not_fully_solved_ev_ids:" <+> ppr not_fully_solved_ev_ids
- , text "fully_soluble_wanteds:" <+> ppr fully_soluble_wanteds
- , text "other_wanteds:" <+> ppr other_wanteds
+ , text "spec_e_wanted:" <+> ppr spec_e_wanted
, text "quant_cts:" <+> ppr quant_cts
, text "residual_wc:" <+> ppr residual_wc
+ , text "fully_soluble_wanteds:" <+> ppr fully_soluble_cts
+ , text "non_quant_cts:" <+> ppr non_quant_cts
]
- -- (5) Store the results in a SpecPragE record, which will be
+ -- (6) Store the results in a SpecPragE record, which will be
-- zonked and then consumed by the desugarer.
; return [SpecPragE { spe_fn_nm = nm
@@ -1126,77 +1105,23 @@ 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 = concatMap (map evid_from_vertex . toList)
- $ Graph.dfs
- (Graph.transposeG ev_graph)
- (map (expectJust "tcSpecPrag (computing fully solved)" . vertex_from_key) unsolved_ids)
- ; return (mkVarSet 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 <- evVarsOfTerm' body
- return [(ev_id, ev_id, nonDetEltsUniqSet 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
-
--- Like 'GHC.Tc.Types.Evidence.evVarsOfTerm', except that it properly computes
--- the 'VarSet' for an 'EvFun'.
-evVarsOfTerm' :: EvTerm -> TcM VarSet
-evVarsOfTerm' (EvExpr e) = return $ exprSomeFreeVars isEvVar e
-evVarsOfTerm' (EvTypeable _ ev) =
- case ev of
- EvTypeableTyCon _ e -> foldMapM evVarsOfTerm' e
- EvTypeableTyApp e1 e2 -> foldMapM evVarsOfTerm' [e1,e2]
- EvTypeableTrFun e1 e2 e3 -> foldMapM evVarsOfTerm' [e1,e2,e3]
- EvTypeableTyLit e -> evVarsOfTerm' e
-evVarsOfTerm' (EvFun { et_given = givens, et_binds = tcev_binds, et_body = body_id }) = do
- ev_binds <-
- bagToList <$>
- case tcev_binds of
- TcEvBinds var -> evBindMapBinds <$> getTcEvBindsMap var
- EvBinds binds -> return binds
- let lhs_evvars = map evBindVar ev_binds
- rhs_evvars <- foldMapM (evVarsOfTerm' . eb_rhs) ev_binds
+-- | Try to fully solve a constraint.
+fullySolveCt_maybe :: Ct -> TcM (Maybe EvId)
+fullySolveCt_maybe ct = do
+ throwaway_ev_binds_var <- newTcEvBinds
+ res_wc <-
+ runTcSWithEvBinds throwaway_ev_binds_var $
+ solveWanteds $ emptyWC { wc_simple = unitBag ct }
+ -- NB: don't use 'solveSimpleWanteds', as this will not
+ -- fully solve quantified constraints.
+ traceTc "fullySolveCt_maybe" $
+ vcat [ text "ct:" <+> ppr ct
+ , text "res_wc:" <+> ppr res_wc
+ ]
return $
- ( ( rhs_evvars `extendVarSet` body_id )
- `delVarSetList` lhs_evvars
- ) `delVarSetList` 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 = mapMaybeBag prune yes_impls }
- , wc { wc_simple = no_cts, wc_impl = mapMaybeBag prune 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 })
- prune :: Implication -> Maybe Implication
- prune i =
- if isEmptyWC ( ic_wanted i )
- then Nothing
- else Just i
+ if isSolvedWC res_wc
+ then Just $ ctEvId ct
+ else Nothing
--------------
tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1903,6 +1903,8 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
, can_unify tv (metaTyVarInfo tv) rhs_ty
-- this checks for CycleBreakerTvs and TyVarTvs; forgetting
-- the latter was #19106.
+ , all ((metaTyVarTcLevel tv `deeperThanOrSame`) . tcTyVarLevel)
+ (filter isSkolemTyVar (tyCoVarsOfTypeList rhs_ty))
= BindMe
-- See Examples 4, 5, and 6 from the Note
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -924,20 +924,20 @@ solveSimpleWanteds simples
go n limit wc
| n `intGtLimit` limit
= failWithTcS $ TcRnSimplifierTooManyIterations simples limit wc
- | isEmptyBag (wc_simple wc)
- = return (n,wc)
+ | isEmptyBag (wc_simple wc)
+ = return (n,wc)
- | otherwise
- = do { -- Solve
- wc1 <- solve_simple_wanteds wc
+ | otherwise
+ = do { -- Solve
+ wc1 <- solve_simple_wanteds wc
- -- Run plugins
- ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
+ -- Run plugins
+ ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
- ; if rerun_plugin
- then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
- ; go (n+1) limit wc2 } -- Loop
- else return (n, wc2) } -- Done
+ ; if rerun_plugin
+ then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
+ ; go (n+1) limit wc2 } -- Loop
+ else return (n, wc2) } -- Done
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
=====================================
testsuite/tests/typecheck/should_compile/TcSpecPragmas.hs
=====================================
@@ -50,7 +50,7 @@ tyEq ( _ :: Proxy a ) ( _ :: Proxy b ) =
Just HRefl -> 1.1
-- Check that we don't emit a "useless specialisation" warning, as the
--- specialisation allows us to drop dead code in the body of 'f7'.
+-- specialisation allows us to drop dead code in the body of 'tyEq'.
{-# SPECIALISE tyEq :: Typeable c => Proxy c -> Proxy c -> Float #-}
--------------------------------------------------------------------------------
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/2d65f88fb38d577e9001053501ad5881f407134c...62a55f97b4be925ad8f738898abe893f8c0499a8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/2d65f88fb38d577e9001053501ad5881f407134c...62a55f97b4be925ad8f738898abe893f8c0499a8
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/20250211/a51b3972/attachment-0001.html>
More information about the ghc-commits
mailing list