[Git][ghc/ghc][wip/T24359] 2 commits: new approach from Jan 31
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Tue Feb 4 09:31:47 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
ea8fe09b by sheaf at 2025-02-03T19:29:45+01:00
new approach from Jan 31
- - - - -
2d65f88f by sheaf at 2025-02-04T10:31:36+01:00
polish up new approach
- - - - -
9 changed files:
- 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/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
- testsuite/tests/typecheck/should_compile/SpecPragmas.hs → testsuite/tests/typecheck/should_compile/TcSpecPragmas.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -960,12 +960,16 @@ dsSpec poly_rhs (
; tracePm "dsSpec" (vcat [ text "poly_id" <+> ppr poly_id
, text "bndrs" <+> ppr bndrs
+ , text "lhs_args" <+> ppr lhs_args
+ , text "bndr_set" <+> ppr bndr_set
, text "all_bndrs" <+> ppr all_bndrs
+ , text "rule_bndrs" <+> ppr rule_bndrs
, text "const_bndrs" <+> ppr const_bndrs
- , text "ds_call" <+> ppr ds_call
- , text "core_call" <+> ppr core_call
+ , text "spec_bndrs" <+> ppr spec_bndrs
, text "core_call fvs" <+> ppr (exprFreeVars core_call)
- , text "spec_const_binds" <+> ppr spec_const_binds ])
+ , text "spec_const_binds" <+> ppr spec_const_binds
+ , text "ds_call" <+> ppr ds_call
+ , text "core_call" <+> ppr core_call ])
; finishSpecPrag poly_nm poly_rhs
rule_bndrs poly_id lhs_args
@@ -1004,7 +1008,7 @@ prepareSpecLHS poly_id evs the_call
= Nothing
transfer_to_spec_rhs qevs rhs
- = isEmptyVarSet (exprSomeFreeVars is_quant_id rhs)
+ = isEmptyVarSet $ exprSomeFreeVars is_quant_id rhs
where
is_quant_id v = isId v && v `elemVarSet` qevs
-- See Note [Desugaring SPECIALISE pragmas] wrinkle (SP4)
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -772,8 +772,9 @@ This is done in three parts.
(1) Typecheck the expression, capturing its constraints
- (2) Simplify these constraints, in special TcSSpecPrag mode
- SLD TODO add more details.
+ (2) Solve the Wanted constraints that arose from (1).
+ This is a bit subtle, as we don't want to allow arbitrary constraint
+ simplification. See Note [Fully solving constraints for specialisation].
(3) Decide which constraints to quantify over, and quantify.
@@ -807,6 +808,69 @@ This is done in three parts.
of the form:
forall @a @b d1 d2 d3. f d1 d2 d3 = $sf d1 d2 d3
+Note [Fully solving constraints for specialisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As far as specialisation is concerned, it is actively harmful to simplify
+constraints without fully solving them. Two key examples:
+
+f :: ∀ a t. (Eq a, ∀x. Eq x => Eq (t x)). t a -> Char
+{-# SPECIALISE f @Int #-}
+
+ Typechecking 'f' will result in [W] Eq Int, [W] ∀x. Eq x => Eq (t x).
+ We absolutely MUST leave the quantified constraint alone, because we want to
+ quantify over it. If we were to try to simplify it, we would emit an
+ implication and would thereafter never be able to quantify over the original
+ quantified constraint.
+
+ However, we still need to simplify quantified constraints that can be fully
+ solved from instances, otherwise we would never be able to specialise them
+ away. Example: {-# SPECIALISE f @a @[] #-}.
+
+g :: ∀ a. Eq a => a -> Bool
+{-# SPECIALISE g @[e] #-}
+
+ Typechecking 'g' will result in [W] Eq [e]. Were we to simplify this to
+ [W] Eq e, we would have difficulty generating a RULE for the specialisation:
+
+ $sg :: Eq e => [e] -> Bool
+
+ RULE ∀ e (d :: Eq [e]). g @[e] d = $sg @e (??? :: Eq e)
+ -- Can't fill in ??? because we can't run instances in reverse.
+
+ RULE ∀ e (d :: Eq e). g @[e] ($fEqList @e d) = $sg @e d
+ -- Bad RULE matching template: matches on the structure of a dictionary
+
+ Moreover, there is no real benefit to any of this, because the specialiser
+ can't do anything useful from the knowledge that a dictionary for 'Eq [e]' is
+ constructed from a dictionary for 'Eq e' using the 'Eq' instance for lists.
+
+ Note however that it is less important to tackle this problem in the typechecker,
+ as the desugarer would still be able to generate the correct RULE if we did
+ simplify 'Eq [e]' to 'Eq e'. See the second bullet point in (SP2) in
+ Note [Desugaring SPECIALISE pragmas] in GHC.HsToCore.Binds.
+
+The conclusion is this:
+
+ when solving the constraints that arise from a specialise pragma, following
+ the recipe described in Note [Handling new-form SPECIALISE pragmas], all
+ Wanteds should either be:
+ - fully solved (no free evidence variables), or
+ - left untouched.
+
+To achieve this, we proceed as follows:
+
+ 1. Clone the Wanteds that arose from typechecking the specialise expression.
+ 2. Solve these cloned Wanteds.
+ 3. Look through the evidence produced by the solver to determine which
+ of these Wanteds were fully solved using instances (no free evidence variables).
+ 4. Zonk the original Wanteds, to benefit from any unifications that happened in (2).
+ 5. Use the information obtained in (3) to partition the original Wanteds into
+ two sets: those that can be fully solved, and the rest.
+ 6. Fully solve the "fully soluble" Wanteds, and leave the rest alone (left
+ as candidates for quantification).
+ (NB: it is wasteful to do another round of solving here, but doing so is
+ more convenient than somehow transferring over the evidence terms from the
+ cloned Wanteds).
Note [Handling old-form SPECIALISE pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -978,7 +1042,7 @@ 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 SpecSigE 1" (ppr nm $$ ppr spec_e)
+ ; traceTc "tcSpecPrag SpecSigE {" (ppr nm $$ ppr spec_e)
; skol_info <- mkSkolemInfo skol_info_anon
; (rhs_tclvl, spec_e_wanted, (rule_bndrs', (tc_spec_e, _rho)))
<- tcRuleBndrs skol_info rule_bndrs $
@@ -988,80 +1052,71 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
-- in a special way: every original Wanted should be either fully solved
-- or left untouched.
--
- -- We achieve this by:
- --
- -- 2.1. Clone the wanteds that arose from typechecking spec_e.
- --
- -- 2.2 Try to solve them, and look through the evidence to see which
- -- ones we could fully solve.
- --
- -- 2.3 Separate the original Wanteds into two groups, those that
- -- we could fully solve and those that we couldn't
- --
- -- The fully soluble ones get solved again (a bit wasteful).
- -- The other ones either get quantified or emitted as residuals,
- -- depending on whether they can be quantified (see 'getRuleQuantCts'.)
+ -- See Note [Fully solving constraints for specialisation].
+
+ -- (2.1) Clone the Wanteds.
; ev_binds_var_clone <- newTcEvBinds
; spec_e_wanted_clone <- cloneWC spec_e_wanted
+
+ -- (2.2) Solve the cloned Wanteds.
; simpl_spec_e_wanted_clone <- setTcLevel rhs_tclvl $
runTcSWithEvBinds ev_binds_var_clone $
solveWanteds spec_e_wanted_clone
- ; not_fully_solved <-
+
+ -- (2.3) Determine which cloned Wanteds were fully solved.
+ ; not_fully_solved_ev_ids <-
notFullySolvedWanteds ev_binds_var_clone simpl_spec_e_wanted_clone
+ -- (2.4) Zonk the original Wanteds to benefit from any unifications in (2.2)
; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted
- ; let (fully_soluble1, other1) =
- partitionWC
- (\ ev_id -> not (ev_id `elemVarSet` not_fully_solved))
- spec_e_wanted
+ -- (2.5) Partition the original Wanteds into fully soluble Wanteds and the rest.
+ ; let (other_wanteds, fully_soluble_wanteds) =
+ partitionWC (`elemVarSet` not_fully_solved_ev_ids) spec_e_wanted
+ -- (2.6) Fully solve the fully-soluble Wanteds.
; ev_binds_var <- newTcEvBinds
- ; simpl_fully_soluble1 <- setTcLevel rhs_tclvl $
+ ; simpl_fully_soluble <- setTcLevel rhs_tclvl $
runTcSWithEvBinds ev_binds_var $
- solveWanteds fully_soluble1
- ; massertPpr (isSolvedWC simpl_fully_soluble1) $
- vcat [ text "tcSpecPrag: fully soluble Wanteds couldn't be fully solved?"
- , text "spec_e_wanted:" <+> ppr spec_e_wanted
- , text "spec_e_wanted_clone:" <+> ppr spec_e_wanted_clone
- , text "simpl_spec_e_wanted_clone:" <+> ppr simpl_spec_e_wanted_clone
- , text "not_fully_solved:" <+> ppr not_fully_solved
- , text "fully_soluble1:" <+> ppr fully_soluble1
- , text "other1:" <+> ppr other1
- , text "simpl_fully_soluble1:" <+> ppr simpl_fully_soluble1
- ]
-
- -- (3) Quantify over the constraints
- ; (quant_cts, residual) <- getRuleQuantCts other1
+ solveWanteds fully_soluble_wanteds
+ ; massertPpr (isSolvedWC simpl_fully_soluble) $
+ vcat [ text "tcSpecPrag (SpecSigE): unexpected unsolved constraints for" <+> quotes (ppr nm) <> colon
+ , ppr simpl_fully_soluble
+ , text "original Wanteds:" <+> ppr spec_e_wanted
+ , text "supposedly soluble Wanteds:" <+> ppr fully_soluble_wanteds
+ , text "not_fully_solved_ev_ids:" <+> ppr not_fully_solved_ev_ids
+ , text "spec_e:" <+> ppr spec_e
+ ]
+
+ -- (3) Quantify other constraints. The quantification candidates
+ -- are the non-fully-soluble constraints computed in (2.5).
+ ; (quant_cts, residual_wc) <- getRuleQuantCts other_wanteds
; let qevs = map ctEvId $ bagToList quant_cts
- -- (4) Emit the residual (non-quantified) constraints,
- -- and wrap the expression in the evidence let bindings
+ -- (4) Emit the residual constraints, and wrap the expression
+ -- in the evidence let bindings
; let tv_bndrs = filter isTyVar rule_bndrs'
; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var
emptyVarSet tv_bndrs qevs
- residual
+ residual_wc
; let lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var)) tc_spec_e
- ; traceTc "tcSpecPrag:SpecSigE" $
+ ; 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 (replicate 40 '=')
- , text "spec_e_wanted:" <+> ppr spec_e_wanted
- , text "spec_e_wanted_clone:" <+> ppr spec_e_wanted_clone
- , text "simpl_spec_e_wanted_clone:" <+> ppr simpl_spec_e_wanted_clone
- , text "not_fully_solved:" <+> ppr not_fully_solved
- , text "fully_soluble1:" <+> ppr fully_soluble1
- , text "other1:" <+> ppr other1
- , text "simpl_fully_soluble1:" <+> ppr simpl_fully_soluble1
- , text (replicate 40 '-')
+ , text "not_fully_solved_ev_ids:" <+> ppr not_fully_solved_ev_ids
+ , text "fully_soluble_wanteds:" <+> ppr fully_soluble_wanteds
+ , text "other_wanteds:" <+> ppr other_wanteds
, text "quant_cts:" <+> ppr quant_cts
- , text "residual:" <+> ppr residual
+ , text "residual_wc:" <+> ppr residual_wc
]
+ -- (5) Store the results in a SpecPragE record, which will be
+ -- zonked and then consumed by the desugarer.
+
; return [SpecPragE { spe_fn_nm = nm
, spe_fn_id = poly_id
, spe_bndrs = qevs ++ rule_bndrs' -- Dependency order
@@ -1076,14 +1131,14 @@ tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
notFullySolvedWanteds :: EvBindsVar -> WantedConstraints -> TcM VarSet
notFullySolvedWanteds ev_binds_var wc
= do { (unsolved_ids, ev_deps_edges) <- ev_binds_edges ev_binds_var wc
- ; let (ev_graph, node_from_vertex, vertex_from_key) = Graph.graphFromEdges ev_deps_edges
- evid_from_vertex v = case node_from_vertex v of ( ev_id, _, _ ) -> ev_id
- reachable = mkVarSet
- $ concatMap (map evid_from_vertex . toList)
- $ Graph.dfs
- (Graph.transposeG ev_graph)
- (map (expectJust "tcSpecPrag (computing fully solved)" . vertex_from_key) unsolved_ids)
- ; return reachable
+ ; let
+ (ev_graph, node_from_vertex, vertex_from_key) = Graph.graphFromEdges ev_deps_edges
+ evid_from_vertex v = case node_from_vertex v of (ev_id, _, _) -> ev_id
+ reachable = concatMap (map evid_from_vertex . toList)
+ $ Graph.dfs
+ (Graph.transposeG ev_graph)
+ (map (expectJust "tcSpecPrag (computing fully solved)" . vertex_from_key) unsolved_ids)
+ ; return (mkVarSet reachable)
}
ev_binds_edges :: EvBindsVar -> WantedConstraints -> TcM ([EvId], [(EvId, EvId, [EvId])])
@@ -1131,12 +1186,17 @@ partitionWC :: (EvId -> Bool) -> WantedConstraints -> (WantedConstraints, Wanted
partitionWC f wc@(WC { wc_simple = cts, wc_impl = implics }) =
let (yes_cts, no_cts) = partitionBag (f . ctEvId) cts
(yes_impls, no_impls) = unzipBag $ mapBag f_impl implics
- in ( wc { wc_simple = yes_cts, wc_impl = yes_impls }
- , wc { wc_simple = no_cts, wc_impl = no_impls } )
+ in ( wc { wc_simple = yes_cts, wc_impl = mapMaybeBag prune yes_impls }
+ , wc { wc_simple = no_cts, wc_impl = mapMaybeBag prune no_impls } )
where
f_impl i@(Implic { ic_wanted = wc' }) =
let (yes, no) = partitionWC f wc'
in (i { ic_wanted = yes }, i { ic_wanted = no })
+ prune :: Implication -> Maybe Implication
+ prune i =
+ if isEmptyWC ( ic_wanted i )
+ then Nothing
+ else Just i
--------------
tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -172,8 +172,10 @@ canDictCt ev cls tys
| otherwise
= Stage $
do { dflags <- getDynFlags
- ; let fuel | classHasSCs cls = wantedsFuel dflags
- | otherwise = doNotExpand
+ ; let fuel | classHasSCs cls
+ = wantedsFuel dflags
+ | otherwise
+ = doNotExpand
-- See Invariants in `CCDictCan.cc_pend_sc`
; continueWith (DictCt { di_ev = ev, di_cls = cls
, di_tys = tys, di_pend_sc = fuel }) }
@@ -842,7 +844,6 @@ shortCutSolver dflags ev_w
; 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.
@@ -856,10 +857,6 @@ shortCutSolver dflags ev_w
_other_inst_res -> mzero }
- ForAllPred _tvs _theta _body ->
- -- TODO: implement short-cut solving for quantified constraints
- mzero
-
_other_pred -> mzero
where
pred = ctEvPred ev
@@ -887,12 +884,11 @@ tryInstances :: DictCt -> SolverStage ()
tryInstances dict_ct
= Stage $ do { dflags <- getDynFlags
; inerts <- getInertSet
- ; mode <- getModeTcS
- ; try_instances inerts dflags mode dict_ct }
+ ; try_instances inerts dflags dict_ct }
-try_instances :: InertSet -> DynFlags -> TcSMode -> DictCt -> TcS (StopOrContinue ())
+try_instances :: InertSet -> DynFlags -> DictCt -> TcS (StopOrContinue ())
-- Try to use type-class instance declarations to simplify the constraint
-try_instances inerts dflags mode
+try_instances inerts dflags
work_item@(DictCt { di_ev = ev, di_cls = cls
, di_tys = xis })
| isGiven ev -- Never use instances for Given constraints
@@ -903,16 +899,6 @@ try_instances inerts dflags mode
= 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 { lkup_res <- matchClassInst dflags inerts cls xis dict_loc
; case lkup_res of
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2018,7 +2018,7 @@ finishCanWithIrred :: CtIrredReason -> CtEvidence
-> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred reason ev
= do { -- Abort fast if we have any insoluble Wanted constraints,
- -- and the TcSMode is TcsHoleFits
+ -- and the TcSMode is TcSHoleFits
mode <- getModeTcS
; when (mode == TcSHoleFits && isInsolubleReason reason) failTcS
=====================================
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, runTcSSpecPragWithEvBinds,
+ runTcSEqualities,
failTcS, failWithTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
@@ -856,14 +856,11 @@ data TcSMode
--
-- See Note [Speeding up valid hole-fits].
- | TcSSpecPrag -- ^ Don't use instance declarations or unpack forall constraints;
- -- used when simplifying a SPECIALISE pragma.
deriving( Eq )
instance Outputable TcSMode where
ppr TcSVanilla = text "TcSVanilla"
ppr TcSHoleFits = text "TcSHoleFits"
- ppr TcSSpecPrag = text "TcSSpecPrag"
---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
@@ -994,10 +991,6 @@ 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
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -1212,28 +1212,11 @@ solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFu
-> TcS (StopOrContinue Void)
-- Precondition: already rewritten by inert set
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
-{- SLD TODO
- | 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 { let qci = QCI { qci_ev = ev, qci_tvs = tvs
- , qci_pred = pred, qci_pend_sc = fuel }
- ; addInertForAll qci
- ; stopWith ev "TcSSpecPrag QC: Wanted kept as inert" }
- }
- | otherwise
--}
+ | CtGiven {} <- ev
+ -- See Note [Solving a Given forall-constraint]
+ = do { addInertForAll qci
+ ; stopWith ev "Given forall-constraint" }
+ | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc } <- ev
= -- See Note [Solving a Wanted forall-constraint]
TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $
-- This setSrcSpan is important: the emitImplicationTcS uses that
@@ -1279,11 +1262,6 @@ solve_forAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_l
ClassPred cls tys -> pSizeClassPred cls tys
_ -> pSizeType pred
- -- See Note [Solving a Given forall-constraint]
-solve_forAll ev@(CtGiven {}) tvs _theta pred fuel _mode
- = do { addInertForAll qci
- ; stopWith ev "Given forall-constraint" }
- where
qci = QCI { qci_ev = ev, qci_tvs = tvs
, qci_pred = pred, qci_pend_sc = fuel }
=====================================
testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
=====================================
@@ -6,7 +6,10 @@
module DsSpecPragmas where
-import Control.Monad.ST ( ST )
+import Control.Monad.ST
+ ( ST )
+import Data.Proxy
+ ( Proxy(..) )
-- Some specialise pragmas that are difficult to generate the correct RULE for.
@@ -17,22 +20,28 @@ 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) = ...
+-- forall @e (d :: Eq e). f1 @[e] ($fEqList d) = ...
--
-- but rather
--
--- forall @e (d :: Eq [e]). f @[e] d = ...
+-- forall @e (d :: Eq [e]). f1 @[e] d = ...
{-# SPECIALISE f1 :: Eq [e] => Word -> [e] -> Int #-}
+f1_qc :: ( forall x. Eq x => Eq ( f x ), Eq a, Num b ) => Proxy f -> a -> b -> Char
+f1_qc _ _ _ = 'q'
+
+-- Like 'f1', but with a local instance (quantified constraint).
+{-# SPECIALISE f1_qc :: ( forall y. Eq y => Eq ( g y ), Eq ( g e ) ) => Proxy g -> g e -> Word -> Char #-}
+
--------------------------------------------------------------------------------
-f2 :: ( Eq a, Eq b ) => a -> b -> Int
-f2 a b = if ( a == a ) == ( b == b ) then 1 else 2
+f2 :: ( Eq a, Eq b, Num c ) => a -> b -> c -> Int
+f2 _ _ _ = 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 #-}
+{-# SPECIALISE f2 :: Eq c => c -> c -> Word -> Int #-}
--------------------------------------------------------------------------------
@@ -69,15 +78,30 @@ f5 x = x == x
{-# SPECIALISE f5 :: D Int -> Bool #-}
-f6 :: ( Eq a, Eq ( T a ), forall x. ( Eq x, Eq ( T x ) ) => Eq ( f x ) ) => f a -> Bool
-f6 z = z == z
+f5_qc :: ( Eq a, Eq ( T a ), forall x. ( Eq x, Eq ( T x ) ) => Eq ( f x ) ) => f a -> Bool
+f5_qc z = z == z
-- Discharge a quantified constraint using a top-level instance
-- whose context includes a type family application.
-{-# SPECIALISE f6 :: D Int -> Bool #-}
+{-# SPECIALISE f5_qc :: D Int -> Bool #-}
-- Quantify over this same quantified constraint, but discharge the
-- other dictionary constraints.
-{-# SPECIALISE f6 :: ( forall y. ( Eq y, Eq ( T y ) ) => Eq ( g y ) ) => g Int -> Bool #-}
+{-# SPECIALISE f5_qc :: ( forall y. ( Eq y, Eq ( T y ) ) => Eq ( g y ) ) => g Int -> Bool #-}
+
+--------------------------------------------------------------------------------
+
+f6 :: ( Eq a, Ord b, Num c ) => a -> b -> c -> Char
+f6 _ _ _ = 'c'
+
+-- Check that we do perform simplification among Wanteds that we quantify over.
+{-# SPECIALISE f6 :: Ord c => c -> c -> Word -> Char #-}
+
+
+f6_qc :: ( forall x. Eq x => Eq ( f x ), forall y. Eq y => Ord ( g y ), Num c ) => Proxy f -> Proxy g -> c -> Char
+f6_qc _ _ _ = 'd'
+
+-- Like 'f6', but with quantified constraints.
+{-# SPECIALISE f6_qc :: ( forall z. Eq z => Ord ( h z ) ) => Proxy h -> Proxy h -> Word -> Char #-}
--------------------------------------------------------------------------------
=====================================
testsuite/tests/typecheck/should_compile/SpecPragmas.hs → testsuite/tests/typecheck/should_compile/TcSpecPragmas.hs
=====================================
@@ -1,8 +1,17 @@
-{-# LANGUAGE NamedWildCards, PartialTypeSignatures #-}
+{-# LANGUAGE GADTs, NamedWildCards, PartialTypeSignatures #-}
module SpecPragmas where
+import Data.Proxy
+ ( Proxy(..) )
+import Data.Type.Equality
+ ( (:~~:)(HRefl) )
+import Data.Typeable
+ ( Typeable, heqT )
+
+--------------------------------------------------------------------------------
+
foo :: Num a => a -> a
foo x = x + 1
@@ -32,3 +41,16 @@ baz a b = realToFrac a + fromIntegral b
{-# SPECIALISE [~1] forall a. forall. baz @a @_ @a #-}
+--------------------------------------------------------------------------------
+
+tyEq :: ( Typeable a, Typeable b ) => Proxy a -> Proxy b -> Float
+tyEq ( _ :: Proxy a ) ( _ :: Proxy b ) =
+ case heqT @a @b of
+ Nothing -> 17.9
+ Just HRefl -> 1.1
+
+-- Check that we don't emit a "useless specialisation" warning, as the
+-- specialisation allows us to drop dead code in the body of 'f7'.
+{-# SPECIALISE tyEq :: Typeable c => Proxy c -> Proxy c -> Float #-}
+
+--------------------------------------------------------------------------------
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -738,7 +738,7 @@ test('ExplicitSpecificityA1', normal, compile, [''])
test('ExplicitSpecificityA2', normal, compile, [''])
test('ExplicitSpecificity4', normal, compile, [''])
test('RuleEqs', normal, compile, [''])
-test('SpecPragmas', normal, compile, [''])
+test('TcSpecPragmas', 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/-/compare/4c9dc29cd3b4c8612ea03f36ea35ba7d9579fba3...2d65f88fb38d577e9001053501ad5881f407134c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4c9dc29cd3b4c8612ea03f36ea35ba7d9579fba3...2d65f88fb38d577e9001053501ad5881f407134c
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/20250204/d3b459c7/attachment-0001.html>
More information about the ghc-commits
mailing list