[Git][ghc/ghc][wip/T24359] revert back to previous plan, adding tests etc
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Tue Jan 28 12:02:18 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
b92e5784 by sheaf at 2025-01-28T13:02:00+01:00
revert back to previous plan, adding tests etc
- - - - -
10 changed files:
- 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/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Zonk/Type.hs
- + testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
- testsuite/tests/simplCore/should_compile/all.T
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Hs/Binds.hs
=====================================
@@ -862,23 +862,8 @@ data TcSpecPrag
, spe_bndrs :: [Var]
-- ^ TyVars, EvVars, and Ids
- , spe_expr :: LHsExpr GhcTc
+ , spe_call :: 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
@@ -1027,7 +1012,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_expr = spec_e, spe_inl = inl })
+ ppr (SpecPragE { spe_bndrs = bndrs, spe_call = spec_e, spe_inl = inl })
= text (extractSpecPragName $ inl_src inl)
<+> hang (ppr bndrs) 2 (pprLExpr spec_e)
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -791,9 +791,6 @@ 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] #-}
@@ -930,22 +927,7 @@ dsSpec poly_rhs (
, 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
- -- SLD TODO: I am not using the bindings anywhere, only the LHS EvVars
- --
- -- On the face of it, this seems obviously incorrect (I am missing the
- -- BLUE let bindings), but I don't have a case that triggers a problem,
- -- while ADDING the BLUE bindings causes complications due to the fact
- -- that the 'sd's are defined by simplifying the 'd's, without cloning,
- -- so we naively get (loopy) recursive bindings.
-
- -- 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
+ , spe_call = the_call
})
-- SpecPragE case: See Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig
= do { ds_call <- unsetGOptM Opt_EnableRewriteRules $ -- Note [Desugaring RULE left hand sides]
@@ -953,69 +935,80 @@ dsSpec poly_rhs (
zapUnspecables $
dsLExpr the_call
+ -- Simplify the (desugared) call; see wrinkle (SP1)
+ -- in Note [Desugaring SPECIALISE pragmas]
; dflags <- getDynFlags
- ; let
- -- See (SP1) in Note [Desugaring SPECIALISE pragmas]
- simpl_opts = initSimpleOpts dflags
- core_call = simpleOptExprNoInline simpl_opts ds_call
- ; case collectSpecArgs poly_id core_call of {
+ ; 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 rule_lhs_args ->
- do { let
- -- 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 rule_lhs_args
- spec_bndrs mk_spec_body inl
+ ; 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
- } } } }
-dsSpec _ (SpecPragE{}) = panic "dsSpec: SpecPragE not zonked"
+ -- 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 ])
+
+ ; finishSpecPrag poly_nm poly_rhs
+ rule_bndrs poly_id lhs_args
+ spec_bndrs mk_spec_body inl } } }
-collectSpecArgs :: Id -> CoreExpr
- -> Maybe [CoreExpr]
+prepareSpecLHS :: Id -> [EvVar] -> CoreExpr
+ -> Maybe (VarSet, [CoreBind], [CoreExpr])
-- See (SP2) in Note [Desugaring SPECIALISE pragmas]
--- SLD TODO: good example for this is simpl016
-collectSpecArgs poly_id the_call
- = go the_call
+prepareSpecLHS poly_id evs the_call
+ = go (mkVarSet evs) [] the_call
where
- go :: CoreExpr
- -> Maybe [CoreExpr]
- go (Cast e _)
- = go e
- go (Let _bind e)
- = go e
- go e
+ 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
+
+ go qevs acc e
| (Var fun, args) <- collectArgs e
= assertPpr (fun == poly_id) (ppr fun $$ ppr poly_id) $
- Just args
+ 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)
+
finishSpecPrag :: Name -> CoreExpr -- RHS to specialise
-> [Var] -> Id -> [CoreExpr] -- RULE LHS pattern
-> [Var] -> (CoreExpr -> CoreExpr) -> InlinePragma -- Specialised form
=====================================
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, runTcSSpecPrag )
+import GHC.Tc.Solver.Monad( runTcS, runTcSSpecPragWithEvBinds )
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Monad
@@ -722,93 +722,20 @@ 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 t. forall x y z. f (x::[Proxy t]) y y [z] True #-}
-We want to generate:
-
- 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 -- We will refer to these as the
- sd2 = d4 -- "RULE RHS evidence bindings"
- in
- $sf @p @q sd1 sd2 x y z
- $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 -- We will refer to these as the
- d3 = sd1 -- "specialised call evidence bindings"
- d4 = sd2 --
- in
- f @[Proxy t] @p @p @[q] d1 d2 d3 d4 x y y [z] True
-
-Key observations:
-
- O1.
-
- The most important part is to **completely solve** the Eq [Int] constraint,
- so that we specialise the call to 'f' to a known dictionary. Without that,
- we're not doing any typeclass specialisation!
-
- O2.
-
- 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. 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])
- (x::[Int]) (y::p) (z::q).
-
- Note that:
-
- - We have separate binders for `d2` and `d3` even though they are
- the same (Eq p) dictionary. Reason: we don't want to force them to be
- visibly equal at the call site.
-
- - 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,
- e.g. if we instead had a RULE binder (d4' :: Eq q), we would have to either:
-
- - generate a RULE of the form
-
- forall ... @q (d4' :: Eq q). f d1 d2 d3 ($fEqList d4') = ...
-
- 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 ..).
-
- 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:
-
- - define 'let(non-rec) f = <f-rhs>'
- - refer to this shadowing 'f' in the last line of $sf
-
- This allows us to deal with functions that recursively call themselves,
- as opposed to simply writing
-
- $sf ... =
- let <dicts>
- in
- (<f-rhs>) @p @p @[q] d1 d2 d3 d4 x y y [z] True
+Example:
+ f :: forall a b. (Eq a, Eq b, Eq c) => a -> b -> c -> Bool -> blah
+ {-# SPECIALISE forall x y. f (x::Int) y y True #-}
+ -- y::p
+We want to generate:
+ RULE forall @p (d1::Eq Int) (d2::Eq p) (d3::Eq p) (x::Int) (y::p).
+ f @Int @p @p d1 d2 d3 x y y True
+ = $sf @p d2 x y
+ $sf @p (d2::Eq p) (x::Int) (y::p)
+ = let d1 = $fEqInt
+ d3 = d2
+ in <f-rhs> @p @p @Int (d1::Eq p) (d2::Eq p) (d3::Eq p) x y y True
Note that
@@ -835,26 +762,46 @@ Note that
spec_const_binds = let d1 = $fEqInt
d3 = d2
-How it works:
+This is done in three parts.
+
+ A. Typechecker: `GHC.Tc.Gen.Sig.tcSpecPrag`
+
+ (1) Typecheck the expression, capturing its constraints
+
+ (2) Simplify these constraints, in special TcSSpecPrag mode
+ SLD TODO add more details.
-* SLD TODO outdated: `GHC.Tc.Gen.Sig.tcSpecPrag` just typechecks the expression, putting the results
- into a `SpecPragE` record. Nothing very exciting happens here.
+ (3) Decide which constraints to quantify over, and quantify.
-* `GHC.Tc.Zonk.Type.zonkLTcSpecPrags` does a little extra work to collect any
- free type variables of the LHS. See Note [Free tyvars on rule LHS] in
- GHC.Tc.Zonk.Type. These weren't conveniently available earlier.
+ (4) Emit the residual (non-quantified) constraints, and wrap the
+ expression in a let binding for those constraints.
-* `GHC.HsToCore.Binds.dsSpec` does the clever stuff:
+ (5) Store all the information in a 'SpecPragE' record, to be consumed
+ by the desugarer.
- * Simplifies the expression. This is important because a type signature in the
- expression will have led to type/dictionary abstractions/applications. Now
- it should look like
- let <dict-binds> in f e1 e1 e3
+ B. Zonker: `GHC.Tc.Zonk.Type.zonkLTcSpecPrags`
- * SLD TODO outdated: `prepareSpecLHS` identifies the `spec_const_binds` (see above), discards
- the other dictionary bindings, and decomposes the call.
+ The zonker does a little extra work to collect any free type variables
+ of the LHS. See Note [Free tyvars on rule LHS] in GHC.Tc.Zonk.Type.
+ These weren't conveniently available earlier.
- * Then it can build the RULE and specialised function.
+ C. Desugarer: `GHC.HsToCore.Binds.dsSpec`.
+
+ This is where most of the clever stuff happens. See
+ Note [Desugaring SPECIALISE pragmas] in GHC.HsToCore.Binds for details,
+ but in brief:
+
+ (1) Simplify the expression. This is important because a type signature in
+ the expression will have led to type/dictionary abstractions/applications.
+ Now it should look like
+ let <dict-binds> in f d1 d2 d3
+
+ (2) `prepareSpecLHS` identifies the `spec_const_binds`, discards the other
+ dictionary bindings, and decomposes the call.
+
+ (3) Then we build the specialised function $sf, and concoct a RULE
+ of the form:
+ forall @a @b d1 d2 d3. f d1 d2 d3 = $sf d1 d2 d3
Note [Handling old-form SPECIALISE pragmas]
@@ -1027,84 +974,44 @@ 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)
+ ; traceTc "tcSpecPrag SpecSigE 1" (ppr nm $$ ppr spec_e)
; skol_info <- mkSkolemInfo skol_info_anon
; (rhs_tclvl, wanted, (rule_bndrs', (tc_spec_e, _rho)))
<- tcRuleBndrs skol_info rule_bndrs $
tcInferRho spec_e
- -- (2) Perform unifications:
- -- - clone the original constraints,
- -- - simplify these cloned constraints
- -- - zonk the original constraints
- ; wanted_clone <- cloneWC wanted
- ; _ <- setTcLevel rhs_tclvl $
- runTcS $
- solveWanteds wanted_clone
- ; wanted <- liftZonkM $ zonkWC wanted
-
- -- (3) Get the constraints we will quantify over (e.g. d1, ..., d4)
- ; (quant_cts, non_quant_wc) <- getRuleQuantCts wanted
- ; let qevs = map ctEvId (bagToList quant_cts)
-
- -- (4) Emit the residual constraints.
- ; non_quant_binds <- newTcEvBinds
+ -- (2) Simplify the constraints, in special TcSSpecPrag mode
+ ; ev_binds_var <- newTcEvBinds
+ ; wanted <- setTcLevel rhs_tclvl $
+ runTcSSpecPragWithEvBinds ev_binds_var $
+ solveWanteds wanted
+
+ -- (3) Quantify over the constraints
+ ; qevs <- mapM newEvVar $
+ ctsPreds $
+ approximateWC False wanted
+
+ -- (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 non_quant_binds
+ ; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var
emptyVarSet tv_bndrs qevs
- 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 }" $
+ wanted
+ ; let lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var)) tc_spec_e
+
+ ; traceTc "tcSpecPrag:SpecSigE" $
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
- , 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)
- }] }
+ , 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 }] }
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -3,6 +3,7 @@
-- | Solving Class constraints CDictCan
module GHC.Tc.Solver.Dict (
solveDict, solveDictNC,
+ shortCutSolver,
checkInstanceOK,
matchLocalInst, chooseInstance,
makeSuperClasses, mkStrictSuperClasses,
@@ -771,7 +772,6 @@ wantShortCut dflags ev_w ev_i =
-- 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 (xopt LangExt.IncoherentInstances dflags)
-- If IncoherentInstances is on then we cannot rely on coherence of proofs
@@ -788,6 +788,12 @@ shortCutSolver :: DynFlags
-> CtEvidence -- Work item
-> TcS Bool -- True <=> success
shortCutSolver dflags ev_w
+ | isIPLikePred (ctEvPred ev_w)
+ -- Not for implicit parameters (#18627)
+ -- TODO: we should probably also reject QCs,
+ -- e.g. ( forall a. Eq a => IP "ip" a )
+ = return False
+ | otherwise
= do { ev_binds_var <- getTcEvBindsVar
; ev_binds <- assertPpr (not (isCoEvBindsVar ev_binds_var )) (ppr ev_w) $
getTcEvBindsMap ev_binds_var
@@ -812,46 +818,51 @@ shortCutSolver dflags ev_w
try_solve_from_instance -- See Note [Shortcut try_solve_from_instance]
:: (EvBindMap, DictMap DictCt) -> CtEvidence
-> MaybeT TcS (EvBindMap, DictMap DictCt)
- try_solve_from_instance (ev_binds, solved_dicts) ev
- | let pred = ctEvPred ev
- , ClassPred cls tys <- classifyPredType pred
- = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc_w
- ; lift $ warn_custom_warn_instance inst_res loc_w
- -- See Note [Implementation of deprecated instances]
- ; case inst_res of
- OneInst { cir_new_theta = preds
- , cir_mk_ev = mk_ev
- , cir_canonical = canonical
- , cir_what = what }
- | safeOverlap what
- , all isTyFamFree preds -- Note [Shortcut solving: type families]
- -> do { let dict_ct = DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }
- solved_dicts' = addSolvedDict dict_ct solved_dicts
- -- solved_dicts': it is important that we add our goal
- -- to the cache before we solve! Otherwise we may end
- -- up in a loop while solving recursive dictionaries.
-
- ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
- ; loc' <- lift $ checkInstanceOK (ctEvLoc ev) what pred
- ; lift $ checkReductionDepth loc' pred
-
-
- ; evc_vs <- mapM (new_wanted_cached ev loc' solved_dicts') preds
- -- Emit work for subgoals but use our local cache
- -- so we can solve recursive dictionaries.
-
- ; let ev_tm = mk_ev (map getEvExpr evc_vs)
- ev_binds' = extendEvBinds ev_binds $
- mkWantedEvBind (ctEvEvId ev) canonical ev_tm
-
- ; foldlM try_solve_from_instance (ev_binds', solved_dicts') $
- freshGoals evc_vs }
-
- _ -> mzero }
+ try_solve_from_instance (ev_binds, solved_dicts) ev =
+ case classifyPredType pred of
+ ClassPred cls tys ->
+ do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc_w
+ ; lift $ warn_custom_warn_instance inst_res loc_w
+ -- See Note [Implementation of deprecated instances]
+ ; case inst_res of
+ OneInst { cir_new_theta = preds
+ , cir_mk_ev = mk_ev
+ , cir_canonical = canonical
+ , cir_what = what }
+ | safeOverlap what
+ , all isTyFamFree preds -- Note [Shortcut solving: type families]
+ -> do { let dict_ct = DictCt { di_ev = ev, di_cls = cls
+ , di_tys = tys, di_pend_sc = doNotExpand }
+ solved_dicts' = addSolvedDict dict_ct solved_dicts
+ -- solved_dicts': it is important that we add our goal
+ -- to the cache before we solve! Otherwise we may end
+ -- up in a loop while solving recursive dictionaries.
- | otherwise
- = mzero
+ ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
+ ; loc' <- lift $ checkInstanceOK (ctEvLoc ev) what pred
+ ; lift $ checkReductionDepth loc' pred
+
+
+ ; evc_vs <- mapM (new_wanted_cached ev loc' solved_dicts') preds
+ -- Emit work for subgoals but use our local cache
+ -- so we can solve recursive dictionaries.
+
+ ; let ev_tm = mk_ev (map getEvExpr evc_vs)
+ ev_binds' = extendEvBinds ev_binds $
+ mkWantedEvBind (ctEvEvId ev) canonical ev_tm
+
+ ; foldlM try_solve_from_instance (ev_binds', solved_dicts') $
+ freshGoals evc_vs }
+
+ _other_inst_res -> mzero }
+
+ ForAllPred _tvs _theta _body ->
+ -- TODO: implement short-cut solving for quantified constraints
+ mzero
+
+ _other_pred -> mzero
+ where
+ pred = ctEvPred ev
-- Use a local cache of solved dicts while emitting EvVars for new work
@@ -874,13 +885,16 @@ shortCutSolver dflags ev_w
tryInstances :: DictCt -> SolverStage ()
tryInstances dict_ct
- = Stage $ do { inerts <- getInertSet
- ; try_instances inerts dict_ct }
+ = Stage $ do { dflags <- getDynFlags
+ ; inerts <- getInertSet
+ ; mode <- getModeTcS
+ ; try_instances inerts dflags mode dict_ct }
-try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
+try_instances :: InertSet -> DynFlags -> TcSMode -> DictCt -> TcS (StopOrContinue ())
-- Try to use type-class instance declarations to simplify the constraint
-try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
- , di_tys = xis })
+try_instances inerts dflags mode
+ work_item@(DictCt { di_ev = ev, di_cls = cls
+ , di_tys = xis })
| isGiven ev -- Never use instances for Given constraints
= continueWith ()
-- See Note [No Given/Given fundeps]
@@ -889,30 +903,26 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
= do { setEvBindIfWanted ev EvCanonical (ctEvTerm solved_ev)
; stopWith ev "Dict/Top (cached)" }
+ | TcSSpecPrag <- mode
+ -- 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].
+ = do { shortcut_worked <- shortCutSolver dflags ev
+ ; if shortcut_worked
+ then stopWith ev "TcSSpecPrag DictCt: short-cut fully solved Wanted from instances"
+ else continueWith ()
+ }
+
| otherwise -- Wanted, but not cached
- = do { dflags <- getDynFlags
- ; mode <- getModeTcS
- ; 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
- ; updSolvedDicts what work_item
- ; chooseInstance ev lkup_res }
- _ -> -- NoInstance or NotSure
- -- We didn't solve it; so try functional dependencies
- continueWith () } } }
+ = do { lkup_res <- matchClassInst dflags inerts cls xis dict_loc
+ ; case lkup_res of
+ OneInst { cir_what = what }
+ -> do { insertSafeOverlapFailureTcS what work_item
+ ; updSolvedDicts what work_item
+ ; chooseInstance ev lkup_res }
+ _ -> -- NoInstance or NotSure
+ -- We didn't solve it; so try functional dependencies
+ continueWith () }
where
dict_loc = ctEvLoc ev
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Tc.Solver.Monad (
-- The TcS monad
TcS, TcSMode(..),
runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
- runTcSEqualities, runTcSSpecPrag,
+ runTcSEqualities, runTcSSpecPragWithEvBinds,
failTcS, failWithTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
@@ -994,6 +994,10 @@ csTraceTcM mk_doc
runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds = runTcSWorker True TcSVanilla
+-- | This version of 'runTcSWithEvBinds' uses the 'TcSSpecPrag' mode.
+runTcSSpecPragWithEvBinds :: EvBindsVar -> TcS a -> TcM a
+runTcSSpecPragWithEvBinds = runTcSWorker True TcSSpecPrag
+
runTcS :: TcS a -> TcM (a, EvBindMap)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
@@ -1015,14 +1019,6 @@ runTcSEqualities thing_inside
= do { ev_binds_var <- TcM.newNoTcEvBinds -- No bindings
; runTcSWorker True TcSVanilla ev_binds_var thing_inside }
--- | This version of runTcS uses mode TcSSpecPrag
-runTcSSpecPrag :: TcS a -> TcM (a, Bag EvBind)
-runTcSSpecPrag thing_inside
- = do { ev_binds_var <- TcM.newTcEvBinds
- ; res <- runTcSWorker True TcSSpecPrag ev_binds_var thing_inside
- ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
- ; return (res, evBindMapBinds ev_binds) }
-
-- | A variant of 'runTcS' that takes and returns an 'InertSet' for
-- later resumption of the 'TcS' session.
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -1053,7 +1053,7 @@ solveCt (CNonCanonical ev) = solveNC ev
solveCt (CIrredCan (IrredCt { ir_ev = ev })) = solveNC ev
solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs, eq_rhs = rhs }))
+ , eq_lhs = lhs, eq_rhs = rhs }))
= solveEquality ev eq_rel (canEqLHSType lhs) rhs
solveCt (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
@@ -1211,8 +1211,25 @@ solveForAllNC ev tvs theta pred
solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel
-> TcS (StopOrContinue Void)
-- Precondition: already rewritten by inert set
-solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
- tvs theta pred _fuel
+solveForAll ev tvs theta pred fuel
+ = do { mode <- getModeTcS
+ ; solve_forAll ev tvs theta pred fuel mode
+ }
+
+solve_forAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType
+ -> ExpansionFuel -> TcSMode
+ -> TcS (StopOrContinue Void)
+solve_forAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
+ tvs theta pred fuel mode
+ | TcSSpecPrag <- mode
+ = do { dflags <- getDynFlags
+ ; shortcut_worked <- shortCutSolver dflags ev
+ ; if shortcut_worked
+ then stopWith ev "TcSSpecPrag QC: short-cut fully solved Wanted from instances"
+ else do { addInertForAll qci
+ ; stopWith ev "TcSSpecPrag QC: Wanted kept as inert" }
+ }
+ | otherwise
= -- See Note [Solving a Wanted forall-constraint]
TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $
-- This setSrcSpan is important: the emitImplicationTcS uses that
@@ -1257,9 +1274,11 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
get_size pred = case classifyPredType pred of
ClassPred cls tys -> pSizeClassPred cls tys
_ -> pSizeType pred
+ qci = QCI { qci_ev = ev, qci_tvs = tvs
+ , qci_pred = pred, qci_pend_sc = fuel }
-- See Note [Solving a Given forall-constraint]
-solveForAll ev@(CtGiven {}) tvs _theta pred fuel
+solve_forAll ev@(CtGiven {}) tvs _theta pred fuel _mode
= do { addInertForAll qci
; stopWith ev "Given forall-constraint" }
where
=====================================
compiler/GHC/Tc/Zonk/Type.hs
=====================================
@@ -854,29 +854,20 @@ 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_expr = spec_e
- , spe_rule_binds = rule_evbinds
- , spe_call_evvars = call_evvars
- , spe_call_wrapper = call_wrapper }))
+ zonk_prag (L loc prag@(SpecPragE { spe_fn_id = poly_id
+ , spe_bndrs = bndrs
+ , spe_call = spec_e }))
= 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 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_expr = spec_e'
- , spe_rule_binds = rule_evbinds'
- , spe_call_evvars = call_evvars'
- , spe_call_wrapper = call_wrapper'
+ ; return (L loc (prag { spe_fn_id = poly_id'
+ , spe_bndrs = skol_tvs ++ bndrs'
+ , spe_call = spec_e'
}))
}}
=====================================
testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
=====================================
@@ -0,0 +1,51 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module DsSpecPragmas where
+
+-- Some specialise pragmas that are difficult to generate the correct RULE for.
+
+--------------------------------------------------------------------------------
+
+f1 :: ( Num a, Eq b ) => a -> b -> Int
+f1 _ _ = 111
+
+-- Make sure we don't generate a rule with an LHS of the form
+--
+-- forall @e (d :: Eq e). f @[e] ($fEqList d) = ...
+--
+-- but rather
+--
+-- forall @e (d :: Eq [e]). f @[e] d = ...
+{-# SPECIALISE f1 :: Eq [e] => Word -> [e] -> Int #-}
+
+--------------------------------------------------------------------------------
+
+f2 :: ( Eq a, Eq b ) => a -> b -> Int
+f2 a b = if ( a == a ) == ( b == b ) then 1 else 2
+
+-- Make sure the rule LHS is of the form
+--
+-- f2 @c @c d1 d2 and not f2 @c @c d d
+{-# SPECIALISE f2 :: Eq c => c -> c -> Int #-}
+
+--------------------------------------------------------------------------------
+
+f3 :: ( Eq a, forall x. Eq x => Eq ( f x ) ) => f a -> Bool
+f3 z = z == z
+
+-- Discharge the quantified constraint but keep the 'Eq' constraint
+{-# SPECIALISE f3 :: Eq c => [ c ] -> Bool #-}
+
+-- Discharge the 'Eq' constraint but keep the quantified constraint
+{-# SPECIALISE f3 :: ( forall y. Eq y => Eq ( g y ) ) => g Int -> Bool #-}
+
+--------------------------------------------------------------------------------
+
+f4 :: Monad m => a -> m a
+f4 = return
+
+-- Check we can deal with locally quantified variables in constraints,
+-- in this case 'Monad (ST s)'.
+{-# SPECIALISE f4 :: b -> ST s b #-}
+
+--------------------------------------------------------------------------------
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -502,6 +502,7 @@ test('T23491d', [extra_files(['T23491.hs']), grep_errmsg(r'Static argument')], m
test('T23074', normal, compile, ['-O -ddump-rules'])
test('T23272', [only_ways(['ghci']), extra_hc_opts('-fno-unoptimized-core-for-interpreter -O')], ghci_script, ['T23272.script'])
test('T23567', [extra_files(['T23567A.hs'])], multimod_compile, ['T23567', '-O -v0'])
+test('DsSpecPragmas', normal, compile, ['-O -ddump-rules'])
# The -ddump-simpl of T22404 should have no let-bindings
test('T22404', [only_ways(['optasm']), check_errmsg(r'let') ], compile, ['-ddump-simpl -dsuppress-uniques'])
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -738,6 +738,7 @@ test('ExplicitSpecificityA1', normal, compile, [''])
test('ExplicitSpecificityA2', normal, compile, [''])
test('ExplicitSpecificity4', normal, compile, [''])
test('RuleEqs', normal, compile, [''])
+test('SpecPragmas', normal, compile, [''])
test('T17775-viewpats-a', normal, compile, [''])
test('T17775-viewpats-b', normal, compile_fail, [''])
test('T17775-viewpats-c', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b92e57841019d5339acd35d9c1f77435efcb7cf6
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b92e57841019d5339acd35d9c1f77435efcb7cf6
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/20250128/076fa4e0/attachment-0001.html>
More information about the ghc-commits
mailing list