Simon Peyton Jones pushed to branch wip/spj-try-opt-coercion at Glasgow Haskell Compiler / GHC Commits: f4eea9ba by Simon Peyton Jones at 2026-01-07T11:40:17+00:00 Fix expression-equality for (Coercion co) We were just saying "True" which is utterly wrong. See Note [Equality for coercions] in GHC.Core.Map.Type - - - - - 68e18fc9 by Simon Peyton Jones at 2026-01-07T11:41:27+00:00 Wibbles on coercion bindings - - - - - 9 changed files: - compiler/GHC/Core/Map/Expr.hs - compiler/GHC/Core/Map/Type.hs - compiler/GHC/Core/Opt/CSE.hs - compiler/GHC/Core/Opt/Simplify/Env.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Data/TrieMap.hs - compiler/GHC/Iface/Make.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Types/Id.hs Changes: ===================================== compiler/GHC/Core/Map/Expr.hs ===================================== @@ -26,6 +26,7 @@ import GHC.Prelude import GHC.Data.TrieMap import GHC.Core.Map.Type import GHC.Core +import GHC.Core.Coercion( coercionRKind ) import GHC.Core.Type import GHC.Types.Tickish import GHC.Types.Var @@ -150,13 +151,16 @@ instance Eq (DeBruijn CoreExpr) where eqDeBruijnExpr :: DeBruijn CoreExpr -> DeBruijn CoreExpr -> Bool eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where - go (Var v1) (Var v2) = eqDeBruijnVar (D env1 v1) (D env2 v2) - go (Lit lit1) (Lit lit2) = lit1 == lit2 - go (Type t1) (Type t2) = eqDeBruijnType (D env1 t1) (D env2 t2) - -- See Note [Alpha-equality for Coercion arguments] - go (Coercion {}) (Coercion {}) = True - go (Cast e1 co1) (Cast e2 co2) = D env1 co1 == D env2 co2 && go e1 e2 - go (App f1 a1) (App f2 a2) = go f1 f2 && go a1 a2 + go (Var v1) (Var v2) = eqDeBruijnVar (D env1 v1) (D env2 v2) + go (Lit lit1) (Lit lit2) = lit1 == lit2 + go (Type t1) (Type t2) = eqDeBruijnType (D env1 t1) (D env2 t2) + go (Coercion co1) (Coercion co2) = eqDeBruijnCoercion (D env1 co1) (D env2 co2) + go (Cast e1 co1) (Cast e2 co2) = go e1 e2 && eqDeBruijnType (D env1 (coercionRKind co1)) + (D env2 (coercionRKind co2)) + go (App f1 a1) (App f2 a2) + | isCoArg a1, isCoArg a2 = go f1 f2 + | otherwise = go f1 f2 && go a1 a2 + -- isCoArg: see Note [Coercions in expressions] go (Tick n1 e1) (Tick n2 e2) = eqDeBruijnTickish (D env1 n1) (D env2 n2) && go e1 e2 @@ -204,12 +208,17 @@ eqDeBruijnTickish (D env1 t1) (D env2 t2) = go t1 t2 where eqCoreExpr :: CoreExpr -> CoreExpr -> Bool eqCoreExpr e1 e2 = eqDeBruijnExpr (deBruijnize e1) (deBruijnize e2) -{- Note [Alpha-equality for Coercion arguments] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The 'Coercion' constructor only appears in argument positions, and so, if the -functions are equal, then the arguments must have equal types. Because the -comparison for coercions (correctly) checks only their types, checking for -alpha-equality of the coercions is redundant. +{- Note [Coercions in expressions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When a coercion appears in an expression, we mainly use `eqDeBruijnCoercion` +(see Note [Equality for coercions] in GHC.Core.Map.Type). But we can optimise + * Applications: f1 (CO: co1) = f2 (CO: co2) + If the two functions are equal their argument coercions must have equal + types, so no need to compare the coercions at all. + + * Casts: e1 |> co1 = e2 |> co2 + If e1 and e2 are equal, the coercionLKinds of the coercions are equal; + so we only need to compare the coercionRKinds -} {- Note [Alpha-equality for let-bindings] ===================================== compiler/GHC/Core/Map/Type.hs ===================================== @@ -20,6 +20,7 @@ module GHC.Core.Map.Type ( TypeMapG, CoercionMapG, DeBruijn(..), deBruijnize, eqDeBruijnType, eqDeBruijnVar, + eqDeBruijnCoercion, BndrMap, xtBndr, lkBndr, VarMap, xtVar, lkVar, lkDFreeVar, xtDFreeVar, @@ -78,9 +79,14 @@ import Control.Monad ( (>=>) ) ************************************************************************ -} --- We should really never care about the contents of a coercion. Instead, --- just look up the coercion's type. +{- Note [Equality for coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A coercion is a proof, and any one proof is as good as any other. +So to compare coercions we just compare their types. +-} + newtype CoercionMap a = CoercionMap (CoercionMapG a) + -- See [Equality for coercions] -- TODO(22292): derive instance Functor CoercionMap where @@ -98,6 +104,9 @@ instance TrieMap CoercionMap where type CoercionMapG = GenMap CoercionMapX newtype CoercionMapX a = CoercionMapX (TypeMapX a) +-- CoercionMapX key point: two coercions are considered equal if +-- their coercionTypes are the same; so we just defer to TypeMap + -- TODO(22292): derive instance Functor CoercionMapX where @@ -113,11 +122,6 @@ instance TrieMap CoercionMapX where filterTM f (CoercionMapX core_tm) = CoercionMapX (filterTM f core_tm) mapMaybeTM f (CoercionMapX core_tm) = CoercionMapX (mapMaybeTM f core_tm) -instance Eq (DeBruijn Coercion) where - D env1 co1 == D env2 co2 - = D env1 (coercionType co1) == - D env2 (coercionType co2) - lkC :: DeBruijn Coercion -> CoercionMapX a -> Maybe a lkC (D env co) (CoercionMapX core_tm) = lkT (D env $ coercionType co) core_tm @@ -126,6 +130,16 @@ xtC :: DeBruijn Coercion -> XT a -> CoercionMapX a -> CoercionMapX a xtC (D env co) f (CoercionMapX m) = CoercionMapX (xtT (D env $ coercionType co) f m) +-- This equality instance is needed for the equality test in leaf compression; +-- see GenMap and Note [Compressed TrieMap] in GHC.Data.TrieMap +instance Eq (DeBruijn Coercion) where + (==) = eqDeBruijnCoercion + +eqDeBruijnCoercion :: DeBruijn Coercion -> DeBruijn Coercion -> Bool +eqDeBruijnCoercion (D env1 co1) (D env2 co2) + = eqDeBruijnType (D env1 (coercionType co1)) (D env2 (coercionType co2)) + + {- ************************************************************************ * * @@ -139,9 +153,7 @@ xtC (D env co) f (CoercionMapX m) -- but it is strictly internal to this module. If you are including a 'TypeMap' -- inside another 'TrieMap', this is the type you want. Note that this -- lookup does not do a kind-check. Thus, all keys in this map must have --- the same kind. Also note that this map respects the distinction between --- @Type@ and @Constraint@, despite the fact that they are equivalent type --- synonyms in Core. +-- the same kind. type TypeMapG = GenMap TypeMapX -- | @TypeMapX a@ is the base map from @DeBruijn Type@ to @a@, but without the @@ -191,9 +203,6 @@ instance TrieMap TypeMapX where filterTM = filterT mapMaybeTM = mpT -instance Eq (DeBruijn Type) where - (==) = eqDeBruijnType - -- | An equality relation between two 'Type's (known below as @t1 :: k2@ -- and @t2 :: k2@) data TypeEquality = TNEQ -- ^ @t1 /= t2@ @@ -219,7 +228,7 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) = liftEquality :: Bool -> TypeEquality liftEquality False = TNEQ - liftEquality _ = TEQ + liftEquality True = TEQ hasCast :: TypeEquality -> TypeEquality hasCast TEQ = TEQX @@ -272,7 +281,7 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) = go (D (extendCME env tv) ty) (D (extendCME env' tv') ty') (CoercionTy {}, CoercionTy {}) -> TEQ - _ -> TNEQ + _ -> TNEQ -- These bangs make 'gos' strict in the CMEnv, which in turn -- keeps the CMEnv unboxed across the go/gos mutual recursion @@ -282,9 +291,6 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) = gos e1 e2 tys1 tys2 gos _ _ _ _ = TNEQ -instance Eq (DeBruijn Var) where - (==) = eqDeBruijnVar - eqDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Bool eqDeBruijnVar (D env1 v1) (D env2 v2) = case (lookupCME env1 v1, lookupCME env2 v2) of @@ -292,6 +298,14 @@ eqDeBruijnVar (D env1 v1) (D env2 v2) = (Nothing, Nothing) -> v1 == v2 _ -> False +-- This equality instance is needed for the equality test in leaf compression; +-- see GenMap and Note [Compressed TrieMap] in GHC.Data.TrieMap +instance Eq (DeBruijn Type) where + (==) = eqDeBruijnType + +instance Eq (DeBruijn Var) where + (==) = eqDeBruijnVar + instance {-# OVERLAPPING #-} Outputable a => Outputable (TypeMapG a) where ppr m = text "TypeMap elts" <+> ppr (foldTM (:) m []) @@ -488,6 +502,7 @@ instance TrieMap LooseTypeMap where filterTM f (LooseTypeMap m) = LooseTypeMap (filterTM f m) mapMaybeTM f (LooseTypeMap m) = LooseTypeMap (mapMaybeTM f m) + {- ************************************************************************ * * ===================================== compiler/GHC/Core/Opt/CSE.hs ===================================== @@ -450,7 +450,7 @@ cse_bind toplevel env_rhs env_body (in_id, in_rhs) out_id | otherwise = (env_body', (out_id'', out_rhs)) where - (env_body', out_id') = extendCSEnvWithBinding env_body in_id out_id out_rhs cse_done + (env_body', out_id') = extendCSEnvWithBinding env_body in_id out_id out_rhs cse_done (cse_done, out_rhs) = try_for_cse env_rhs in_rhs out_id'' | cse_done = zapStableUnfolding $ delayInlining toplevel out_id' ===================================== compiler/GHC/Core/Opt/Simplify/Env.hs ===================================== @@ -422,11 +422,12 @@ data SimplFloats } instance Outputable SimplFloats where - ppr (SimplFloats { sfLetFloats = lf, sfJoinFloats = jf, sfInScope = is }) + ppr (SimplFloats { sfLetFloats = lf, sfJoinFloats = jf, sfInScope = _is }) = text "SimplFloats" <+> braces (vcat [ text "lets: " <+> ppr lf , text "joins:" <+> ppr jf - , text "in_scope:" <+> ppr is ]) +-- , text "in_scope:" <+> ppr _is + ]) emptyFloats :: SimplEnv -> SimplFloats emptyFloats env ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -2098,8 +2098,9 @@ coercionIsSmall :: Coercion -> Bool -- This function is called inside `exprIsTrivial` so it needs to be -- pretty efficient. It should return False quickly on a big coercion; -- it should /not/ traverse the big coercion! +-- The literal constant 40# is pretty arbitrary coercionIsSmall co - = not (isTrue# ((coercion_is_small co 100#) <# 0#)) + = not (isTrue# ((coercion_is_small co 40#) <# 0#)) coercion_is_small :: Coercion -> Int# -> Int# coercion_is_small co n = go co n ===================================== compiler/GHC/Data/TrieMap.hs ===================================== @@ -359,7 +359,6 @@ mpList f (LM { lm_nil = mnil, lm_cons = mcons }) Note [Compressed TrieMap] ~~~~~~~~~~~~~~~~~~~~~~~~~ - The GenMap constructor augments TrieMaps with leaf compression. This helps solve the performance problem detailed in #9960: suppose we have a handful H of entries in a TrieMap, each with a very large key, size K. If you fold over ===================================== compiler/GHC/Iface/Make.hs ===================================== @@ -199,7 +199,11 @@ updateDecl decls m_stg_infos m_cmm_infos m_cmm_infos tag_sigs = fromMaybe mempty m_stg_infos - update_decl (IfaceId nm ty details infos) + update_decl decl@(IfaceId nm ty details infos) + | IfCoVarId <- details + = decl -- Coercions can appear at top level in interface files + -- but we generate no code for them and they have no LFInfo + | let not_caffy = elemNameSet nm non_cafs , let mb_lf_info = lookupNameEnv lf_infos nm , let sig = lookupNameEnv tag_sigs nm ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -1698,12 +1698,21 @@ tcIfaceExpr (IfaceCase scrut case_bndr alts) = do return (Case scrut' case_bndr' (coreAltsType alts') alts') tcIfaceExpr (IfaceLet (IfaceNonRec (IfLetBndr fs ty info ji) rhs) body) + | IfaceCo co <- rhs + = -- For CoVars we ignore `info` and `ji` + do { name <- newIfaceName (mkVarOccFS (ifLclNameFS fs)) + ; ty' <- tcIfaceType ty + ; let covar = mkLocalCoVar name ty' + ; co' <- tcIfaceCo co + ; body' <- extendIfaceIdEnv [covar] (tcIfaceExpr body) + ; return (Let (NonRec covar (Coercion co')) body') } + | otherwise = do { name <- newIfaceName (mkVarOccFS (ifLclNameFS fs)) ; ty' <- tcIfaceType ty ; id_info <- tcIdInfo False {- Don't ignore prags; we are inside one! -} NotTopLevel name ty' info ; let id = mkLocalIdWithInfo name ManyTy ty' id_info - `asJoinId_maybe` ji + `asJoinId_maybe` ji ; rhs' <- tcIfaceExpr rhs ; body' <- extendIfaceIdEnv [id] (tcIfaceExpr body) ; return (Let (NonRec id rhs') body') } ===================================== compiler/GHC/Types/Id.hs ===================================== @@ -329,8 +329,8 @@ mkLocalIdOrCoVar name w ty | isCoVarType ty = mkLocalCoVar name ty | otherwise = mkLocalId name w ty - -- proper ids only; no covars! mkLocalIdWithInfo :: HasDebugCallStack => Name -> Mult -> Type -> IdInfo -> Id +-- Used for proper ids only; no covars! mkLocalIdWithInfo name w ty info = Var.mkLocalVar VanillaId name w (assert (not (isCoVarType ty)) ty) info -- Note [Free type variables] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/528c804fa394c2b7eb421078f953738... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/528c804fa394c2b7eb421078f953738... You're receiving this email because of your account on gitlab.haskell.org.