[Git][ghc/ghc][wip/T24359] 2 commits: wip 2
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Jan 24 15:19:14 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
5ee12fb7 by sheaf at 2025-01-23T14:30:29+01:00
wip 2
- - - - -
3d52add4 by sheaf at 2025-01-24T16:17:18+01:00
first attempt at new approach for specialise expression
- - - - -
9 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/Monad.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Zonk/Type.hs
- hie.yaml
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
=====================================
@@ -59,6 +59,7 @@ import GHC.Utils.Misc ((<||>))
import Data.Function
import Data.List (sortBy)
import Data.Data (Data)
+import GHC.Data.Bag (Bag)
{-
************************************************************************
@@ -824,7 +825,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 +836,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_binds :: (TcEvBinds, Bag EvBind)
+ -- ^ "specialised call evidence bindings"
+ --
+ -- See Note [Handling new-form SPECIALISE pragmas]
+ -- in GHC.Tc.Gen.Sig
+ }
noSpecPrags :: TcSpecPrags
noSpecPrags = SpecPrags []
@@ -996,7 +1028,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,72 @@ 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
+ , spe_rule_binds = EvBinds rule_evbinds
+ -- BLUE bindings, let sd1 = d1, sd3 = d3
+ , spe_call_evvars = rule_evvars
+ -- RED dictionary binders d1, ..., d4
+ , spe_call_binds = (EvBinds non_quant_call_evbinds, call_evbinds)
+ -- RED bindings d1 = sd1, d2 = sd1, d3 = sd2, d4 = $fEqList ...
+ })
-- 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]
- -- 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
+ simpl_opts = initSimpleOpts dflags
+ core_call = simpleOptExprNoInline simpl_opts ds_call
+
+ (_, rule_lhs_args) = collectArgs ds_call
+
+ -- Yes, this is correct (rule_evvars defined using call_evbinds,
+ -- and spec_evvars defined using rule_evbinds)
+ spec_evvars =
+ map evBindVar (bagToList rule_evbinds)
+
+ -- 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
+
+ spec_evbinds =
+ non_quant_call_evbinds `unionBags` call_evbinds
+
+ ; spec_coreevbinds <- dsEvBinds spec_evbinds return
+
+ ; let
+ mk_spec_body spec_fun =
+ mkLets spec_coreevbinds $
+ mkCoreApps spec_fun 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 "non_quant_call_evbinds:" <+> ppr non_quant_call_evbinds
+ , text "call_evbinds:" <+> ppr call_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 "spec_coreevbinds:" <+> ppr spec_coreevbinds
+ , 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 +1041,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, runTcSWithEvBinds )
+import GHC.Tc.Solver.Monad( runTcS, runTcSSpecPrag )
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Monad
@@ -703,32 +703,112 @@ Note [Handling new-form SPECIALISE pragmas]
New-form SPECIALISE pragmas are described by GHC Proposal #493.
The pragma takes the form of a function application, possibly with intervening
-parens and type signatures, with a variable at the head. It may have rule
-for-alls at the top. e.g.
+parens and type signatures, with a variable at the head:
{-# SPECIALISE f1 @Int 3 #-}
- {-# SPECIALISE forall x xs. f2 (x:xs) #-}
- {-# SPECIALISE f3 :: Int -> Int #-}
- {-# SPECIALISE (f4 :: Int -> Int) 5 #-}
+ {-# SPECIALISE f2 :: Int -> Int #-}
+ {-# SPECIALISE (f3 :: Int -> Int) 5 #-}
+
+It may also have rule for-alls at the top, e.g.
+
+ {-# SPECIALISE forall x xs. f4 (x:xs) #-}
{-# SPECIALISE forall a. forall x xs. f5 @a @a (x:xs) #-}
See `GHC.Rename.Bind.checkSpecESigShape` for the shape-check.
+We are going to use the following (perhaps somewhat contrived) example to
+demonstrate the subtle aspects of the implementation:
-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
+ 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 @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
+ 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
+
+
Note that
@@ -757,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
@@ -771,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.
@@ -944,49 +1024,85 @@ 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)
- = do { -- Typecheck the expression, spec_e, capturing its constraints
+ -- 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)
; skol_info <- mkSkolemInfo skol_info_anon
- ; (rhs_tclvl, wanted, (rule_bndrs', (spec_e', _rho)))
+ ; (rhs_tclvl, wanted, (rule_bndrs', (tc_spec_e, _rho)))
<- tcRuleBndrs skol_info rule_bndrs $
tcInferRho spec_e
- -- Simplify the constraints enough to perform unificaitons
+ -- (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
- -- Quantify over the the constraints
- ; (quant_cts, residual_wanted) <- getRuleQuantCts 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)
- -- Wrap the call in bindings for any other constraints
- ; 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 lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var1)) spec_e'
- -- The free vars of `lhs_call` 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 spec_e'
- , text "inl:" <+> ppr inl ]
+ , 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_bndrs = qevs ++ rule_bndrs' -- Dependency order
- -- does not matter
- , spe_call = lhs_call
- , spe_inl = inl }] }
+ ; 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_binds = (TcEvBinds non_quant_binds, spec_call_binds)
+ }] }
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
@@ -1419,9 +1535,9 @@ in `getRuleQuantCts`. Why not?
* Equality constraints are unboxed, and that leads to complications
For example equality constraints from the LHS will emit coercion hole
Wanteds. These don't have a name, so we can't quantify over them directly.
- Instead, in `mk_one` in `getRuleQuantCts` in we'd have to invent a new EvVar
- for the coercion, fill the hole with the invented EvVar, and then quantify
- over the EvVar. Here is old code from `mk_one`
+ Instead, in `getRuleQuantCts`, we'd have to invent a new EvVar for the
+ coercion, fill the hole with the invented EvVar, and then quantify over the
+ EvVar. Here is old code from `mk_one`
do { ev_id <- newEvVar pred
; fillCoercionHole hole (mkCoVarCo ev_id)
; return ev_id }
@@ -1488,8 +1604,8 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted
; lhs_wanted <- liftZonkM $ zonkWC lhs_wanted
-- Note [The SimplifyRule Plan] step 3
- ; (quant_cts, residual_lhs_wanted) <-getRuleQuantCts lhs_wanted
- ; let qant_evs = map ctEvId (bagToTolist quant_cts)
+ ; (quant_cts, residual_lhs_wanted) <- getRuleQuantCts lhs_wanted
+ ; let quant_evs = map ctEvId (bagToList quant_cts)
; traceTc "simplifyRule" $
vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
@@ -1510,16 +1626,16 @@ getRuleQuantCts :: WantedConstraints -> TcM (Cts, WantedConstraints)
-- and attempt to solve them from the quantified constraints. Instead
-- we /partition/ the WantedConstraints into ones to quantify and ones
-- we can't quantify. We could use approximateWC instead, and leave
--- `wanted` unchanged; but then we'd have clone fresh binders and
+-- `wanted` unchanged; but then we'd have to clone fresh binders and
-- generate silly identity bindings. Seems more direct to do this.
--- Probably not a big eal wither way.
+-- Probably not a big deal wither way.
--
-- NB: we must look inside implications, because with
-- -fdefer-type-errors we generate implications rather eagerly;
-- see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
getRuleQuantCts wc
- = float_wc emptyVarSet wc
+ = return $ float_wc emptyVarSet wc
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_errors = errs })
@@ -1545,17 +1661,6 @@ getRuleQuantCts wc
EqPred {} -> False -- Note [RULE quantification over equalities]
_ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
- mk_one :: Ct -> TcM EvVar
- mk_one ct
- | CtWanted { ctev_dest = dest } <- ctEvidence ct
- , EvVarDest ev_id <- dest
- -- HoleDest can't happen because we don't quantify
- -- over EqPred: See rule_quant_ct above
- = return ev_id
-
- | otherwise
- = pprPanic "getRuleQuantCts" (ppr ct)
-
{- Note [Quantifying over equalities in RULES]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
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,18 @@ 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
+ -- 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 +911,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 +958,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/Monad.hs
=====================================
@@ -851,12 +851,13 @@ data TcSEnv
data TcSMode
= TcSVanilla
- | TcSHoleFits -- See Note [Speeding up valid hole-fits].
- -- In this moe we throw an exception if we come across an
- -- insoluble constraint, to fail-fast when checking for hole-fits.
+ | TcSHoleFits -- ^ Throw an exception if we come across an insoluble constraint,
+ -- to fail-fast when checking for hole-fits.
+ --
+ -- See Note [Speeding up valid hole-fits].
- | TcSSpecPrag -- Don't use instance declarations or upack forall constraints
- -- when simplifying a SPECIALISE pragma
+ | TcSSpecPrag -- ^ Don't use instance declarations or unpack forall constraints;
+ -- used when simplifying a SPECIALISE pragma.
deriving( Eq )
instance Outputable TcSMode where
@@ -996,7 +997,7 @@ runTcSWithEvBinds = runTcSWorker True TcSVanilla
runTcS :: TcS a -> TcM (a, EvBindMap)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; res <- runTcSWorker True TcSVanilla aev_binds_var tcs
+ ; res <- runTcSWorker True TcSVanilla ev_binds_var tcs
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; return (res, ev_binds) }
@@ -1006,7 +1007,7 @@ runTcS tcs
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcSWorker' True TcSHoleFits ev_binds_var tcs }
+ ; runTcSWorker True TcSHoleFits ev_binds_var tcs }
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
@@ -1018,16 +1019,16 @@ runTcSEqualities thing_inside
runTcSSpecPrag :: TcS a -> TcM (a, Bag EvBind)
runTcSSpecPrag thing_inside
= do { ev_binds_var <- TcM.newTcEvBinds
- ; res <- runTcSWorker True TcSSpecPrag ev_binds_var tcs
+ ; 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)
-runTcSInerts inerts tcs = do
+runTcSInerts inerts tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcWorker False TcSVanilla ev_binds_var $
+ ; runTcSWorker False TcSVanilla ev_binds_var $
do { setInertSet inerts
; a <- tcs
; new_inerts <- getInertSet
=====================================
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,32 @@ 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_binds = (non_quant_evbinds, call_evbinds) }))
= 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 (zonkTcEvBinds non_quant_evbinds) $ \ non_quant_evbinds' ->
+ runZonkBndrT (zonkEvBinds call_evbinds) $ \ call_evbinds' ->
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_binds = (non_quant_evbinds', call_evbinds')
+ }))
+ }}
{-
************************************************************************
=====================================
hie.yaml
=====================================
@@ -5,4 +5,4 @@
# cradle: {bios: {program: "./hadrian/hie-bios.bat"}}
#
# The format is documented here - https://github.com/mpickering/hie-bios
-cradle: {bios: {program: "./hadrian/hie-bios"}}
+cradle: {bios: {program: "./hadrian/hie-bios.bat"}}
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/32e0aa0571ac34032426a94b8f2f1be10002bdd9...3d52add4d0f8def6818adad064f129eca62afa6f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/32e0aa0571ac34032426a94b8f2f1be10002bdd9...3d52add4d0f8def6818adad064f129eca62afa6f
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/e1679d6e/attachment-0001.html>
More information about the ghc-commits
mailing list