[Git][ghc/ghc][wip/T24359] Thinking about equalities and casts in SpecSigE
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Nov 7 17:33:29 UTC 2024
Simon Peyton Jones pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
f9cb037f by Simon Peyton Jones at 2024-11-07T17:32:54+00:00
Thinking about equalities and casts in SpecSigE
- - - - -
4 changed files:
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Types/Evidence.hs
- testsuite/tests/simplCore/should_compile/T5821.hs
Changes:
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -847,9 +847,10 @@ dsSpec mb_poly_rhs (SpecPragE { spe_poly_id = poly_id
; mk_spec_call <- do { ds_call <- dsLExpr the_call
; return $ \ poly_id poly_rhs ->
+ mkLets ds_lhs_binds $
+ mkLets ds_rhs_binds $
mkLetNonRec (localiseId poly_id) poly_rhs $
- mkLets ds_lhs_binds $
- mkLets ds_rhs_binds ds_call }
+ ds_call }
; finishSpecPrag mb_poly_rhs
(tv_bndrs ++ lhs_evs ++ id_bndrs) core_call
@@ -865,7 +866,7 @@ failBecauseOfClassOp poly_id
; return Nothing }
finishSpecPrag :: Maybe CoreExpr -- See the first param of dsSpec
- -> [Var] -- LHS binders
+ -> [Var] -- Binders, over LHS and RHS
-> CoreExpr -- LHS pattern
-> [Var] -> (Id -> CoreExpr -> CoreExpr) -- Make spec RHS given function body
-> InlinePragma
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -50,7 +50,7 @@ import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
import GHC.Tc.Utils.Env
import GHC.Tc.Types.Origin
-import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
+import GHC.Tc.Types.Evidence( HsWrapper, (<.>), hsWrapperHasNoBinders )
import GHC.Tc.Types.Constraint
import GHC.Tc.Zonk.TcType
@@ -717,29 +717,39 @@ See `GHC.Rename.Bind.checkSpecESigShape` for the shape-check.
Example:
f :: forall a b. (Eq a, Eq b, Ord 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::Ord p) (x::Int) (y::p).
f @Int @p @p d1 d2 d3 x y y True
= $sf @p d1 d2 d3 x y
- $sf @p (d1::Eq Int) (d2::Eq p) (d3::Ord p) (x::Int) (y::p)
- = let d1a = $fEqint
- d2a = d2
- d3a = d3
+ $sf @p (d1a::Eq Int) (d2a::Eq p) (d3a::Ord p) (x::Int) (y::p)
+ = let d1 = $fEqInt
+ d2 = d2a
+ d3 = d3a
in let f = <f-rhs>
- in f @p @p @Int (d1a::Eq p) (d2a::Eq p) (d3a::OrdInt) y y True
+ in f @p @p @Int (d1::Eq p) (d2::Eq p) (d3::Ord Int) x y y True
+
+In terms of the code:
+ spe_tv_bndrs = @p
+ spe_id_bndrs = x:Int y y:p
+ spe_lhs_ev_bndrs = (e1:Eq p) (d2:Eq p) (d3:Ord Int)
+ spe_lhs_call = f @p @p @Int (d1::Eq p) (d2::Eq p) (d3::Ord Int) x y y True
+ -- We can't meddle with this; it's a perhaps-big expression
+ spe_rhs_ev_bndrs = @d1a @d2a @d3a
+ spe_rhs_binds = { d1=$fEqInt; d2=d2a; d3=d3a }
Note that
-* In the RULE we have separate binders for `d1` and `d2` 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.
+* In the RULE we have separate binders for `d1` and `d2` 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.
-* The specialised function $sf takes all three dictionaries as
- arguments; but the constraint solver does not use d1 (short-cut
- solved). We rely on the Simplifier to drop the dead arguments.
- It isn't strictly necessary to pass d2 either, but it does no harm.
+* The specialised function $sf takes all three dictionaries as arguments; but
+ the constraint solver does not use d1 (short-cut solved). We rely on the
+ Simplifier to drop the dead arguments. It isn't strictly necessary to pass d2
+ either, but it does no harm.
Note [Handling old-form SPECIALISE pragmas]
@@ -895,8 +905,10 @@ tcSpecPrag poly_id (SpecSigE nm bndrs spec_e inl)
do { (tv_bndrs, id_bndrs) <- tcRuleBndrs skol_info bndrs
; tcExtendNameTyVarEnv [(tyVarName tv, tv) | tv <- tv_bndrs] $
tcExtendIdEnv id_bndrs $
- do { (spec_e', rho) <- tcInferRho spec_e
- ; return (id_bndrs, spec_e', rho) } }
+ do { (L loc spec_e', rho) <- tcInferRho spec_e
+ ; return (id_bndrs, L loc (unwrap_hs_expr spec_e'), rho) } }
+ -- unwrap_hs_expr: if the expression looks like (e |> co), simply drop `co`
+ -- ToDo: document this
-- Solve unification constraints
-- c.f. Note [The SimplifyRule Plan] step 1
@@ -922,15 +934,18 @@ tcSpecPrag poly_id (SpecSigE nm bndrs spec_e inl)
qtkvs lhs_evs residual_wanted
-- rhs_binds uses rhs_evs to build `wanted` (NB not just `residual_wanted`)
- ; let quant_wanted = emptyWC { wc_simple = quant_cts }
; rhs_evs <- mapM newEvVar quant_preds
; (implic2, rhs_binds) <- buildImplicationFor tc_lvl skol_info_anon
- qtkvs rhs_evs quant_wanted
+ qtkvs rhs_evs
+ (emptyWC { wc_simple = quant_cts })
; emitImplications (implic1 `unionBags` implic2)
; traceTc "tcSpecPrag:SpecSigE" $
- vcat [ text "tv/id bndrs:" <+> ppr qtkvs <+> ppr id_bndrs
+ vcat [ text "nm:" <+> ppr nm
+ , text "bndrs:" <+> ppr bndrs
+ , text "spec_e:" <+> ppr spec_e
+ , text "tv/id bndrs:" <+> ppr qtkvs <+> ppr id_bndrs
, text "lhs_evs:" <+> ppr lhs_evs
, text "rhs_evs:" <+> ppr rhs_evs
, text "spec_e:" <+> ppr spec_e'
@@ -944,6 +959,18 @@ tcSpecPrag poly_id (SpecSigE nm bndrs spec_e inl)
, spe_rhs_ev_bndrs = rhs_evs
, spe_rhs_binds = rhs_binds
, spe_inl = inl }] }
+ where
+ unwrap_hs_expr e
+{-
+ | ExprWithTySig _ (L _ inner_e) _ <- e
+ = unwrap_hs_expr inner_e
+ | XExpr (WrapExpr wrap inner_e) <- e
+ , hsWrapperHasNoBinders wrap
+ = unwrap_hs_expr inner_e
+ | otherwise
+-}
+ = e
+
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
@@ -1457,7 +1484,7 @@ mk_quant_evs cts
mk_one ct = pprPanic "mk_quant_ev" (ppr ct)
getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
--- Extract all the constraints we can quantify over,
+-- Extract all the constraints that we can quantify over,
-- also returning the depleted WantedConstraints
--
-- NB: we must look inside implications, because with
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -11,7 +11,7 @@ module GHC.Tc.Types.Evidence (
mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
collectHsWrapBinders,
idHsWrapper, isIdHsWrapper,
- pprHsWrapper, hsWrapDictBinders,
+ pprHsWrapper, hsWrapDictBinders, hsWrapperHasNoBinders,
-- * Evidence bindings
TcEvBinds(..), EvBindsVar(..),
@@ -331,6 +331,19 @@ collectHsWrapBinders wrap = go wrap []
add_lam v (vs,w) = (v:vs, w)
+hsWrapperHasNoBinders :: HsWrapper -> Bool
+hsWrapperHasNoBinders wrap = go wrap
+ where
+ go WpHole = True
+ go (w1 `WpCompose` w2) = go w1 && go w2
+ go (WpEvLam {}) = False
+ go (WpTyLam {}) = False
+ go (WpFun _ w _) = go w
+ go (WpCast {}) = True
+ go (WpEvApp {}) = True
+ go (WpTyApp {}) = True
+ go (WpLet {}) = False
+
{-
************************************************************************
* *
=====================================
testsuite/tests/simplCore/should_compile/T5821.hs
=====================================
@@ -9,3 +9,6 @@ foo :: Num a => a -> T a
foo = undefined
{-# SPECIALISE foo :: Int -> Bool #-}
+{- # SPECIALISE (foo :: Int -> Bool) # -}
+{- # SPECIALISE forall x. foo (x::Int) :: Bool # -}
+{- # SPECIALISE forall x. (foo :: Int -> Bool) x # -}
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f9cb037f22c98ad27681d5d0503ab60f0d5a8832
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f9cb037f22c98ad27681d5d0503ab60f0d5a8832
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/20241107/3c5e6a88/attachment-0001.html>
More information about the ghc-commits
mailing list