Simon Peyton Jones pushed to branch wip/T26989 at Glasgow Haskell Compiler / GHC Commits: 9ec89815 by Simon Peyton Jones at 2026-04-28T11:48:38+01:00 Do not use mkCast during typechecking This commit fixes #27219. The problem was that the typechecker was using `mkCast`, whose assertion checks legitimately fail when applied to types that contain unification variables. - - - - - bd1503ad by Simon Peyton Jones at 2026-04-28T11:50:14+01:00 More improvements * pushCoValArg and pushCoTyArg return tyL, which is helpful for the caller * Don't optimise coercions if the type-substitution is empty. See Note [Optimising coercions] - - - - - 4 changed files: - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -2875,43 +2875,44 @@ pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion) -- 'co' is always Representational pushCoArg co arg | Type ty <- arg - = do { (ty', m_co') <- pushCoTyArg co ty + = do { (_, ty', m_co') <- pushCoTyArg co ty ; return (Type ty', m_co') } | otherwise - = do { (arg_mco, m_co') <- pushCoValArg co + = do { (_, arg_mco, m_co') <- pushCoValArg co ; let arg_mco' = checkReflexiveMCo arg_mco -- checkReflexiveMCo: see Note [Check for reflexive casts in eta expansion] -- The coercion is very often (arg_co -> res_co), but without -- the argument coercion actually being ReflCo ; return (arg `mkCastMCo` arg_mco', m_co') } -pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR) +pushCoTyArg :: CoercionR -> Type -> Maybe (Type, Type, MCoercionR) -- We have (fun |> co) @ty -- Push the coercion through to return -- (fun @ty') |> co' -- 'co' is always Representational -- If the returned coercion is Nothing, then it would have been reflexive; -- it's faster not to compute it, though. -pushCoTyArg co ty +pushCoTyArg co arg_ty -- The following is inefficient - don't do `eqType` here, the coercion -- optimizer will take care of it. See #14737. -- -- | tyL `eqType` tyR -- -- = Just (ty, Nothing) - | isReflCo co - = Just (ty, MRefl) + | Just (ty, _) <- isReflCo_maybe co + = Just (ty, arg_ty, MRefl) | isForAllTy_ty tyL - = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr ty) $ - Just (ty `mkCastTy` co1, MCo co2) + = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr arg_ty) $ + Just (tyL, arg_ty `mkCastTy` co1, MCo co2) | otherwise = Nothing where - Pair tyL tyR = coercionKind co - -- co :: tyL ~R tyR - -- tyL = forall (a1 :: k1). ty1 - -- tyR = forall (a2 :: k2). ty2 + -- co :: tyL ~R tyR + -- tyL = forall (a1 :: k1). ty1 + -- tyR = forall (a2 :: k2). ty2 + tyL = coercionLKind co + tyR = coercionRKind co -- Used only in asssertions and debug messages co1 = mkSymCo (mkSelCo SelForAll co) -- co1 :: k2 ~N k1 @@ -2919,30 +2920,32 @@ pushCoTyArg co ty -- kinds of the types related by a coercion between forall-types. -- See the SelCo case in GHC.Core.Lint. - co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1) - -- co2 :: ty1[ (ty|>co1)/a1 ] ~R ty2[ ty/a2 ] + co2 = mkInstCo co (mkGReflLeftCo Nominal arg_ty co1) + -- co2 :: ty1[ (arg_ty|>co1)/a1 ] ~R ty2[ arg_ty/a2 ] -- Arg of mkInstCo is always nominal, hence Nominal --- | If @pushCoValArg co = Just (co_arg, co_res)@, then +-- | If @pushCoValArg co = Just (tyL, co_arg, co_res)@, then -- --- > (\x.body) |> co = (\y. let { x = y |> co_arg } in body) |> co_res) +-- co :: tyL ~R# tyR +-- and +-- (\x.body) |> co = (\y. let { x = y |> co_arg } in body) |> co_res) -- -- or, equivalently -- --- > (fun |> co) arg = (fun (arg |> co_arg)) |> co_res +-- (fun |> co) arg = (fun (arg |> co_arg)) |> co_res -- -- If the LHS is well-typed, then so is the RHS. In particular, the argument -- @arg |> co_arg@ is guaranteed to have a fixed 'RuntimeRep', in the sense of -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -pushCoValArg :: CoercionR -> Maybe (MCoercionR, MCoercionR) +pushCoValArg :: CoercionR -> Maybe (Type, MCoercionR, MCoercionR) pushCoValArg co -- The following is inefficient - don't do `eqType` here, the coercion -- optimizer will take care of it. See #14737. -- -- | tyL `eqType` tyR -- -- = Just (mkRepReflCo arg, Nothing) - | isReflCo co - = Just (MRefl, MRefl) + | Just (ty, _) <- isReflCo_maybe co + = Just (ty, MRefl, MRefl) | isFunTy tyL , (_, co1, co2) <- decomposeFunCo co @@ -2961,7 +2964,7 @@ pushCoValArg co (vcat [ text "co:" <+> ppr co , text "old_arg_ty:" <+> ppr old_arg_ty , text "new_arg_ty:" <+> ppr new_arg_ty ]) $ - Just (coToMCo (mkSymCo co1), coToMCo co2) + Just (tyL, coToMCo (mkSymCo co1), coToMCo co2) -- Critically, coToMCo to checks for ReflCo; the whole coercion may not -- be reflexive, but either of its components might be -- We could use isReflexiveCo, but it's not clear if the benefit @@ -2970,9 +2973,12 @@ pushCoValArg co | otherwise = Nothing where - old_arg_ty = funArgTy tyR + tyL = coercionLKind co new_arg_ty = funArgTy tyL - Pair tyL tyR = coercionKind co + + -- These two are used only in assertions and debug messages + tyR = coercionRKind co + old_arg_ty = funArgTy tyR pushCoercionIntoLambda :: HasDebugCallStack => InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr) ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -17,8 +17,7 @@ import GHC.Driver.Flags import GHC.Core import GHC.Core.Opt.Simplify.Monad import GHC.Core.Opt.ConstantFold -import GHC.Core.Type hiding ( substCo, substTy, substTyVar, extendTvSubst, extendCvSubst ) -import GHC.Core.TyCo.Compare( eqType ) +import GHC.Core.Opt.Stats ( Tick(..) ) import GHC.Core.Opt.Simplify.Env import GHC.Core.Opt.Simplify.Inline import GHC.Core.Opt.Simplify.Utils @@ -26,11 +25,14 @@ import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr, zapLambdaBndrs ) import GHC.Core.Make ( FloatBind, mkImpossibleExpr, castBottomExpr ) import qualified GHC.Core.Make import GHC.Core.Coercion hiding ( substCo, substCoVar ) +import qualified GHC.Core.Coercion as Coercion import GHC.Core.Reduction import GHC.Core.Coercion.Opt ( optCoercion ) +import GHC.Core.Type hiding ( substCo, substTy, substTyVar, extendTvSubst, extendCvSubst ) +import GHC.Core.TyCo.Compare( eqType ) +import GHC.Core.TyCo.Subst( isEmptyTvSubst ) import GHC.Core.FamInstEnv ( FamInstEnv, topNormaliseType_maybe ) import GHC.Core.DataCon -import GHC.Core.Opt.Stats ( Tick(..) ) import GHC.Core.Ppr ( pprCoreExpr ) import GHC.Core.Unfold import GHC.Core.Unfold.Make @@ -1399,16 +1401,38 @@ simplCoercionF env co cont simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion simplCoercion env co - = do { let opt_co | reSimplifying env = substCo env co - | otherwise = optCoercion opts subst co - -- If (reSimplifying env) is True we have already simplified - -- this coercion once, and we don't want do so again; doing - -- so repeatedly risks non-linear behaviour - -- See Note [Inline depth] in GHC.Core.Opt.Simplify.Env - ; seqCo opt_co `seq` return opt_co } + = seqCo opt_co `seq` return opt_co where + -- See Note [Optimising coercions] + -- NB: substCo has a short-cut when both type and coercion substs are empty + opt_co | subst_only = Coercion.substCo subst co + | otherwise = optCoercion opts subst co + subst = getTCvSubst env opts = seOptCoercionOpts env + subst_only = isEmptyTvSubst subst || reSimplifying env + +{- Note [Optimising coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Some programs have very big coercions and we'd like to avoid repeatedly +re-optimising them: + +* If the type-substitution is empty (common when no further transformations + are taking place) then there is generally no point in re-optimising. + If there is a type substitution, however, Refls may appear. + Example where this isEmptyTCvSubst test really helped: aT5030. + + Actually, if this is a "freshly-made" coercion (one built in the previous + iteration of the Simplifier, or a previous pass) then perhaps optimisations + /could/ occur; but we check for reflexivity in `rebuild_go`, and that's the + big win. Otherwise having a bigger-than necessary coercion is no so bad. + +* (reSimplifying env) is True we are in the body of an inlined function + so we (conservatively) and we don't want do so again; doing so repeatedly + risks non-linear behaviour. See Note [Inline depth] in GHC.Core.Opt.Simplify.Env. + + But if the inlining did a type substitution maybe we should re-optimise? +-} ----------------------------------- -- | Push a TickIt context outwards past applications and cases, as @@ -1742,6 +1766,9 @@ pushCast :: SimplEnv -> OutCoercion -> SimplCont -> SimplM SimplCont pushCast env co cont = go co True cont where + + -- ToDo: pushCast Refl (ApplylToVal arg1 (ApplyToVal arg2 ...)) + -- will do lots of unnecessary work. go :: OutCoercion -> Bool -> SimplCont -> SimplM SimplCont go co1 _ (CastIt { sc_co = co2, sc_cont = cont }) -- See Note [Optimising reflexivity] = go (mkTransCo co1 co2) False cont @@ -1749,12 +1776,12 @@ pushCast env co cont -- See Note [Avoid re-simplifying coercions] go co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail }) - | Just (arg_ty', m_co') <- pushCoTyArg co arg_ty + | Just (tyL, arg_ty', m_co') <- pushCoTyArg co arg_ty = {-#SCC "addCoerce-pushCoTyArg" #-} do { tail' <- go_mco m_co' co_is_opt tail ; return (ApplyToTy { sc_arg_ty = arg_ty' , sc_cont = tail' - , sc_hole_ty = coercionLKind co }) } + , sc_hole_ty = tyL }) } -- NB! As the cast goes past, the -- type of the hole changes (#16312) @@ -1768,16 +1795,14 @@ pushCast env co cont = -- pushCoValArg duplicates the coercion, so optimise first go (optOutCoercion (zapSubstEnv env) co co_is_opt) True cont --- ToDo: return coercionLKind. And similarly pushCoTyArg - - | Just (m_co1, m_co2) <- pushCoValArg co + | Just (tyL, m_co1, m_co2) <- pushCoValArg co = {-#SCC "addCoerce-pushCoValArg" #-} - do { tail' <- go_mco m_co2 co_is_opt tail + do { tail' <- go_mco m_co2 True tail ; return (ApplyToVal { sc_arg = arg , sc_env = arg_se , sc_cast = arg_mco `mkTransMCo` m_co1 , sc_cont = tail' - , sc_hole_ty = coercionLKind co }) } + , sc_hole_ty = tyL }) } go co co_is_opt cont | isReflCo co = return cont -- Having this at the end makes a huge @@ -1785,8 +1810,6 @@ pushCast env co cont -- See Note [Optimising reflexivity] | otherwise = return (CastIt { sc_co = co, sc_opt = co_is_opt, sc_cont = cont }) --- ToDo: pushCast Refl (ApplylToVal arg1 (ApplyToVal arg2 ...)) will do lots of unnecessary work. - -- If the first parameter is MRefl, then simplifying revealed a -- reflexive coercion. Omit. go_mco :: MOutCoercion -> Bool -> SimplCont -> SimplM SimplCont ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -12,7 +12,7 @@ module GHC.Core.TyCo.Subst -- * Substitutions Subst(..), TvSubstEnv, CvSubstEnv, IdSubstEnv, emptyIdSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubst, - emptySubst, mkEmptySubst, isEmptyTCvSubst, isEmptySubst, + emptySubst, mkEmptySubst, isEmptyTvSubst, isEmptyTCvSubst, isEmptySubst, mkSubst, mkTCvSubst, mkTvSubst, mkCvSubst, mkIdSubst, getTvSubstEnv, getIdSubstEnv, getCvSubstEnv, substInScopeSet, setInScope, getSubstRangeTyCoFVs, @@ -262,6 +262,11 @@ isEmptySubst :: Subst -> Bool isEmptySubst (Subst _ id_env tv_env cv_env) = isEmptyVarEnv id_env && isEmptyVarEnv tv_env && isEmptyVarEnv cv_env +-- | Checks if the type substitution (only) is empty +isEmptyTvSubst :: Subst -> Bool +isEmptyTvSubst (Subst _ _ tv_env _) + = isEmptyVarEnv tv_env + -- | Checks whether the tyvar and covar environments are empty. -- This function should be used over 'isEmptySubst' when substituting -- for types, because types currently do not contain expressions; we can ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -59,7 +59,6 @@ import GHC.Tc.Utils.TcType import GHC.Core import GHC.Core.Coercion.Axiom import GHC.Core.Coercion -import GHC.Core.Utils( mkCast ) import GHC.Core.Ppr () -- Instance OutputableBndr TyVar import GHC.Core.Predicate import GHC.Core.Type @@ -932,7 +931,8 @@ evCastE ee co | assertPpr (coercionRole co == Representational) (vcat [text "Coercion of wrong role passed to evCastE:", ppr ee, ppr co]) $ isReflCo co = ee - | otherwise = mkCast ee co + | otherwise = Cast ee co -- Do not call mkCast because its assertion + -- checks fail on un-zonked terms (#27219) evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm -- Dictionary instance application, including when the "dictionary function" View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9bbd56e8ba16b562d10b5b94d92dbc0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9bbd56e8ba16b562d10b5b94d92dbc0... You're receiving this email because of your account on gitlab.haskell.org.