Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 722236dd by sheaf at 2026-07-18T08:48:31-04:00 Coercion optimisation: avoid double-Sym for InstCo Ticket #27374 pointed out an issue with GHC.Core.Coercion.Opt.optCoercion's handling of InstCo: it contravened (LC2) in Note [The LiftingContext in optCoercion] because it applied the ambient 'sym' to a coercion that was then added to the lifting context substitution. Fixes #27374 Co-authored-by: Simon Jakobi <simon.jakobi@gmail.com> - - - - - ff70fc75 by sheaf at 2026-07-18T08:48:31-04:00 Coercion optimisation: avoid exponential behaviour The change to coercion optimisation of 'InstCo' in the previous commit introduces exponential behaviour to the coercion optimiser. To avoid this, this commit provides a way to push in 'Sym' of an already-optimised coercion: GHC.Core.Coercion.Opt.mkDeepSymCo. See Note [Pushing Sym without re-optimising] in GHC.Core.Coercion.Opt. - - - - - 4 changed files: - + changelog.d/T27374 - compiler/GHC/Core/Coercion/Opt.hs - + testsuite/tests/corelint/T27374.hs - testsuite/tests/corelint/all.T Changes: ===================================== changelog.d/T27374 ===================================== @@ -0,0 +1,9 @@ +section: compiler +issues: #27374 +mrs: !16207 +synopsis: + Fix optimisation of InstCo coercions +description: + Fixes a bug in which the coercion optimiser would incorrectly optimise certain + InstCo coercions, incorrectly changing their kinds. + ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -274,10 +274,11 @@ opt_co4, opt_co4' :: LiftingContext -> SwapFlag -> ReprFlag -- Precondition: In every call (opt_co4 lc sym rep role co) -- we should have role = coercionRole co -- Precondition: role is not Phantom --- Postcondition: The resulting coercion is equivalant to --- wrapsub (wrapsym (mksub co) --- where wrapsym is SymCo if sym=True --- wrapsub is SubCo if rep=True +-- Postcondition: The resulting coercion is equivalent to +-- wrapSub (wrapSym (substCo co)) +-- where substCo applies the LiftingContext substitution +-- wrapSym wraps in SymCo when the ambient Sym is IsSwapped +-- wrapSub wraps in SubCo when rep=True -- opt_co4 is there just to support tracing, when debugging -- Usually it just goes straight to opt_co4' @@ -327,7 +328,10 @@ opt_co4' env sym rep r (GRefl _r ty (MCo kco)) text "Type:" <+> ppr ty) $ if isReflKindCo kco || isReflKindCo kco' then wrapSym sym ty_co - else wrapSym sym $ mk_coherence_right_co r' (coercionRKind ty_co) kco' ty_co + else + -- Keep 'sym' on the outside instead of trying to push it in, to avoid + -- duplicating 'k_co' in 'GRefl r (ty |> kco) (MCo (sym kco))' + wrapSym sym $ mk_coherence_right_co r' (coercionRKind ty_co) kco' ty_co -- ty :: k1 -- kco :: k1 ~ k2 -- Desired result coercion: ty ~ ty |> co @@ -534,25 +538,36 @@ opt_co4' env sym rep r (InstCo fun_co arg_co) , let s2' = coercionRKind arg_co' tv_co = mk_coherence_right_co Nominal s2' (mkSymCo k_co') arg_co' env' = extendLiftingContext (zapLiftingContext env) tv' tv_co - = opt_co4 env' NotSwapped False r' body_co' + = opt_co4 env' sym False r' body_co' -- See Note [Forall over coercion] | Just (cv', _visL, _visR, _kind_co', body_co') <- splitForAllCo_co_maybe fun_co' , CoercionTy h1' <- coercionLKind arg_co' , let env' = extendLiftingContextCvSubst (zapLiftingContext env) cv' h1' - = opt_co4 env' NotSwapped False r' body_co' + = opt_co4 env' sym False r' body_co' -- Those cases didn't work either, so rebuild the InstCo - -- Push Sym into /both/ function /and/ arg_coument - | otherwise = InstCo fun_co' arg_co' + | otherwise = InstCo sym_fun_co' sym_arg_co' where - -- fun_co' arg_co' are both optimised, /and/ we have pushed `sym` into both - -- So no more sym'ing on th results of fun_co' arg_co' - fun_co' = opt_co4 env sym rep r fun_co - arg_co' = opt_co4 env sym False Nominal arg_co r' = chooseRole rep r + -- Optimised versions of fun_co & arg_co. + -- NB: we do /not/ push in `sym` (hence using `NotSwappped`), + -- in order to respect (LC2) in Note [The LiftingContext in optCoercion]. + fun_co' = opt_co4 env NotSwapped rep r fun_co + arg_co' = opt_co4 env NotSwapped False Nominal arg_co + + -- Like fun_co'/arg_co', except we /have/ pushed in `sym`. + -- We use 'mkDeepSymCo' to push in 'sym' without re-optimising. + -- See Note [Pushing Sym without re-optimising] + sym_fun_co' + | isSwapped sym = mkDeepSymCo fun_co' + | otherwise = fun_co' + sym_arg_co' + | isSwapped sym = mkDeepSymCo arg_co' + | otherwise = arg_co' + opt_co4' env sym _rep r (KindCo co) = assert (r == Nominal) $ let kco' = promoteCoercion co in @@ -575,6 +590,83 @@ We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo] in GHC.Core.Coercion. -} +{- Note [Pushing Sym without re-optimising] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +To optimise (InstCo fun_co arg_co) we must first optimise fun_co and arg_co +/without/ the ambient Sym, as required by (LC2) of +Note [The LiftingContext in optCoercion]. + +But in the fallback case (when the optimised fun_co is not a ForAllCo), we need +to push the ambient Sym into both components when rebuilding the InstCo. + + Re-running the optimiser with sym=IsSwapped would optimise each component twice. + As the components can themselves contain 'InstCo's, this has the potential to + trigger exponential behaviour. + + Simply wrapping 'sym' on the outside would fail to push 'sym' deeply into the + coercion, which would be in tension with the rest of the coercion optimiser + which relies on 'sym' being pushed into the leaves to expose cancellation + opportunities. + +To solve this, we define 'mkDeepSymCo': it pushes a Sym into an already +optimised coercion. This is much simpler than full coercion optimisation, as it +doesn't need to do coercion lifting nor downgrade roles. +-} + +-- | Push 'Sym' deeply into an already-optimised coercion. +-- +-- Morally the same as re-optimising the coercion with @sym=IsSwapped@, but +-- more efficient. +-- +-- See Note [Pushing Sym without re-optimising] +mkDeepSymCo :: NormalCo -> NormalCo +mkDeepSymCo = go + where + go :: NormalCo -> NormalCo + -- Straightforward cases + go (SymCo co) = co + go co@(UnivCo { uco_lty = t1, uco_rty = t2 }) = co { uco_lty = t2, uco_rty = t1 } + go (TyConAppCo r tc cos) = TyConAppCo r tc $ map go cos + go (AppCo co1 co2) = AppCo (go co1) (go co2) + go (FunCo r afl afr cow co1 co2) = FunCo r afr afl (go cow) (go co1) (go co2) + go (TransCo co1 co2) = TransCo (go co2) (go co1) + go (SelCo cs co) = SelCo cs $ go co + go (LRCo lr co) = LRCo lr $ go co + go (InstCo fun_co arg_co) = InstCo (go fun_co) (go arg_co) + go (KindCo co) = KindCo $ go co + go (SubCo co) = SubCo $ go co + go co@(CoVarCo {}) = SymCo co + go co@(Refl {}) = co + go co@(GRefl _ _ MRefl) = co + go co@(GRefl _ _ (MCo {})) = SymCo co + -- keep the sym outside, like the GRefl case of opt_co4' does, instead of + -- GRefl r (ty |> kco) (MCo (sym kco)) + -- as that duplicates 'kco' + go co@(AxiomCo {}) = SymCo co + -- Same as in opt_co4': do *not* push sym inside top-level axioms. + + go co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR + , fco_kind = k_mco, fco_body = body_co }) + = case k_mco of + MRefl -> ForAllCo tcv visR visL k_mco (go body_co) + MCo {} -> + -- Pushing 'sym' into the kind coercion would require threading a + -- substitution through, as per Note [Optimising ForAllCo]. + -- This wouldn't be difficult (see commented out code below), but + -- for now we prefer to keep 'mkDeepSymCo' as simple as possible. + SymCo co + + -- Pushing 'sym' into the kind coercion, threading 'Subst' through: + -- + -- = ForAllCo tcv' visR visL k_mco' (go subst' body_co) + -- where + -- k_mco' = case k_mco of + -- MRefl -> MRefl + -- MCo co -> MCo (go subst co) + -- (subst', tcv') = forAllCoBndrSubst IsSwapped tcv k_mco' subst + + go (HoleCo h) = pprPanic "mkDeepSymCo: HoleCo" (ppr h) + ------------- -- | Optimize a phantom coercion. The input coercion may not necessarily -- be a phantom, but the output sure will be. @@ -1450,6 +1542,9 @@ But if sym=Swapped, things are trickier. Here is an identity that helps: of tv:k1 in bodyco by (tv:k2 |> Sym kco) This mirrors what happens in the typing rule for ForAllCo See Note [ForAllCo] in GHC.Core.TyCo.Rep + NB: doing so inlines 'kco' at all occurrences of tv, duplicating it. This is + inconsistent with how we optimise GRefl, where we keep the 'Sym' on the + outside to avoid duplicating the kind coercion. -} optForAllCoBndr :: LiftingContext -> SwapFlag @@ -1464,13 +1559,20 @@ optForAllCoBndr env sym tcv k_mco MRefl -> MRefl MCo co -> MCo (opt_co4 env sym False Nominal co) - (env', tcv') = updateLCSubst env upd_subst - - upd_subst :: Subst -> (Subst, TyCoVar) - upd_subst subst - | isTyVar tcv = upd_subst_tv subst - | otherwise = upd_subst_cv subst - + (env', tcv') = updateLCSubst env (forAllCoBndrSubst sym tcv k_mco') + +-- | Substitute a 'ForAllCo' binder, returning the body substitution. +-- +-- See Note [Optimising ForAllCo]. +forAllCoBndrSubst + :: SwapFlag + -> TyCoVar -- ^ the ForAllCo binder + -> MCoercionN -- ^ its kind coercion, with the ambient Sym already pushed into it + -> Subst -> (Subst, TyCoVar) +forAllCoBndrSubst sym tcv k_mco' + | isTyVar tcv = upd_subst_tv + | otherwise = upd_subst_cv + where upd_subst_tv subst = case k_mco' of MCo k_co' | isSwapped sym -> (subst2, tv2) ===================================== testsuite/tests/corelint/T27374.hs ===================================== @@ -0,0 +1,201 @@ +{-# LANGUAGE BlockArguments #-} + +-- | Regression test for #27374: +-- +-- - manually construct some coercions that are not InstCo but become InstCo +-- after optimisation +-- - check that the coercion optimiser properly optimises these by running +-- Core Lint on the output + +module Main (main) where + +-- base +import Control.Monad.IO.Class + ( liftIO ) +import Data.Foldable + ( for_ ) +import System.Environment + ( getArgs ) + +-- ghc +import GHC + ( runGhc, getSessionDynFlags, getLogger ) +import GHC.Builtin.Types + ( maybeTyCon, tupleTyCon, mkBoxedTupleTy ) +import GHC.Core + ( Expr(Coercion) ) +import GHC.Core.Coercion + ( Coercion, CoVar, MCoercion(..) + , Role(..), CoSel(..), FunSel(..) + , mkCoercionType + , mkCoVar, mkCoVarCo, mkForAllCo, mkInstCo, mkReflCo, mkNomReflCo + , mkSelCo, mkSymCo, mkTransCo, mkTyConAppCo + , tyCoVarsOfCo + ) +import GHC.Core.Coercion.Opt + ( OptCoercionOpts(..), optCoercion ) +import GHC.Core.Lint + ( lintExpr ) +import GHC.Core.Predicate + ( mkNomEqPred ) +import GHC.Core.TyCo.FVs + ( tyCoVarsOfCoList ) +import GHC.Core.TyCo.Rep + ( Type(CoercionTy) ) +import GHC.Core.Type + +import GHC.Data.FastString + ( fsLit ) + +import GHC.Driver.Config.Core.Lint + ( initLintConfig ) + +import GHC.Types.Basic + ( Boxity(Boxed) ) +import GHC.Types.Var + ( mkTyVar, coreTyLamForAllTyFlag ) +import GHC.Types.Var.Env + ( mkInScopeSet ) +import GHC.Types.Name + ( mkInternalName ) +import GHC.Types.Name.Occurrence + ( mkTyVarOccFS, mkVarOccFS ) +import GHC.Types.SrcLoc + ( noSrcSpan ) +import GHC.Types.Unique + ( mkUniqueGrimily ) + +import GHC.Utils.Error + ( pprMessageBag, putMsg ) +import GHC.Utils.Outputable + ( (<+>), text, vcat ) + +-------------------------------------------------------------------------------- +-- Helpers for building fresh variables +-------------------------------------------------------------------------------- + +mkTv :: Int -> String -> Kind -> TyVar +mkTv i s = + mkTyVar $ + mkInternalName + ( mkUniqueGrimily (fromIntegral i) ) + ( mkTyVarOccFS (fsLit s) ) + noSrcSpan + +mkCv :: Int -> String -> Type -> CoVar +mkCv i s = + mkCoVar $ + mkInternalName + ( mkUniqueGrimily (fromIntegral i) ) + ( mkVarOccFS (fsLit s) ) + noSrcSpan + +-------------------------------------------------------------------------------- +-- ForAllCo-over-type +-------------------------------------------------------------------------------- + +co1 :: Coercion +co1 = + -- Use mkTransCo to get a coercion that is not InstCo but optimises to InstCo + lhs `mkTransCo` rhs + where + p = mkTv 21 "p" liftedTypeKind + q = mkTv 22 "q" liftedTypeKind + a = mkTv 23 "a" liftedTypeKind + b = mkTv 24 "b" liftedTypeKind + + tup2 = tupleTyCon Boxed 2 + + -- cv :: p ~# q + cv = mkCoVarCo $ + mkCv 25 "cv" $ + mkCoercionType Nominal (mkTyVarTy p) (mkTyVarTy q) + + -- arg :: Maybe q ~ Maybe p + arg = mkSymCo (mkTyConAppCo Nominal maybeTyCon [cv]) + + -- forallCo = <forall a b. (a, b) -> a>_N + forallCo = + mkReflCo Nominal $ + mkSpecForAllTys [a, b] $ + mkVisFunTyMany + (mkBoxedTupleTy [mkTyVarTy a, mkTyVarTy b]) + (mkTyVarTy a) + + -- forallCo @arg @arg + inst_co = mkInstCo (mkInstCo forallCo arg) arg + + rhs = mkSymCo (mkSelCo (SelFun SelArg) inst_co) + lhs = mkTyConAppCo Nominal tup2 [arg, arg] + +-------------------------------------------------------------------------------- +-- ForAllCo-over-coercion +-------------------------------------------------------------------------------- + +co2 :: Coercion +co2 = + -- This outer 'sym' was necessary to trigger the specific bug + mkSymCo $ + mkInstCo ( mkSymCo g ) arg + where + k1 = mkTyVarTy $ mkTv 11 "k1" liftedTypeKind + k2 = mkTyVarTy $ mkTv 12 "k2" liftedTypeKind + + x = mkTv 13 "x" k1 + + -- cv :: k1 ~# Type + cv_ty = mkNomEqPred k1 liftedTypeKind + cv = mkCv 14 "cv" cv_ty + + -- hk :: (k1 ~# Type) ~# (k2 ~# Type) + hk = mkCoVarCo (mkCv 15 "hk" (mkNomEqPred cv_ty (mkNomEqPred k2 liftedTypeKind))) + + -- body :: (x |> cv) ~# (x |> cv) + body = mkNomReflCo (mkCastTy (mkTyVarTy x) (mkCoVarCo cv)) + + -- g :: (forall (cv :: k1 ~# Type). x |> cv) + -- ~# (forall (cv' :: k2 ~# Type). x |> (sel 2 hk ; cv' ; sym (sel 3 hk))) + g = mkForAllCo cv vis vis (MCo hk) body + vis = coreTyLamForAllTyFlag + + -- two distinct coercions to instantiate at + coL = mkCoVarCo (mkCv 16 "coL" (mkNomEqPred k1 liftedTypeKind)) + coR = mkCoVarCo (mkCv 17 "coR" (mkNomEqPred k2 liftedTypeKind)) + arg = mkCoVarCo (mkCv 18 "arg" (mkNomEqPred (CoercionTy coL) (CoercionTy coR))) + +-------------------------------------------------------------------------------- +-- Test runner +-------------------------------------------------------------------------------- + +test_cos :: [ ( String, Coercion ) ] +test_cos = + [ ( "InstCo (TyVar)", co1 ) + , ( "InstCo (CoVar)", co2 ) + ] + +opt_co :: Coercion -> Coercion +opt_co co = + let in_scope = mkInScopeSet $ tyCoVarsOfCo co + in + optCoercion + ( OptCoercionOpts { optCoercionEnabled = True } ) + ( mkEmptySubst in_scope ) + co + +main :: IO () +main = do + [libdir] <- getArgs + runGhc ( Just libdir ) do + dflags <- getSessionDynFlags + logger <- getLogger + liftIO $ for_ test_cos \ ( name, co ) -> do + -- Optimise each test coercion and run the result through Core Lint. + let + co' = opt_co co + in_scope = tyCoVarsOfCoList co' + lint_cfg = initLintConfig dflags in_scope + for_ ( lintExpr lint_cfg ( Coercion co' ) ) \ errs -> + putMsg logger $ + vcat [ text "Core Lint error for" <+> text name + , pprMessageBag errs + ] ===================================== testsuite/tests/corelint/all.T ===================================== @@ -9,5 +9,6 @@ setTestOpts(extra_hc_opts('-package ghc')) setTestOpts(extra_run_opts('"' + config.libdir + '"')) test('LintEtaExpand', normal, compile_and_run, ['']) +test('T27374', normal, compile_and_run, ['']) ## These tests use the GHC API. ## Test cases which don't use the GHC API should be added nearer the top. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fe3b059c714be22dac658a620a2b5a0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fe3b059c714be22dac658a620a2b5a0... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help