Simon Peyton Jones pushed to branch wip/spj-try-opt-coercion at Glasgow Haskell Compiler / GHC
Commits:
-
52c7e75f
by Simon Peyton Jones at 2026-01-20T17:47:22+00:00
5 changed files:
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/SimpleOpt.hs
- compiler/GHC/Driver/Config.hs
- compiler/GHC/Driver/Config/Core/Lint.hs
Changes:
| ... | ... | @@ -300,8 +300,13 @@ optCoRefl check_stuff subst in_co |
| 300 | 300 | out_co
|
| 301 | 301 | |
| 302 | 302 | opt_co_refl :: Subst -> InCoercion -> OutCoercion
|
| 303 | -opt_co_refl subst co = go co
|
|
| 303 | +opt_co_refl subst co
|
|
| 304 | + | lk `eqTypeIgnoringMultiplicity` rk = mkReflCo (coercionRole co) lk
|
|
| 305 | + | otherwise = out_co
|
|
| 304 | 306 | where
|
| 307 | + out_co = go co
|
|
| 308 | + Pair lk rk = coercionKind out_co
|
|
| 309 | + |
|
| 305 | 310 | go_m MRefl = MRefl
|
| 306 | 311 | go_m (MCo co) = MCo (go co)
|
| 307 | 312 | |
| ... | ... | @@ -339,14 +344,25 @@ opt_co_refl subst co = go co |
| 339 | 344 | where
|
| 340 | 345 | !(subst', v') = substVarBndr subst v
|
| 341 | 346 | |
| 342 | - -- This is the main payload
|
|
| 343 | - go (TransCo co1 co2) = gobble gs0 co1 [co2]
|
|
| 347 | + -- The TransCo case fires up the main loop for
|
|
| 348 | + -- eliminating reflexive chains of TransCo
|
|
| 349 | + go (TransCo co1 co2)
|
|
| 350 | + | lk' `eqTypeIgnoringMultiplicity` rk' = go co2
|
|
| 351 | + | otherwise = gobble0 gs1 [co2]
|
|
| 344 | 352 | where
|
| 345 | - lk' = substTy subst (coercionLKind co1)
|
|
| 353 | + co1' = go co1
|
|
| 354 | + Pair lk' rk' = coercionKind co1
|
|
| 346 | 355 | role = coercionRole co1
|
| 347 | 356 | |
| 348 | - gs0 :: GobbleState
|
|
| 349 | - gs0 = GS (mkReflCo role lk') (insertTM lk' gs0 emptyTM)
|
|
| 357 | + gs0, gs1 :: GobbleState
|
|
| 358 | + gs0 = GS (mkReflCo role lk') tm0
|
|
| 359 | + gs1 = GS co1' (insertTM rk' gs1 tm0)
|
|
| 360 | + |
|
| 361 | + tm0 = insertTM lk' gs0 emptyTM
|
|
| 362 | + |
|
| 363 | + gobble0 :: GobbleState -> [InCoercion] -> OutCoercion
|
|
| 364 | + gobble0 (GS co _) [] = co
|
|
| 365 | + gobble0 gs (co:cos) = gobble gs co cos
|
|
| 350 | 366 | |
| 351 | 367 | gobble :: GobbleState -> InCoercion -> [InCoercion] -> OutCoercion
|
| 352 | 368 | -- gobble (GS co1 tm) co2 cos returns a coercion equivalent to (co1;co2;cos)
|
| ... | ... | @@ -361,8 +377,6 @@ opt_co_refl subst co = go co |
| 361 | 377 | rk' = coercionRKind co2'
|
| 362 | 378 | gs' = GS (co1' `mkTransCo` co2') (insertTM rk' gs' tm)
|
| 363 | 379 | |
| 364 | - gobble0 (GS co _) [] = co
|
|
| 365 | - gobble0 gs (co:cos) = gobble gs co cos
|
|
| 366 | 380 | |
| 367 | 381 | data GobbleState = GS OutCoercion (TypeMap GobbleState)
|
| 368 | 382 | -- The map is keyed by OutType
|
| ... | ... | @@ -26,6 +26,7 @@ import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr, zapLambdaBndrs, scrutOkForBind |
| 26 | 26 | import GHC.Core.Make ( FloatBind, mkImpossibleExpr, castBottomExpr )
|
| 27 | 27 | import qualified GHC.Core.Make
|
| 28 | 28 | import GHC.Core.Coercion hiding ( substCo, substCoVar )
|
| 29 | +import qualified GHC.Core.Coercion as Coercion
|
|
| 29 | 30 | import GHC.Core.Coercion.Opt
|
| 30 | 31 | import GHC.Core.Reduction
|
| 31 | 32 | import GHC.Core.FamInstEnv ( FamInstEnv, topNormaliseType_maybe )
|
| ... | ... | @@ -1391,19 +1392,20 @@ simplCoercionF env co cont |
| 1391 | 1392 | simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
|
| 1392 | 1393 | simplCoercion env co
|
| 1393 | 1394 | = do { let out_co | sm_opt_refl_co mode
|
| 1394 | - , not (isEmptyTCvSubst subst) || initial_phase
|
|
| 1395 | - = optCoRefl (sm_check_opt_co mode) subst co
|
|
| 1396 | - | otherwise
|
|
| 1397 | - = substCo env co
|
|
| 1398 | - subst = getTCvSubst env
|
|
| 1399 | - initial_phase = case sePhase env of
|
|
| 1400 | - SimplPhase InitialPhase -> True
|
|
| 1401 | - _ -> False
|
|
| 1395 | + = if isEmptyTCvSubst subst
|
|
| 1396 | + then co
|
|
| 1397 | + else optCoRefl chk_opts subst co
|
|
| 1398 | + | otherwise -- substCo also has a shortcut
|
|
| 1399 | + -- when substitution is empty
|
|
| 1400 | + = Coercion.substCo subst co
|
|
| 1402 | 1401 | |
| 1403 | 1402 | ; seqCo out_co `seq`
|
| 1404 | 1403 | return out_co }
|
| 1405 | 1404 | where
|
| 1406 | - mode = seMode env
|
|
| 1405 | + mode = seMode env
|
|
| 1406 | + chk_opts = sm_check_opt_co mode
|
|
| 1407 | + subst = getTCvSubst env
|
|
| 1408 | + |
|
| 1407 | 1409 | |
| 1408 | 1410 | -----------------------------------
|
| 1409 | 1411 | -- | Push a TickIt context outwards past applications and cases, as
|
| ... | ... | @@ -34,6 +34,7 @@ import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSub |
| 34 | 34 | , isInScope, substTyVarBndr, cloneTyVarBndr )
|
| 35 | 35 | import GHC.Core.Predicate( isCoVarType )
|
| 36 | 36 | import GHC.Core.Coercion hiding ( substCo, substCoVarBndr )
|
| 37 | +import GHC.Core.Coercion.Opt( optCoRefl )
|
|
| 37 | 38 | |
| 38 | 39 | import GHC.Types.Literal
|
| 39 | 40 | import GHC.Types.Id
|
| ... | ... | @@ -115,14 +116,18 @@ data SimpleOpts = SimpleOpts |
| 115 | 116 | , so_eta_red :: !Bool -- ^ Eta reduction on?
|
| 116 | 117 | , so_inline :: !Bool -- ^ False <=> do no inlining whatsoever,
|
| 117 | 118 | -- even for trivial or used-once things
|
| 119 | + , so_opt_co :: !Bool -- ^ Run the simple `optCoRefl` optimiser on coercions
|
|
| 120 | + , so_check_opt_co :: !Bool -- ^ Do debug-checking for `optCoRefl`
|
|
| 118 | 121 | }
|
| 119 | 122 | |
| 120 | 123 | -- | Default options for the Simple optimiser.
|
| 121 | 124 | defaultSimpleOpts :: SimpleOpts
|
| 122 | 125 | defaultSimpleOpts = SimpleOpts
|
| 123 | - { so_uf_opts = defaultUnfoldingOpts
|
|
| 124 | - , so_eta_red = False
|
|
| 125 | - , so_inline = True
|
|
| 126 | + { so_uf_opts = defaultUnfoldingOpts
|
|
| 127 | + , so_eta_red = False
|
|
| 128 | + , so_inline = True
|
|
| 129 | + , so_opt_co = True
|
|
| 130 | + , so_check_opt_co = False
|
|
| 126 | 131 | }
|
| 127 | 132 | |
| 128 | 133 | simpleOptExpr :: HasDebugCallStack => SimpleOpts -> CoreExpr -> CoreExpr
|
| ... | ... | @@ -327,19 +332,15 @@ simple_opt_expr env expr = go expr |
| 327 | 332 | (env', bndrs') = subst_opt_bndrs env bndrs
|
| 328 | 333 | |
| 329 | 334 | simple_opt_co :: SimpleOptEnv -> InCoercion -> OutCoercion
|
| 330 | -simple_opt_co env co = substCo (soe_subst env) co
|
|
| 331 | - |
|
| 332 | -mk_cast :: CoreExpr -> CoercionR -> CoreExpr
|
|
| 333 | --- Like GHC.Core.Utils.mkCast, but does a full reflexivity check.
|
|
| 334 | --- mkCast doesn't do that because the Simplifier does (in simplCast)
|
|
| 335 | --- But in SimpleOpt it's nice to kill those nested casts (#18112)
|
|
| 336 | -mk_cast (Cast e co1) co2 = mk_cast e (co1 `mkTransCo` co2)
|
|
| 337 | -mk_cast (Tick t e) co = Tick t (mk_cast e co)
|
|
| 338 | -mk_cast e co
|
|
| 339 | - | isReflexiveCo co
|
|
| 340 | - = e
|
|
| 341 | - | otherwise
|
|
| 342 | - = Cast e co
|
|
| 335 | +-- Optimise a coercion, optionally running
|
|
| 336 | +-- the simple `optCoRefl` optimiser
|
|
| 337 | +-- If (so_opt_co opts) is on, we run the optimiser even if the substition
|
|
| 338 | +-- is empty, to kill off Refls; but if not, `substCo` does a no-op if
|
|
| 339 | +-- the substitution is empty
|
|
| 340 | +simple_opt_co (SOE { soe_subst = subst, soe_opts = opts }) co
|
|
| 341 | + | so_opt_co opts = optCoRefl (so_check_opt_co opts) subst co
|
|
| 342 | + | otherwise = substCo subst co
|
|
| 343 | + |
|
| 343 | 344 | |
| 344 | 345 | ----------------------
|
| 345 | 346 | -- simple_app collects arguments for beta reduction
|
| ... | ... | @@ -406,8 +407,8 @@ simple_app env e0@(Lam {}) as0@(_:_) |
| 406 | 407 | | otherwise
|
| 407 | 408 | = rebuild_app env (simple_opt_expr env e) as
|
| 408 | 409 | |
| 409 | - do_beta env (Cast e co) as =
|
|
| 410 | - do_beta env e (add_cast env co as)
|
|
| 410 | + do_beta env (Cast e co) as
|
|
| 411 | + = do_beta env e (add_cast env co as)
|
|
| 411 | 412 | |
| 412 | 413 | do_beta env body as
|
| 413 | 414 | = simple_app env body as
|
| ... | ... | @@ -478,7 +479,7 @@ rebuild_app env fun args = foldl mk_app fun args |
| 478 | 479 | in_scope = soeInScope env
|
| 479 | 480 | mk_app out_fun = \case
|
| 480 | 481 | ApplyToArg arg -> App out_fun (simple_opt_clo in_scope arg)
|
| 481 | - CastIt co -> mk_cast out_fun co
|
|
| 482 | + CastIt co -> mkCast out_fun co
|
|
| 482 | 483 | |
| 483 | 484 | {- Note [Desugaring unlifted newtypes]
|
| 484 | 485 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| ... | ... | @@ -18,6 +18,8 @@ initSimpleOpts dflags = SimpleOpts |
| 18 | 18 | { so_uf_opts = unfoldingOpts dflags
|
| 19 | 19 | , so_eta_red = gopt Opt_DoEtaReduction dflags
|
| 20 | 20 | , so_inline = True
|
| 21 | + , so_opt_co = gopt Opt_OptReflCoercion dflags
|
|
| 22 | + , so_check_opt_co = dopt Opt_D_opt_co dflags
|
|
| 21 | 23 | }
|
| 22 | 24 | |
| 23 | 25 | -- | Instruct the interpreter evaluation to break...
|
| ... | ... | @@ -153,7 +153,7 @@ perPassFlags dflags pass |
| 153 | 153 | -- `-dlinear-core-lint`: check linearity in every pass
|
| 154 | 154 | || -- Always check linearity just after desugaring
|
| 155 | 155 | case pass of
|
| 156 | - CoreDesugar -> True
|
|
| 156 | + CoreDesugar -> True -- Before even the simple optimiser
|
|
| 157 | 157 | _ -> False
|
| 158 | 158 | |
| 159 | 159 | -- See Note [Checking for rubbish literals] in GHC.Core.Lint
|