Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: fb9cc882 by Simon Peyton Jones at 2025-08-30T05:10:51-04:00 Fix a long standing bug in the coercion optimiser We were mis-optimising ForAllCo, leading to #26345 Part of the poblem was the tricky tower of abstractions leading to the dreadful GHC.Core.TyCo.Subst.substForAllCoTyVarBndrUsing This function was serving two masters: regular substitution, but also coercion optimsation. So tricky was it that it did so wrong. In this MR I locate all the fancy footwork for coercion optimisation in GHC.Core.Coercion.Opt, where it belongs. That leaves substitution free to be much simpler. - - - - - 6 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/Type.hs - + testsuite/tests/typecheck/should_compile/T26345.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -93,9 +93,10 @@ module GHC.Core.Coercion ( liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx, emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope, liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst, + updateLCSubst, mkSubstLiftingContext, liftingContextSubst, zapLiftingContext, - substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet, + lcLookupCoVar, lcInScopeSet, LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight, substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight, @@ -2136,15 +2137,11 @@ extendLiftingContextEx lc@(LC subst env) ((v,ty):rest) zapLiftingContext :: LiftingContext -> LiftingContext zapLiftingContext (LC subst _) = LC (zapSubst subst) emptyVarEnv --- | Like 'substForAllCoBndr', but works on a lifting context -substForAllCoBndrUsingLC :: SwapFlag - -> (Coercion -> Coercion) - -> LiftingContext -> TyCoVar -> Coercion - -> (LiftingContext, TyCoVar, Coercion) -substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co - = (LC subst' lc_env, tv', co') +updateLCSubst :: LiftingContext -> (Subst -> (Subst, a)) -> (LiftingContext, a) +-- Lift a Subst-update function over LiftingContext +updateLCSubst (LC subst lc_env) upd = (LC subst' lc_env, res) where - (subst', tv', co') = substForAllCoBndrUsing sym sco subst tv co + (subst', res) = upd subst -- | The \"lifting\" operation which substitutes coercions for type -- variables in a type to produce a coercion. ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -358,12 +358,12 @@ opt_co4' env sym rep r (AppCo co1 co2) (opt_co4 env sym False Nominal co2) opt_co4' env sym rep r (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR - , fco_kind = k_co, fco_body = co }) - = case optForAllCoBndr env sym tv k_co of - (env', tv', k_co') -> mkForAllCo tv' visL' visR' k_co' $ - opt_co4 env' sym rep r co + , fco_kind = k_co, fco_body = co }) + = mkForAllCo tv' visL' visR' k_co' $ + opt_co4 env' sym rep r co -- Use the "mk" functions to check for nested Refls where + !(env', tv', k_co') = optForAllCoBndr env sym tv k_co !(visL', visR') = swapSym sym (visL, visR) opt_co4' env sym rep r (FunCo _r afl afr cow co1 co2) @@ -1401,10 +1401,68 @@ and these two imply -} +{- Note [Optimising ForAllCo] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If sym=NotSwapped, optimising ForAllCo is relatively easy: + opt env (ForAllCo tcv kco bodyco) + = ForAllCo tcv' (opt env kco) (opt env' bodyco) + where + (env', tcv') = substBndr env tcv + +Just apply the substitution to the kind of the binder, deal with +shadowing etc, and recurse. Remember in (ForAllCo tcv kco bodyco) + varKind tcv = coercionLKind kco + +But if sym=Swapped, things are trickier. Here is an identity that helps: + Sym (ForAllCo (tv:k1) (kco:k1~k2) bodyco) + = ForAllCo (tv:k2) (Sym kco : k2~k1) + (Sym (bodyco[tv:->tv:k2 |> Sym kco])) + +* We re-type tv:k1 to become tv:k2. +* We push Sym into kco +* We push Sym into bodyco +* BUT we must /also/ remember to replace all occurrences of + 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 + +-} optForAllCoBndr :: LiftingContext -> SwapFlag - -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion) -optForAllCoBndr env sym - = substForAllCoBndrUsingLC sym (opt_co4 env sym False Nominal) env + -> TyCoVar -> Coercion + -> (LiftingContext, TyCoVar, Coercion) +-- See Note [Optimising ForAllCo] +optForAllCoBndr env sym tcv kco + = (env', tcv', kco') + where + kco' = opt_co4 env sym False Nominal kco -- Push sym into kco + (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 + + upd_subst_tv subst + | notSwapped sym || isReflCo kco' = (subst1, tv1) + | otherwise = (subst2, tv2) + where + -- subst1,tv1: apply the substitution to the binder and its kind + -- NB: varKind tv = coercionLKind kco + (subst1, tv1) = substTyVarBndr subst tcv + -- In the Swapped case, we re-kind the type variable, AND + -- override the substitution for the original variable to the + -- re-kinded one, suitably casted + tv2 = tv1 `setTyVarKind` coercionLKind kco' + subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` kco')) + `extendSubstInScope` tv2 + + upd_subst_cv subst -- ToDo: probably not right yet + | notSwapped sym || isReflCo kco' = (subst1, cv1) + | otherwise = (subst2, cv2) + where + (subst1, cv1) = substCoVarBndr subst tcv + cv2 = cv1 `setTyVarKind` coercionLKind kco' + subst2 = subst1 `extendSubstInScope` cv2 {- ********************************************************************** ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -60,7 +60,7 @@ import {-# SOURCE #-} GHC.Core.Coercion , mkAxiomCo, mkAppCo, mkGReflCo , mkInstCo, mkLRCo, mkTyConAppCo , mkCoercionType - , coercionKind, coercionLKind, coVarTypesRole ) + , coercionLKind, coVarTypesRole ) import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar ) import {-# SOURCE #-} GHC.Core.Ppr ( ) -- instance Outputable CoreExpr import {-# SOURCE #-} GHC.Core ( CoreExpr ) @@ -68,12 +68,10 @@ import {-# SOURCE #-} GHC.Core ( CoreExpr ) import GHC.Core.TyCo.Rep import GHC.Core.TyCo.FVs -import GHC.Types.Basic( SwapFlag(..), isSwapped, pickSwap, notSwapped ) import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Var.Env -import GHC.Data.Pair import GHC.Utils.Constants (debugIsOn) import GHC.Utils.Misc import GHC.Types.Unique.Supply @@ -922,7 +920,7 @@ substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $ substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, Coercion) substForAllCoBndr subst - = substForAllCoBndrUsing NotSwapped (substCo subst) subst + = substForAllCoBndrUsing (substCo subst) subst -- | Like 'substForAllCoBndr', but disables sanity checks. -- The problems that the sanity checks in substCo catch are described in @@ -932,33 +930,26 @@ substForAllCoBndr subst substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, Coercion) substForAllCoBndrUnchecked subst - = substForAllCoBndrUsing NotSwapped (substCoUnchecked subst) subst + = substForAllCoBndrUsing (substCoUnchecked subst) subst -- See Note [Sym and ForAllCo] -substForAllCoBndrUsing :: SwapFlag -- Apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co +substForAllCoBndrUsing :: (Coercion -> Coercion) -- transformation to kind co -> Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, KindCoercion) -substForAllCoBndrUsing sym sco subst old_var - | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var - | otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var +substForAllCoBndrUsing sco subst old_var + | isTyVar old_var = substForAllCoTyVarBndrUsing sco subst old_var + | otherwise = substForAllCoCoVarBndrUsing sco subst old_var -substForAllCoTyVarBndrUsing :: SwapFlag -- Apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co +substForAllCoTyVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co -> Subst -> TyVar -> KindCoercion -> (Subst, TyVar, KindCoercion) -substForAllCoTyVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) old_var old_kind_co +substForAllCoTyVarBndrUsing sco (Subst in_scope idenv tenv cenv) old_var old_kind_co = assert (isTyVar old_var ) ( Subst (in_scope `extendInScopeSet` new_var) idenv new_env cenv , new_var, new_kind_co ) where - new_env | no_change, notSwapped sym - = delVarEnv tenv old_var - | isSwapped sym - = extendVarEnv tenv old_var $ - TyVarTy new_var `CastTy` new_kind_co - | otherwise - = extendVarEnv tenv old_var (TyVarTy new_var) + new_env | no_change = delVarEnv tenv old_var + | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) no_kind_change = noFreeVarsOfCo old_kind_co no_change = no_kind_change && (new_var == old_var) @@ -974,20 +965,17 @@ substForAllCoTyVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) old_var old new_var = uniqAway in_scope (setTyVarKind old_var new_ki1) -substForAllCoCoVarBndrUsing :: SwapFlag -- Apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co +substForAllCoCoVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co -> Subst -> CoVar -> KindCoercion -> (Subst, CoVar, KindCoercion) -substForAllCoCoVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) +substForAllCoCoVarBndrUsing sco (Subst in_scope idenv tenv cenv) old_var old_kind_co = assert (isCoVar old_var ) ( Subst (in_scope `extendInScopeSet` new_var) idenv tenv new_cenv , new_var, new_kind_co ) where - new_cenv | no_change, notSwapped sym - = delVarEnv cenv old_var - | otherwise - = extendVarEnv cenv old_var (mkCoVarCo new_var) + new_cenv | no_change = delVarEnv cenv old_var + | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var) no_kind_change = noFreeVarsOfCo old_kind_co no_change = no_kind_change && (new_var == old_var) @@ -995,10 +983,8 @@ substForAllCoCoVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) new_kind_co | no_kind_change = old_kind_co | otherwise = sco old_kind_co - Pair h1 h2 = coercionKind new_kind_co - - new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type - new_var_type = pickSwap sym h1 h2 + new_ki1 = coercionLKind new_kind_co + new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_ki1 substCoVar :: Subst -> CoVar -> Coercion substCoVar (Subst _ _ _ cenv) cv ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -559,11 +559,7 @@ expandTypeSynonyms ty go_co _ (HoleCo h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h) - -- the "False" and "const" are to accommodate the type of - -- substForAllCoBndrUsing, which is general enough to - -- handle coercion optimization (which sometimes swaps the - -- order of a coercion) - go_cobndr subst = substForAllCoBndrUsing NotSwapped (go_co subst) subst + go_cobndr subst = substForAllCoBndrUsing (go_co subst) subst {- Notes on type synonyms ~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== testsuite/tests/typecheck/should_compile/T26345.hs ===================================== @@ -0,0 +1,57 @@ +{-# LANGUAGE GHC2021 #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeFamilies #-} +module Bug where + +import Data.Kind (Constraint, Type) + +type Sing :: k -> Type +type family Sing @k + +type Tuple0 :: Type +data Tuple0 = MkTuple0 + +type STuple0 :: Tuple0 -> Type +data STuple0 z where + SMkTuple0 :: STuple0 MkTuple0 +type instance Sing @Tuple0 = STuple0 + +type U1 :: Type +data U1 = MkU1 + +type SU1 :: U1 -> Type +data SU1 z where + SMkU1 :: SU1 MkU1 +type instance Sing @U1 = SU1 + +type Generic :: Type -> Constraint +class Generic a where + type Rep a :: Type + +type PGeneric :: Type -> Constraint +class PGeneric a where + type PFrom (x :: a) :: Rep a + +type SGeneric :: Type -> Constraint +class SGeneric a where + sFrom :: forall (x :: a). Sing x -> Sing (PFrom x) + +instance SGeneric Tuple0 where + sFrom SMkTuple0 = SMkU1 + +instance Generic Tuple0 where + type Rep Tuple0 = U1 + +instance PGeneric Tuple0 where + type PFrom MkTuple0 = MkU1 + +type SDecide :: Type -> Constraint +class SDecide a where + sDecide :: forall (x :: a) (y :: a). Sing x -> Sing y -> Bool + +instance SDecide U1 where + sDecide SMkU1 SMkU1 = True + +sDecideDefault :: Sing MkTuple0 -> Sing MkTuple0 -> Bool +sDecideDefault s1 s2 = sDecide (sFrom s1) (sFrom s2) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -948,3 +948,5 @@ test('T26256a', normal, compile, ['']) test('T25992a', normal, compile, ['']) test('T26346', normal, compile, ['']) test('T26358', expect_broken(26358), compile, ['']) +test('T26345', normal, compile, ['']) + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fb9cc8825f37b1d7f1bc19d5a5c1425c... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fb9cc8825f37b1d7f1bc19d5a5c1425c... You're receiving this email because of your account on gitlab.haskell.org.