Simon Peyton Jones pushed to branch wip/spj-try-opt-coercion at Glasgow Haskell Compiler / GHC
Commits:
-
e180c6dc
by Simon Peyton Jones at 2026-01-14T09:07:38+00:00
4 changed files:
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Utils/Misc.hs
Changes:
| ... | ... | @@ -257,12 +257,17 @@ optCoAlt is (Alt k bs e) |
| 257 | 257 | left-to-right, and won't spot (co1 ; co2 ; sym co2)
|
| 258 | 258 | -}
|
| 259 | 259 | |
| 260 | -optCoRefl :: Coercion -> Coercion
|
|
| 260 | +optCoRefl :: Subst -> Coercion -> Coercion
|
|
| 261 | 261 | -- See Note [optCoRefl]
|
| 262 | -optCoRefl in_co
|
|
| 263 | -#ifdef DEBUG
|
|
| 262 | +optCoRefl subst in_co
|
|
| 263 | + | isEmptyTCvSubst subst = in_co
|
|
| 264 | + |
|
| 265 | + | otherwise
|
|
| 266 | +#ifndef DEBUG
|
|
| 267 | + = opt_co_refl subst in_co
|
|
| 268 | +#else
|
|
| 264 | 269 | -- Debug check that optCoRefl doesn't change the type
|
| 265 | - = let out_co = go in_co
|
|
| 270 | + = let out_co = opt_co_refl subst in_co
|
|
| 266 | 271 | (Pair in_l in_r) = coercionKind in_co
|
| 267 | 272 | (Pair out_l out_r) = coercionKind out_co
|
| 268 | 273 | in if (in_l `eqType` out_l) && (in_r `eqType` out_r)
|
| ... | ... | @@ -274,9 +279,11 @@ optCoRefl in_co |
| 274 | 279 | , text "in_co:" <+> ppr in_co
|
| 275 | 280 | , text "out_co:" <+> ppr out_co ]) $
|
| 276 | 281 | out_co
|
| 277 | -#else
|
|
| 278 | - = go in_co
|
|
| 279 | 282 | #endif
|
| 283 | + |
|
| 284 | + |
|
| 285 | +opt_co_refl :: Subst -> Coercion -> Coercion
|
|
| 286 | +opt_co_refl subst co = go co
|
|
| 280 | 287 | where
|
| 281 | 288 | go_m MRefl = MRefl
|
| 282 | 289 | go_m (MCo co) = MCo (go co)
|
| ... | ... | @@ -294,12 +301,17 @@ optCoRefl in_co |
| 294 | 301 | go (LRCo n co) = mkLRCo n (go co)
|
| 295 | 302 | go (AppCo co1 co2) = mkAppCo (go co1) (go co2)
|
| 296 | 303 | go (InstCo co1 co2) = mkInstCo (go co1) (go co2)
|
| 297 | - go (ForAllCo v vl vr mco co) = mkForAllCo v vl vr (go_m mco) (go co)
|
|
| 298 | 304 | go (FunCo r afl afr com coa cor) = mkFunCo2 r afl afr (go com) (go coa) (go cor)
|
| 299 | 305 | go (TyConAppCo r tc cos) = mkTyConAppCo r tc (go_s cos)
|
| 300 | 306 | go (UnivCo p r lt rt cos) = mkUnivCo p (go_s cos) r lt rt
|
| 301 | 307 | go (AxiomCo ax cos) = mkAxiomCo ax (go_s cos)
|
| 302 | 308 | |
| 309 | + go (ForAllCo v vl vr mco co) = mkForAllCo v' vl vr
|
|
| 310 | + $!! go_m mco
|
|
| 311 | + $!! opt_co_refl subst' co
|
|
| 312 | + where
|
|
| 313 | + !(subst', v') = substVarBndr subst v
|
|
| 314 | + |
|
| 303 | 315 | -- This is the main payload
|
| 304 | 316 | go (TransCo co1 co2) = gobble gs0 co1 [co2]
|
| 305 | 317 | where
|
| ... | ... | @@ -1390,7 +1390,7 @@ simplCoercionF env co cont |
| 1390 | 1390 | |
| 1391 | 1391 | simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
|
| 1392 | 1392 | simplCoercion env co
|
| 1393 | - = do { let out_co = optCoRefl (substCo env co)
|
|
| 1393 | + = do { let out_co = optCoRefl (getTCvSubst env) co
|
|
| 1394 | 1394 | ; seqCo out_co `seq` return out_co }
|
| 1395 | 1395 | |
| 1396 | 1396 | -----------------------------------
|
| ... | ... | @@ -860,33 +860,33 @@ subst_co subst co |
| 860 | 860 | go_mco (MCo co) = MCo (go co)
|
| 861 | 861 | |
| 862 | 862 | go :: Coercion -> Coercion
|
| 863 | - go (Refl ty) = mkNomReflCo $! (go_ty ty)
|
|
| 864 | - go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
|
|
| 865 | - go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args
|
|
| 866 | - go (AxiomCo con cos) = mkAxiomCo con $! go_cos cos
|
|
| 867 | - go (AppCo co arg) = (mkAppCo $! go co) $! go arg
|
|
| 863 | + go (Refl ty) = mkNomReflCo $!! go_ty ty
|
|
| 864 | + go (GRefl r ty mco) = mkGReflCo r $!! go_ty ty $!! go_mco mco
|
|
| 865 | + go (TyConAppCo r tc args)= mkTyConAppCo r tc $!! go_cos args
|
|
| 866 | + go (AxiomCo con cos) = mkAxiomCo con $!! go_cos cos
|
|
| 867 | + go (AppCo co arg) = mkAppCo $!! go co $!! go arg
|
|
| 868 | 868 | go (ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
|
| 869 | 869 | , fco_kind = kind_co, fco_body = co })
|
| 870 | - = ((mkForAllCo $! tcv') visL visR
|
|
| 871 | - $! go_mco kind_co)
|
|
| 872 | - $! subst_co subst' co
|
|
| 870 | + = (mkForAllCo $!! tcv') visL visR
|
|
| 871 | + $!! go_mco kind_co
|
|
| 872 | + $!! subst_co subst' co
|
|
| 873 | 873 | where
|
| 874 | 874 | !(subst', tcv') = substVarBndrUnchecked subst tcv
|
| 875 | 875 | -- Unchecked because used from substTyUnchecked
|
| 876 | - go (FunCo r afl afr w co1 co2) = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2
|
|
| 876 | + go (FunCo r afl afr w co1 co2) = mkFunCo2 r afl afr $!! go w $!! go co1 $!! go co2
|
|
| 877 | 877 | go (CoVarCo cv) = substCoVar subst cv
|
| 878 | 878 | go (UnivCo { uco_prov = p, uco_role = r
|
| 879 | 879 | , uco_lty = t1, uco_rty = t2, uco_deps = deps })
|
| 880 | - = ((((mkUnivCo $! p) $! go_cos deps) $! r) $!
|
|
| 881 | - (go_ty t1)) $! (go_ty t2)
|
|
| 882 | - go (SymCo co) = mkSymCo $! (go co)
|
|
| 883 | - go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
|
|
| 884 | - go (SelCo d co) = mkSelCo d $! (go co)
|
|
| 885 | - go (LRCo lr co) = mkLRCo lr $! (go co)
|
|
| 886 | - go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
|
|
| 887 | - go (KindCo co) = mkKindCo $! (go co)
|
|
| 888 | - go (SubCo co) = mkSubCo $! (go co)
|
|
| 889 | - go (HoleCo h) = HoleCo $! go_hole h
|
|
| 880 | + = mkUnivCo p $!! go_cos deps $!! r
|
|
| 881 | + $!! go_ty t1 $!! go_ty t2
|
|
| 882 | + go (SymCo co) = mkSymCo $!! go co
|
|
| 883 | + go (TransCo co1 co2) = mkTransCo $!! go co1 $!! go co2
|
|
| 884 | + go (SelCo d co) = mkSelCo d $!! go co
|
|
| 885 | + go (LRCo lr co) = mkLRCo lr $!! go co
|
|
| 886 | + go (InstCo co arg) = mkInstCo $!! go co $!! go arg
|
|
| 887 | + go (KindCo co) = mkKindCo $!! go co
|
|
| 888 | + go (SubCo co) = mkSubCo $!! go co
|
|
| 889 | + go (HoleCo h) = HoleCo $!! go_hole h
|
|
| 890 | 890 | |
| 891 | 891 | go_cos cos = let cos' = map go cos
|
| 892 | 892 | in cos' `seqList` cos'
|
| ... | ... | @@ -8,7 +8,7 @@ |
| 8 | 8 | --
|
| 9 | 9 | module GHC.Utils.Misc (
|
| 10 | 10 | -- * Miscellaneous higher-order functions
|
| 11 | - applyWhen, nTimes, const2,
|
|
| 11 | + applyWhen, nTimes, const2, ($!!),
|
|
| 12 | 12 | |
| 13 | 13 | -- * General list processing
|
| 14 | 14 | zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
|
| ... | ... | @@ -44,8 +44,7 @@ module GHC.Utils.Misc ( |
| 44 | 44 | mergeListsBy,
|
| 45 | 45 | isSortedBy,
|
| 46 | 46 | |
| 47 | - -- Foldable generalised functions,
|
|
| 48 | - |
|
| 47 | + -- * Foldable generalised functions,
|
|
| 49 | 48 | mapMaybe',
|
| 50 | 49 | |
| 51 | 50 | -- * Tuples
|
| ... | ... | @@ -153,6 +152,8 @@ import qualified Data.Set as Set |
| 153 | 152 | |
| 154 | 153 | import Data.Time
|
| 155 | 154 | |
| 155 | +infixl 0 $!! -- LEFT associative
|
|
| 156 | + |
|
| 156 | 157 | {-
|
| 157 | 158 | ************************************************************************
|
| 158 | 159 | * *
|
| ... | ... | @@ -199,6 +200,14 @@ third3 f (a, b, c) = (a, b, f c) |
| 199 | 200 | uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
|
| 200 | 201 | uncurry3 f (a, b, c) = f a b c
|
| 201 | 202 | |
| 203 | +($!!) :: forall r a (b :: TYPE r). (a -> b) -> a -> b
|
|
| 204 | +-- | ^ ($!!) is left-associative so you can write
|
|
| 205 | +-- (f $!! e1 $!! e2) for a multi-argument strict application
|
|
| 206 | +-- In contrast ($) and ($!) are right associative
|
|
| 207 | +{-# INLINE ($!!) #-}
|
|
| 208 | +f $!! x = let !vx = x in f vx -- see #2273
|
|
| 209 | + |
|
| 210 | + |
|
| 202 | 211 | {-
|
| 203 | 212 | ************************************************************************
|
| 204 | 213 | * *
|