[Git][ghc/ghc][wip/T24359] first attempt at new approach for specialise expression
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Jan 24 17:46:54 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
d18a1617 by sheaf at 2025-01-24T18:46:40+01:00
first attempt at new approach for specialise expression
- - - - -
8 changed files:
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Hs/Binds.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Zonk/Type.hs
Changes:
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -554,8 +554,8 @@ types/kinds are fully settled and zonked.
-- | Do a topological sort on a list of tyvars,
-- so that binders occur before occurrences
--- E.g. given [ a::k, k::*, b::k ]
--- it'll return a well-scoped list [ k::*, a::k, b::k ]
+-- E.g. given @[ a::k, k::Type, b::k ]@
+-- it'll return a well-scoped list @[ k::Type, a::k, b::k ]@.
--
-- This is a deterministic sorting operation
-- (that is, doesn't depend on Uniques).
=====================================
compiler/GHC/Hs/Binds.hs
=====================================
@@ -824,7 +824,8 @@ instance NoAnn AnnSig where
-- | Type checker Specialisation Pragmas
--
--- 'TcSpecPrags' conveys @SPECIALISE@ pragmas from the type checker to the desugarer
+-- 'TcSpecPrags' conveys @SPECIALISE@ pragmas from the type checker
+-- to the desugarer
data TcSpecPrags
= IsDefaultMethod -- ^ Super-specialised: a default method should
-- be macro-expanded at every call site
@@ -834,21 +835,51 @@ data TcSpecPrags
type LTcSpecPrag = Located TcSpecPrag
-- | Type checker Specialisation Pragma
--- This data type is used briefly, to communicate between the typechecker and renamer
+--
+-- This data type is used to communicate between the typechecker and
+-- the desugarer.
data TcSpecPrag
- = SpecPrag Id HsWrapper InlinePragma
- -- ^ The Id to be specialised, a wrapper that specialises the
- -- polymorphic function, and inlining spec for the specialised function
-
- | SpecPragE { spe_fn_nm :: Name -- The Name of the Id being specialised
- , spe_fn_id :: Id -- The Id being specialised
- -- The spe_fn_name may differ from (idName spe_fn_id) in the
- -- case of instance methods, where the Name is the class-op
- -- selector but the spe_fn_id is that for the local method
-
- , spe_bndrs :: [Var] -- TyVars, EvVars, and Ids
- , spe_call :: LHsExpr GhcTc -- The LHS of the RULE: a call of f
- , spe_inl :: InlinePragma }
+ -- | Old-form specialise pragma
+ = SpecPrag
+ Id
+ -- ^ 'Id' to be specialised
+ HsWrapper
+ -- ^ wrapper that specialises the polymorphic function
+ InlinePragma
+ -- ^ inlining spec for the specialised function
+ -- | New-form specialise pragma
+ | SpecPragE
+ { spe_fn_nm :: Name
+ -- ^ 'Name' of the 'Id' being specialised
+ , spe_fn_id :: Id
+ -- ^ 'Id' being specialised
+ --
+ -- Note that 'spe_fn_nm' may differ from @'idName' 'spe_fn_id'@
+ -- in the case of instance methods, where the 'Name' is the
+ -- class-op selector but the 'spe_fn_id' is that for the local method
+ , spe_inl :: InlinePragma
+ -- ^ (optional) INLINE annotation and activation phase annotation
+
+ , spe_bndrs :: [Var]
+ -- ^ TyVars, EvVars, and Ids
+ , spe_expr :: LHsExpr GhcTc
+ -- ^ The type-checked specialise expression
+ , spe_rule_binds :: TcEvBinds
+ -- ^ "RULE RHS evidence bindings"
+ --
+ -- See Note [Handling new-form SPECIALISE pragmas]
+ -- in GHC.Tc.Gen.Sig
+ , spe_call_evvars :: [Var]
+ -- ^ "specialised call evidence variables"
+ --
+ -- See Note [Handling new-form SPECIALISE pragmas]
+ -- in GHC.Tc.Gen.Sig
+ , spe_call_wrapper :: HsWrapper
+ -- ^ wrapper for the specialised call
+ --
+ -- See Note [Handling new-form SPECIALISE pragmas]
+ -- in GHC.Tc.Gen.Sig
+ }
noSpecPrags :: TcSpecPrags
noSpecPrags = SpecPrags []
@@ -996,7 +1027,7 @@ pprTcSpecPrags (SpecPrags ps) = vcat (map (ppr . unLoc) ps)
instance Outputable TcSpecPrag where
ppr (SpecPrag var _ inl)
= text (extractSpecPragName $ inl_src inl) <+> pprSpec var (text "<type>") inl
- ppr (SpecPragE { spe_bndrs = bndrs, spe_call = spec_e, spe_inl = inl })
+ ppr (SpecPragE { spe_bndrs = bndrs, spe_expr = spec_e, spe_inl = inl })
= text (extractSpecPragName $ inl_src inl)
<+> hang (ppr bndrs) 2 (pprLExpr spec_e)
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -791,6 +791,9 @@ The restrictions are:
Note [Desugaring SPECIALISE pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+SLD TODO: rewrite this whole note, using the same example as
+Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig.
+
Suppose we have f :: forall p q. (Ord p, Eq q) => p -> q -> q, and a pragma
{-# SPECIALISE forall x. f @[a] @[Int] x [3,4] #-}
@@ -823,7 +826,7 @@ Notice that
let { d = d2; d1 = $dfOrdInt } in f @Int @b (d2:Eq b)
Do no inlining in this "simple optimiser" phase: use `simpleOptExprNoInline`.
E.g. we don't want to turn
- let { d1=d; d2=d } in f d d --> f d d
+ let { d1=d; d2=d } in f d1 d2 --> f d d
because the latter is harder to match.
(SP2) the function `prepareSpecLHS` takes the simplified LHS `core_call` and
@@ -921,88 +924,74 @@ dsSpec poly_rhs (SpecPrag poly_id spec_co spec_inl)
rule_bndrs poly_id rule_lhs_args
spec_bndrs core_app spec_inl } }
-dsSpec poly_rhs (SpecPragE { spe_fn_nm = poly_nm
- , spe_fn_id = poly_id
- , spe_bndrs = bndrs
- , spe_call = the_call
- , spe_inl = inl })
+dsSpec poly_rhs (
+ SpecPragE
+ { spe_fn_nm = poly_nm
+ , spe_fn_id = poly_id
+ , spe_inl = inl
+ , spe_bndrs = bndrs
+ , spe_expr = the_call
+
+ -- BLUE bindings (sd1 = d1, sd2 = d3)
+ , spe_rule_binds = EvBinds rule_evbinds
+
+ -- RED binders (d1,..., d4)
+ , spe_call_evvars = rule_evvars
+ -- HsWrapper for RED evidence binds (let d1 = sd1, d2 = sd1, d3 = sd2, d4 = $fEqList ... in)
+ , spe_call_wrapper = call_wrapper
+ })
-- SpecPragE case: See Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig
- = do { ds_call <- zapUnspecables $ -- zapUnspecables: see
- dsLExpr the_call -- Note [Desugaring RULE left hand sides]
+ = do { ds_call <- unsetGOptM Opt_EnableRewriteRules $ -- Note [Desugaring RULE left hand sides]
+ unsetWOptM Opt_WarnIdentities $
+ zapUnspecables $
+ dsLExpr the_call
- -- Simplify the (desugared) call; see wrinkle (SP1)
- -- in Note [Desugaring SPECIALISE pragmas]
; dflags <- getDynFlags
- ; let simpl_opts = initSimpleOpts dflags
- core_call = simpleOptExprNoInline simpl_opts ds_call
-
- ; case prepareSpecLHS poly_id bndrs core_call of {
- Nothing -> do { diagnosticDs (DsRuleLhsTooComplicated ds_call core_call)
- ; return Nothing } ;
-
- Just (bndr_set, spec_const_binds, lhs_args) ->
-
- do { let const_bndrs = mkVarSet (bindersOfBinds spec_const_binds)
- all_bndrs = bndr_set `unionVarSet` const_bndrs
- -- all_bndrs: all binders in core_call that should be quantified
-
- -- rule_bndrs; see (SP3) in Note [Desugaring SPECIALISE pragmas]
- rule_bndrs = scopedSort (exprsSomeFreeVarsList (`elemVarSet` all_bndrs) lhs_args)
- spec_bndrs = filterOut (`elemVarSet` const_bndrs) rule_bndrs
-
- mk_spec_body fn_body = mkLets spec_const_binds $
- mkCoreApps fn_body lhs_args
-
- ; tracePm "dsSpec" (vcat [ text "poly_id" <+> ppr poly_id
- , text "bndrs" <+> ppr bndrs
- , text "all_bndrs" <+> ppr all_bndrs
- , text "const_bndrs" <+> ppr const_bndrs
- , text "ds_call" <+> ppr ds_call
- , text "core_call" <+> ppr core_call
- , text "core_call fvs" <+> ppr (exprFreeVars core_call)
- , text "spec_const_binds" <+> ppr spec_const_binds ])
-
+ ; let
+ -- See (SP1) in Note [Desugaring SPECIALISE pragmas]
+ simpl_opts = initSimpleOpts dflags
+ core_call = simpleOptExprNoInline simpl_opts ds_call
+
+ (_, rule_lhs_args) = collectArgs ds_call
+ -- TODO: why do we need rule_lhs_args?
+ -- Can't we get away without them by using the trick:
+ --
+ -- $sf sd1 sd2 = let[non-rec] f = <f-rhs> in
+ -- let d1 = sd1, d2 = sd1, d3 = sd2, d4 = $fEqList ... in
+ -- in f d1 d2 d3 d4
+
+ -- BLUE binders, in correspondence with the LHS of the blue bindings
+ spec_evvars =
+ map evBindVar (bagToList rule_evbinds)
+ -- Yes: rule_evbinds and not call_evbinds.
+ -- Re-read the example in Note [Handling new-form SPECIALISE pragmas]
+ -- if this is not clear.
+
+ -- The rule binders, including the RED binders d1, ..., d4
+ rule_bndrs = scopedSort $ bndrs ++ rule_evvars
+ -- The specialised $sf binders, including the BLUE binders sd1, sd2
+ spec_bndrs = scopedSort $ bndrs ++ spec_evvars
+
+ ; dsHsWrapper call_wrapper $ \ wrap_call ->
+ do { let mk_spec_body fn_rhs = wrap_call $ mkCoreApps fn_rhs rule_lhs_args
+ ; tracePm "dsSpec" (vcat [ text "poly_id:" <+> ppr poly_id
+ , text "bndrs:" <+> ppr bndrs
+ , text "ds_call:" <+> ppr ds_call
+ , text "core_call:" <+> ppr core_call
+ , text "rule_evbinds:" <+> ppr rule_evbinds
+ , text (replicate 40 '-')
+ , text "rule_evvars:" <+> ppr rule_evvars
+ , text "spec_evvars:" <+> ppr spec_evvars
+ , text "rule_bndrs:" <+> ppr rule_bndrs
+ , text "spec_bndrs:" <+> ppr spec_bndrs
+ , text "rule_lhs_args:" <+> ppr rule_lhs_args
+ ])
; finishSpecPrag poly_nm poly_rhs
- rule_bndrs poly_id lhs_args
- spec_bndrs mk_spec_body inl } } }
-
-prepareSpecLHS :: Id -> [EvVar] -> CoreExpr
- -> Maybe (VarSet, [CoreBind], [CoreExpr])
--- See (SP2) in Note [Desugaring SPECIALISE pragmas]
-prepareSpecLHS poly_id evs the_call
- = go (mkVarSet evs) [] the_call
- where
- go :: VarSet -- Quantified variables, or dependencies thereof
- -> [CoreBind] -- Reversed list of constant evidence bindings
- -> CoreExpr
- -> Maybe (IdSet, [CoreBind], [CoreExpr])
- go qevs acc (Cast e _)
- = go qevs acc e
- go qevs acc (Let bind e)
- | not (all isDictId bndrs) -- A normal 'let' is too complicated
- = Nothing
-
- | all (transfer_to_spec_rhs qevs) $
- rhssOfBind bind -- One of the `const_binds`
- = go qevs (bind:acc) e
-
- | otherwise
- = go (qevs `extendVarSetList` bndrs) acc e
- where
- bndrs = bindersOf bind
+ rule_bndrs poly_id rule_lhs_args
+ spec_bndrs mk_spec_body inl
- go qevs acc e
- | (Var fun, args) <- collectArgs e
- = assertPpr (fun == poly_id) (ppr fun $$ ppr poly_id) $
- Just (qevs, reverse acc, args)
- | otherwise
- = Nothing
-
- transfer_to_spec_rhs qevs rhs
- = isEmptyVarSet (exprSomeFreeVars is_quant_id rhs)
- where
- is_quant_id v = isId v && v `elemVarSet` qevs
- -- See Note [Desugaring SPECIALISE pragmas] wrinkle (SP4)
+ } }
+dsSpec _ (SpecPragE{}) = panic "dsSpec: SpecPragE not zonked"
finishSpecPrag :: Name -> CoreExpr -- RHS to specialise
-> [Var] -> Id -> [CoreExpr] -- RULE LHS pattern
@@ -1054,7 +1043,7 @@ finishSpecPrag poly_nm poly_rhs rule_bndrs poly_id rule_args
; tracePm "dsSpec" (vcat
[ text "fun:" <+> ppr poly_id
- , text "spec_bndrs:" <+> ppr spec_bndrs
+ , text "spec_bndrs:" <+> ppr spec_bndrs
, text "args:" <+> ppr rule_args ])
; return (unitOL (spec_id, spec_rhs), rule) }
-- NB: do *not* use makeCorePair on (spec_id,spec_rhs), because
=====================================
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 )
+import GHC.Tc.Solver.Monad( runTcS, runTcSSpecPrag )
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Monad
@@ -50,7 +50,7 @@ import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
import GHC.Tc.Utils.Env
import GHC.Tc.Types.Origin
-import GHC.Tc.Types.Evidence( HsWrapper(..), (<.>), TcEvBinds(..) )
+import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Zonk.TcType
@@ -720,26 +720,26 @@ We are going to use the following (perhaps somewhat contrived) example to
demonstrate the subtle aspects of the implementation:
f :: forall a b c d. (Eq a, Eq b, Eq c, Eq d) => a -> b -> c -> d -> Bool -> blah
- {-# SPECIALISE forall x y z. f (x::[Int]) y y [z] True #-}
+ {-# SPECIALISE forall t. forall x y z. f (x::[Proxy t]) y y [z] True #-}
We want to generate:
- RULE forall @p @q (d1::Eq [Int]) (d2::Eq p) (d3::Eq p) (d4 :: Eq [q]) (x::Int) (y::p) (z :: q).
- f @[Int] @p @p @[q] d1 d2 d3 d4 x y y [z] True
+ RULE forall @t @p @q (d1::Eq [Proxy t]) (d2::Eq p) (d3::Eq p) (d4 :: Eq [q]) (x::[Proxy t]) (y::p) (z :: q).
+ f @[Proxy t] @p @p @[q] d1 d2 d3 d4 x y y [z] True
= let
- sd1 = d2 --
- sd2 = d4 -- (*)
+ sd1 = d2 -- We will refer to these as the
+ sd2 = d4 -- "RULE RHS evidence bindings"
in
$sf @p @q sd1 sd2 x y z
- $sf @p @q (sd1::Eq p) (sd2::Eq [q]) (x::[Int]) (y::p) (z :: q)
+ $sf @t @p @q (sd1::Eq p) (sd2::Eq [q]) (x::[Proxy t]) (y::p) (z :: q)
= let(non-rec) f = <f-rhs> in
let
d1 = $fEqList $fEqInt --
- d2 = sd1 --
- d3 = sd1 --
- d4 = sd2 -- (**)
+ d2 = sd1 -- We will refer to these as the
+ d3 = sd1 -- "specialised call evidence bindings"
+ d4 = sd2 --
in
- f @[Int] @p @p @[q] d1 d2 d3 d4 x y y [z] True
+ f @[Proxy t] @p @p @[q] d1 d2 d3 d4 x y y [z] True
Key observations:
@@ -754,7 +754,8 @@ Key observations:
The `rule_bndrs`, over which the RULE is quantified, are all the variables
free in the call to `f`, /ignoring/ all dictionary simplification. Why?
Because we want to make the rule maximally applicable; provided the types
- match, the dictionaries should match.
+ match, the dictionaries should match. This is why, in the above example,
+ the rule binders are:
rule_bndrs = @p @q
(d1::Eq [Int]) (d2::Eq p) (d3::Eq p) (d4::Eq [q])
@@ -768,20 +769,31 @@ Key observations:
- We don't assume that the dictionary for 'Eq [q]' was obtained
from the top-level instance 'instance Eq x => Eq [x]'. If we did that,
- with a rule binder (d4 :: Eq q), we would either have to:
+ e.g. if we instead had a RULE binder (d4' :: Eq q), we would have to either:
- - generate a RULE LHS of the form
+ - generate a RULE of the form
- forall ... @q (d5 :: Eq q). f d1 d2 d3 ($fEqList d5)
+ forall ... @q (d4' :: Eq q). f d1 d2 d3 ($fEqList d4') = ...
- - find a way to "run the instance in reverse" to extract evidence for
- (Eq q) from (Eq [q]).
+ which is verboten (it matches on the structure of a dictionary), or
+
+ - "run the instance in reverse" to extract evidence for
+ (Eq q) from (Eq [q]), which is impossible to do in general.
"Partially solving" the Eq [q] constraint by using the instance doesn't
buy us anything; we can't do anything useful with the information that an
Eq [q] dictionary is of the form ($fEqList ..).
- O4.
+ To achieve this, we solve the constraints that originated from typechecking
+ the expression to specialise, but in the special 'TcSSpecPrag' mode, which
+ ensures that:
+
+ - We don't use instances (whether top-level instances or local instances
+ from quantified constraints), as those are not "reversible",
+ - EXCEPT that we **do** use the short-cut solver, so that we can fully
+ solve constraints such as the (Eq [Int]) constraint we mentioned in (O1).
+
+ O3.
In the body of $sf, note that we:
@@ -825,7 +837,7 @@ Note that
How it works:
-* `GHC.Tc.Gen.Sig.tcSpecPrag` just typechecks the expression, putting the results
+* SLD TODO outdated: `GHC.Tc.Gen.Sig.tcSpecPrag` just typechecks the expression, putting the results
into a `SpecPragE` record. Nothing very exciting happens here.
* `GHC.Tc.Zonk.Type.zonkLTcSpecPrags` does a little extra work to collect any
@@ -839,7 +851,7 @@ How it works:
it should look like
let <dict-binds> in f e1 e1 e3
- * `prepareSpecLHS` identifies the `spec_const_binds` (see above), discards
+ * SLD TODO outdated: `prepareSpecLHS` identifies the `spec_const_binds` (see above), discards
the other dictionary bindings, and decomposes the call.
* Then it can build the RULE and specialised function.
@@ -1012,6 +1024,7 @@ tcSpecPrag poly_id prag@(SpecSig _ fun_name hs_tys inl)
; return (SpecPrag poly_id wrap inl) }
tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
+ -- For running commentary, see Note [Handling new-form SPECIALISE pragmas]
= do { -- (1) Typecheck the expression, spec_e, capturing its constraints
let skol_info_anon = SpecESkol nm
; traceTc "tcSpecPrag: specSigE1" (ppr nm $$ ppr spec_e)
@@ -1031,33 +1044,67 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
; wanted <- liftZonkM $ zonkWC wanted
-- (3) Get the constraints we will quantify over (e.g. d1, ..., d4)
- ; (quant_cts, residual_wanted) <- getRuleQuantCts wanted
+ ; (quant_cts, non_quant_wc) <- getRuleQuantCts wanted
; let qevs = map ctEvId (bagToList quant_cts)
- -- (4) Emit the residual constraints, and wrap the call in the appropriate
- -- bindings.
- ; ev_binds_var1 <- newTcEvBinds
+ -- (4) Emit the residual constraints.
+ ; non_quant_binds <- newTcEvBinds
; let tv_bndrs = filter isTyVar rule_bndrs'
- ; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var1
+ ; emitResidualConstraints rhs_tclvl skol_info_anon non_quant_binds
emptyVarSet tv_bndrs qevs
- residual_wanted
- ; let residual_wrap = mkLHsWrap (WpLet (TcEvBinds ev_binds_var1))
- -- The free vars in this wrapper are `qevs`, plus the explicit `rule_bndrs`
- -- and any free tyvars of the above.
-
- ; traceTc "tcSpecPrag:SpecSigE" $
+ non_quant_wc
+
+ -- (5) Figure out sd1, sd2 (rule_rhs_wc) and the red bindings (rule_rhs_binds)
+ -- by solving "quant_cts" in the special TcSSpecPrag mode
+ ; traceTc "tcSpecPrag: computing BLUE Cts and RED bindings {" $
+ vcat [ text "quant_cts:" <+> ppr quant_cts ]
+ ; (rule_rhs_wc, spec_call_binds)
+ <- setTcLevel rhs_tclvl $
+ runTcSSpecPrag $
+ solveWanteds (emptyWC { wc_simple = quant_cts })
+ ; let rule_rhs_implics = wc_impl rule_rhs_wc
+ ; massertPpr (null rule_rhs_implics) $
+ vcat [ text "tcSpecPrag: unexpected non-simple constraints"
+ , text "quant_cts:" <+> ppr quant_cts
+ , text "implics:" <+> ppr rule_rhs_implics ]
+ ; traceTc "tcSpecPrag: computed BLUE Cts and RED bindings }" $
+ vcat [ text "quant_cts:" <+> ppr quant_cts
+ , text "blue Cts:" <+> ppr (wc_simple rule_rhs_wc) ]
+
+ -- (6) Figure out the blue bindings by solving the implication
+ -- [G] d1, d2, d3, d4 => [W] sd1, sd2
+ ; traceTc "tcSpecPrag:SpecSigE: computing BLUE bindings {" $
+ vcat [ text "qevs:" <+> ppr qevs
+ , text "rule_rhs_wc:" <+> ppr rule_rhs_wc
+ ]
+ ; (implics, rule_rhs_binds) <-
+ buildImplicationFor rhs_tclvl skol_info_anon tv_bndrs
+ qevs -- d1, d2, d3, d4
+ rule_rhs_wc -- sd1, sd2
+ ; emitImplications implics
+
+ ; traceTc "tcSpecPrag:SpecSigE: computed BLUE bindings }" $
vcat [ text "nm:" <+> ppr nm
, text "rule_bndrs':" <+> ppr rule_bndrs'
, text "qevs:" <+> ppr qevs
, text "spec_e:" <+> ppr tc_spec_e
- , text "inl:" <+> ppr inl ]
-
- ; return [SpecPragE { spe_fn_nm = nm
- , spe_fn_id = poly_id
- , spe_bndrs = qevs ++ rule_bndrs' -- Dependency order
- -- does not matter
- , spe_call = lhs_call
- , spe_inl = inl }] }
+ , text "inl:" <+> ppr inl
+ , text "non_quant:" <+> ppr non_quant_wc
+ , text (replicate 40 '-')
+ , text "spec_call_binds:" <+> ppr spec_call_binds
+ ]
+
+ ; return [SpecPragE { spe_fn_nm = nm
+ , spe_fn_id = poly_id
+ , spe_inl = inl
+ , spe_bndrs = rule_bndrs'
+ , spe_expr = tc_spec_e
+ , spe_rule_binds = rule_rhs_binds
+ , spe_call_evvars = qevs
+ , spe_call_wrapper =
+ WpLet (TcEvBinds non_quant_binds)
+ <.> WpLet (EvBinds spec_call_binds)
+ }] }
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -727,7 +727,9 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
do { -- First to try to solve it /completely/ from top level instances
-- See Note [Shortcut solving]
dflags <- getDynFlags
- ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
+ ; short_cut_worked <- if wantShortCut dflags ev_w ev_i
+ then shortCutSolver dflags ev_w
+ else return False
; if short_cut_worked
then stopWith ev_w "interactDict/solved from instance"
@@ -755,31 +757,37 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
= do { traceTcS "tryInertDicts:no" (ppr dict_w $$ ppr cls <+> ppr tys)
; continueWith () }
--- See Note [Shortcut solving]
-shortCutSolver :: DynFlags
- -> CtEvidence -- Work item
- -> CtEvidence -- Inert we want to try to replace
- -> TcS Bool -- True <=> success
-shortCutSolver dflags ev_w ev_i
- | isWanted ev_w
- , isGiven ev_i
+-- | See Note [Shortcut solving]
+wantShortCut :: DynFlags
+ -> CtEvidence -- ^ Work item
+ -> CtEvidence -- ^ Inert we want to try to replace
+ -> Bool
+wantShortCut dflags ev_w ev_i =
+ and
+ [ isWanted ev_w
+ , isGiven ev_i
-- We are about to solve a [W] constraint from a [G] constraint. We take
-- a moment to see if we can get a better solution using an instance.
-- Note that we only do this for the sake of performance. Exactly the same
-- programs should typecheck regardless of whether we take this step or
-- not. See Note [Shortcut solving]
+ , not (isIPLikePred (ctEvPred ev_w)) -- Not for implicit parameters (#18627)
- , not (isIPLikePred (ctEvPred ev_w)) -- Not for implicit parameters (#18627)
-
- , not (xopt LangExt.IncoherentInstances dflags)
+ , not (xopt LangExt.IncoherentInstances dflags)
-- If IncoherentInstances is on then we cannot rely on coherence of proofs
-- in order to justify this optimization: The proof provided by the
-- [G] constraint's superclass may be different from the top-level proof.
-- See Note [Shortcut solving: incoherence]
- , gopt Opt_SolveConstantDicts dflags
+ , gopt Opt_SolveConstantDicts dflags
-- Enabled by the -fsolve-constant-dicts flag
+ ]
+-- | See Note [Shortcut solving]
+shortCutSolver :: DynFlags
+ -> CtEvidence -- Work item
+ -> TcS Bool -- True <=> success
+shortCutSolver dflags ev_w
= do { ev_binds_var <- getTcEvBindsVar
; ev_binds <- assertPpr (not (isCoEvBindsVar ev_binds_var )) (ppr ev_w) $
getTcEvBindsMap ev_binds_var
@@ -795,8 +803,6 @@ shortCutSolver dflags ev_w ev_i
; setSolvedDicts solved_dicts'
; return True } }
- | otherwise
- = return False
where
-- This `CtLoc` is used only to check the well-staged condition of any
-- candidate DFun. Our subgoals all have the same stage as our root
@@ -886,7 +892,19 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
| otherwise -- Wanted, but not cached
= do { dflags <- getDynFlags
; mode <- getModeTcS
- ; lkup_res <- matchClassInst dflags mode inerts cls xis dict_loc
+ ; case mode of
+ -- SLD TODO: pass mode to try_instances and have this as a top-level guard
+ -- In TcSSpecPrag mode, we only want to "fully solve" constraints
+ -- from instances. Making partial progress using instances is
+ -- actively harmful; see Note [Handling new-form SPECIALISE pragmas].
+ { TcSSpecPrag ->
+ do { shortcut_worked <- shortCutSolver dflags ev
+ ; if shortcut_worked
+ then stopWith ev "TcSSpecPrag: short-cut fully solved from instances"
+ else continueWith ()
+ }
+ ; _ ->
+ do { lkup_res <- matchClassInst dflags inerts cls xis dict_loc
; case lkup_res of
OneInst { cir_what = what }
-> do { insertSafeOverlapFailureTcS what work_item
@@ -894,7 +912,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
; chooseInstance ev lkup_res }
_ -> -- NoInstance or NotSure
-- We didn't solve it; so try functional dependencies
- continueWith () }
+ continueWith () } } }
where
dict_loc = ctEvLoc ev
@@ -941,13 +959,11 @@ checkInstanceOK loc what pred
| otherwise
= loc
-matchClassInst :: DynFlags -> TcSMode
+matchClassInst :: DynFlags
-> InertSet
-> Class -> [Type]
-> CtLoc -> TcS ClsInstResult
-matchClassInst dflags mode inerts clas tys loc
- | TcSSpecPrag <- mode -- See Note [Handling new-form SPECIALISE pragmas]
- = return NoInstance -- in GHc.Tc.Gen.Sig
+matchClassInst dflags inerts clas tys loc
-- First check whether there is an in-scope Given that could
-- match this constraint. In that case, do not use any instance
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2020,7 +2020,7 @@ finishCanWithIrred reason ev
= do { -- Abort fast if we have any insoluble Wanted constraints,
-- and the TcSMode is TcsHoleFits
mode <- getModeTcS
- ; when (mode == TcSHoleFits && isInsolubleReason reason) failTcS
+ ; when (mode == TcSHoleFits && isInsolubleReason reason) failTcS
; continueWith $ Left $ IrredCt { ir_ev = ev, ir_reason = reason } }
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -373,10 +373,15 @@ data EvBindsVar
}
instance Data.Data TcEvBinds where
- -- Placeholder; we can't travers into TcEvBinds
+ -- Placeholder; we can't traverse into TcEvBinds
toConstr _ = abstractConstr "TcEvBinds"
gunfold _ _ = error "gunfold"
dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
+instance Data.Data EvBind where
+ -- Placeholder; we can't traverse into EvBind
+ toConstr _ = abstractConstr "TcEvBind"
+ gunfold _ _ = error "gunfold"
+ dataTypeOf _ = Data.mkNoRepType "EvBind"
{- Note [Coercion evidence only]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Zonk/Type.hs
=====================================
@@ -854,20 +854,31 @@ zonkLTcSpecPrags ps
= do { co_fn' <- don'tBind $ zonkCoFn co_fn
; id' <- zonkIdOcc id
; return (L loc (SpecPrag id' co_fn' inl)) }
- zonk_prag (L loc prag@(SpecPragE { spe_fn_id = poly_id
- , spe_bndrs = bndrs
- , spe_call = spec_e }))
+ zonk_prag (L loc prag@(SpecPragE { spe_fn_id = poly_id
+ , spe_bndrs = bndrs
+ , spe_expr = spec_e
+ , spe_rule_binds = rule_evbinds
+ , spe_call_evvars = call_evvars
+ , spe_call_wrapper = call_wrapper }))
= do { poly_id' <- zonkIdOcc poly_id
; skol_tvs_ref <- lift $ newTcRef []
; setZonkType (SkolemiseFlexi skol_tvs_ref) $
-- SkolemiseFlexi: see Note [Free tyvars on rule LHS]
- runZonkBndrT (zonkCoreBndrsX bndrs) $ \bndrs' ->
+ runZonkBndrT (zonkCoreBndrsX bndrs) $ \ bndrs' ->
+ runZonkBndrT (zonkCoreBndrsX call_evvars) $ \ call_evvars' ->
+ runZonkBndrT (zonkTcEvBinds rule_evbinds) $ \ rule_evbinds' ->
+ runZonkBndrT (zonkCoFn call_wrapper) $ \ call_wrapper' ->
do { spec_e' <- zonkLExpr spec_e
; skol_tvs <- lift $ readTcRef skol_tvs_ref
- ; return (L loc (prag { spe_fn_id = poly_id'
- , spe_bndrs = skol_tvs ++ bndrs'
- , spe_call = spec_e' })) } }
+ ; return (L loc (prag { spe_fn_id = poly_id'
+ , spe_bndrs = skol_tvs ++ bndrs'
+ , spe_expr = spec_e'
+ , spe_rule_binds = rule_evbinds'
+ , spe_call_evvars = call_evvars'
+ , spe_call_wrapper = call_wrapper'
+ }))
+ }}
{-
************************************************************************
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d18a1617dcc2dba8c33c71a6a84008af282844af
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d18a1617dcc2dba8c33c71a6a84008af282844af
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/20250124/04028a74/attachment-0001.html>
More information about the ghc-commits
mailing list