Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC Commits: c97fd3f5 by Simon Peyton Jones at 2025-10-26T00:07:09+01:00 better - - - - - 3 changed files: - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Errors/Hole.hs - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1602,6 +1602,8 @@ ds_hs_wrapper hs_wrap where go WpHole k = k $ \e -> e go (WpSubType w) k = go (optSubTypeHsWrapper w) k + -- See (DSST3) in Note [Deep subsumption and WpSubType] + -- in GHC.Tc.Types.Evidence go (WpTyApp ty) k = k $ \e -> App e (Type ty) go (WpEvLam ev) k = k $ Lam ev go (WpTyLam tv) k = k $ Lam tv ===================================== compiler/GHC/Tc/Errors/Hole.hs ===================================== @@ -823,9 +823,11 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates = unfoldWrapper :: HsWrapper -> [Type] unfoldWrapper = reverse . unfWrp' - where unfWrp' (WpTyApp ty) = [ty] - unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2 - unfWrp' _ = [] + where + unfWrp' (WpTyApp ty) = [ty] + unfWrp' (WpSubType w) = unfWrp' w + unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2 + unfWrp' _ = [] -- The real work happens here, where we invoke the type checker using ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -138,7 +138,7 @@ maybeSymCo NotSwapped co = co {- Note [Deep subsumption and WpSubType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers. -For example (#26255) suppose we have +For example (#26349) suppose we have (forall a. Eq a => a->a) -> Int <= (forall a. Eq a => a->a) -> Int The two types are equal so we should certainly get an identity wrapper. But we'll get tihs wrapper from `tcSubType`: @@ -158,11 +158,11 @@ is not sound in general, so we'll end up retaining the lambdas. Two bad results may not be able to make a decent RULE at all, and will fail with "LHS of rule is too complicated to desugar (#26255) -It'd be nicest to solve the problem at source, by never generating those +It'd be ideal to solve the problem at source, by never generating those gruesome wrappers in the first place, but we can't do that because -* The WpTyLam and WpTyApp are not introduced together in `tcSubType`, so we can't - easily cancel them out. Even if we have +* The WpTyLam and WpTyApp are introduced independently, not together, in `tcSubType`, + so we can't easily cancel them out. For example, even if we have forall a. t1 <= forall a. t2 there is no guarantee that these are the "same" a. E.g. forall a b. a -> b -> b <= forall x y. y -> x - >x @@ -171,17 +171,23 @@ gruesome wrappers in the first place, but we can't do that because * We have not yet done constraint solving so we don't know what evidence will end up in those WpLet bindings. -TL;DR we must generate -Here's our solution +TL;DR we must generate the wrapper and then optimise it way if it turns out +that it is a no-op. Here's our solution (DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the terms! But in /subtype/ wrappers, these type/dictionary lambdas only scope over - the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is w + the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is what justifies us + eta-reducing the type/dictionarly lambdas. -(WpSubType wp) means the same as `wp`, but with the added promise that -the binders in `wp` do not scope over the hole + In short, (WpSubType wp) means the same as `wp`, but with the added promise that + the binders in `wp` do not scope over the hole + +(DSST2) Avoid creating a WpSubType in the common WpHole case, using `mkWpSubType`. + +(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType. + This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`. -} -- We write wrap :: t1 ~> t2 @@ -190,7 +196,7 @@ data HsWrapper = WpHole -- The identity coercion | WpSubType HsWrapper -- (WpSubType wp) Means the same as `wp` - -- But see Note [WpSubType] + -- See Note [Deep subsumption and WpSubType] (DSST1) | WpCompose HsWrapper HsWrapper -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]] @@ -299,6 +305,7 @@ mkWpFun w_arg w_res t1 t2 = WpFun w_arg w_res t1 t2 -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. mkWpSubType :: HsWrapper -> HsWrapper +-- See (DSST2) in Note [Deep subsumption and WpSubType] mkWpSubType WpHole = WpHole mkWpSubType (WpCast co) = WpCast co mkWpSubType w = WpSubType w @@ -393,7 +400,7 @@ hsWrapDictBinders wrap = go wrap go (w1 `WpCompose` w2) = go w1 `unionBags` go w2 go (WpFun _ w _ _) = go w go WpHole = emptyBag - go (WpSubType {}) = emptyBag -- See Note [WpSubType] + go (WpSubType {}) = emptyBag -- See Note [Deep subsumption and WpSubType] go (WpCast {}) = emptyBag go (WpEvApp {}) = emptyBag go (WpTyLam {}) = emptyBag @@ -420,9 +427,11 @@ collectHsWrapBinders wrap = go wrap [] optSubTypeHsWrapper :: HsWrapper -> HsWrapper +-- This optimiser is used only on the payload of WpSubType +-- It finds cases where the entire wrapper is a no-op +-- See (DSST3) in Note [Deep subsumption and WpSubType] optSubTypeHsWrapper wrap - = -- pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $ - opt wrap + = opt wrap where opt :: HsWrapper -> HsWrapper opt w = foldr (<.>) WpHole (opt1 w []) @@ -436,18 +445,17 @@ optSubTypeHsWrapper wrap opt1 (WpCast co) ws = opt_co co ws opt1 (WpEvLam ev) ws = opt_ev_lam ev ws opt1 (WpTyLam tv) ws = opt_ty_lam tv ws - opt1 (WpLet binds) ws = opt_let binds ws + opt1 (WpLet binds) ws = pushWpLet binds ws opt1 (WpFun w1 w2 sty1 ty2) ws = mk_wp_fun (opt w1) (opt w2) sty1 ty2 ws opt1 w@(WpTyApp {}) ws = w : ws opt1 w@(WpEvApp {}) ws = w : ws - ------------------ - opt_let b@(EvBinds bs) ws | isEmptyBag bs = ws - | otherwise = WpLet b : ws - opt_let (TcEvBinds {}) _ = pprPanic "optHsWrapper1" (ppr wrap) - ----------------- -- (WpTyLam a <+> WpTyApp a <+> w) = w + -- i.e. /\a. <hole> a --> <hole> + -- This is only valid if whatever fills the hole does not mention 'a' + -- But that's guaranteed in subtype-wrappers; + -- see (DSST1) in Note [Deep subsumption and WpSubType] opt_ty_lam tv (WpTyApp ty : ws) | Just tv' <- getTyVar_maybe ty , tv==tv' @@ -458,15 +466,12 @@ optSubTypeHsWrapper wrap opt_ty_lam tv (WpCast co : ws) = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws) - opt_ty_lam tv (WpLet bs : ws) - | Just ws' <- pushWpLet bs ws - = opt_ty_lam tv ws' - opt_ty_lam tv ws = WpTyLam tv : ws ----------------- -- (WpEvLam ev <+> WpEvAp ev <+> w) = w + -- Similar notes to WpTyLam opt_ev_lam ev (WpEvApp ev_tm : ws) | EvExpr (Var ev') <- ev_tm , ev == ev' @@ -481,9 +486,6 @@ optSubTypeHsWrapper wrap (mkNomReflCo ManyTy) (mkRepReflCo (idType ev)) co - opt_ev_lam ev (WpLet bs : ws) - | Just ws' <- pushWpLet bs ws - = opt_ev_lam ev ws' opt_ev_lam ev ws = WpEvLam ev : ws @@ -505,48 +507,64 @@ optSubTypeHsWrapper wrap where co_ify co1 co2 = opt_co (mk_wp_fun_co w co1 co2) ws -pushWpLet :: TcEvBinds -> [HsWrapper] -> Maybe [HsWrapper] +pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper] +-- See if we can transform +-- WpLet binds <.> w1 <.> .. <.> wn --> w1' <.> .. <.> wn' +-- by substitution. +-- We do this just for the narrow case when +-- - the `binds` are all just v=w, variables only +-- - the wi are all WpTyApp, WpEvApp, or WpCast +-- This is just enough to get us the eta-reductions that we seek pushWpLet tc_ev_binds ws - | EvBinds binds <- tc_ev_binds - , Just env <- evBindIdSwizzle binds - = go env ws - | otherwise - = Nothing + = case tc_ev_binds of + TcEvBinds {} -> pprPanic "pushWpLet" (ppr tc_ev_binds) + EvBinds binds + | isEmptyBag binds + -> ws + | Just env <- ev_bind_swizzle binds + -> case go env ws of + Just ws' -> ws' + Nothing -> bale_out + | otherwise + -> bale_out where + bale_out = WpLet tc_ev_binds : ws + go :: IdEnv Id -> [HsWrapper] -> Maybe [HsWrapper] go env (WpCast co : ws) = do { ws' <- go env ws ; return (WpCast co : ws') } go env (WpTyApp ty : ws) = do { ws' <- go env ws ; return (WpTyApp ty : ws') } go env (WpEvApp (EvExpr (Var v)) : ws) - = do { v' <- swizzleId env v + = do { v' <- swizzle_id env v ; ws' <- go env ws ; return (WpEvApp (EvExpr (Var v')) : ws') } go _ ws = case ws of [] -> Just [] - (_:_) -> Nothing -- Could not fully eliminate it + (_:_) -> Nothing -- Could not fully eliminate the WpLet -swizzleId :: IdEnv Id -> Id -> Maybe Id --- Nothing <=> ran out of fuel --- Shoul -swizzleId env v = go 100 v - where - go :: Int -> EvId -> Maybe EvId - go fuel v - | fuel == 0 = Nothing - | Just v' <- lookupVarEnv env v = go (fuel-1) v' - | otherwise = Just v - -evBindIdSwizzle :: Bag EvBind -> Maybe (IdEnv Id) -evBindIdSwizzle evbs = foldl' do_one (Just emptyVarEnv) evbs - where - do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id) - do_one Nothing _ = Nothing - do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs}) - = case rhs of - EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v) - _ -> Nothing + swizzle_id :: IdEnv Id -> Id -> Maybe Id + -- Nothing <=> ran out of fuel + -- This is just belt and braces; we should never build bottom evidence + swizzle_id env v = go 100 v + where + go :: Int -> EvId -> Maybe EvId + go fuel v + | fuel == 0 = Nothing + | Just v' <- lookupVarEnv env v = go (fuel-1) v' + | otherwise = Just v + + ev_bind_swizzle :: Bag EvBind -> Maybe (IdEnv Id) + -- Succeeds only if the bindings are all var-to-var bindings + ev_bind_swizzle evbs = foldl' do_one (Just emptyVarEnv) evbs + where + do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id) + do_one Nothing _ = Nothing + do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs}) + = case rhs of + EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v) + _ -> Nothing {- ************************************************************************ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c97fd3f51c07bca9b2e66545a7bdaac3... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c97fd3f51c07bca9b2e66545a7bdaac3... You're receiving this email because of your account on gitlab.haskell.org.