GitLab

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

 +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

 +{-# 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.