Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC Commits: ce4975ed by Simon Peyton Jones at 2025-10-25T12:51:24+01:00 Better now Added WpSubType - - - - - 5 changed files: - compiler/GHC/Hs/Syn/Type.hs - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/Type.hs Changes: ===================================== compiler/GHC/Hs/Syn/Type.hs ===================================== @@ -191,6 +191,7 @@ hsWrapperType :: HsWrapper -> Type -> Type hsWrapperType wrap ty = prTypeType $ go wrap (ty,[]) where go WpHole = id + go (WpSubType w) = go w go (w1 `WpCompose` w2) = go w1 . go w2 go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t -> let act_res = funResultTy t ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1598,9 +1598,10 @@ ds_hs_wrapper :: HsWrapper -> ((CoreExpr -> CoreExpr) -> DsM a) -> DsM a ds_hs_wrapper hs_wrap - = go (optHsWrapper hs_wrap) + = go hs_wrap where go WpHole k = k $ \e -> e + go (WpSubType w) k = go (optSubTypeHsWrapper w) k 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/Types/Evidence.hs ===================================== @@ -8,11 +8,11 @@ module GHC.Tc.Types.Evidence ( -- * HsWrapper HsWrapper(..), (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast, - mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, + mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, mkWpSubType, collectHsWrapBinders, idHsWrapper, isIdHsWrapper, pprHsWrapper, hsWrapDictBinders, - optHsWrapper, + optSubTypeHsWrapper, -- * Evidence bindings TcEvBinds(..), EvBindsVar(..), @@ -135,11 +135,20 @@ maybeSymCo NotSwapped co = co ************************************************************************ -} +{- Note [WpSubType] +~~~~~~~~~~~~~~~~~~~ +(WpSubType wp) means the same as `wp`, but with the added promise that +the binders in `wp` do not scope over the hole +-} + -- We write wrap :: t1 ~> t2 -- if wrap[ e::t1 ] :: t2 data HsWrapper = WpHole -- The identity coercion + | WpSubType HsWrapper -- (WpSubType wp) Means the same as `wp` + -- But see Note [WpSubType] + | WpCompose HsWrapper HsWrapper -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]] -- @@ -246,6 +255,11 @@ mkWpFun w_arg w_res t1 t2 = WpFun w_arg w_res t1 t2 -- Unfortunately, we can't check this with an assertion here, because of -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. +mkWpSubType :: HsWrapper -> HsWrapper +mkWpSubType WpHole = WpHole +mkWpSubType (WpCast co) = WpCast co +mkWpSubType w = WpSubType w + mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper -- (mkWpEta [x1, x2] wrap) [e] -- = \x1. \x2. wrap[e x1 x2] @@ -336,6 +350,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 (WpCast {}) = emptyBag go (WpEvApp {}) = emptyBag go (WpTyLam {}) = emptyBag @@ -351,6 +366,7 @@ collectHsWrapBinders wrap = go wrap [] go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper) go (WpEvLam v) wraps = add_lam v (gos wraps) go (WpTyLam v) wraps = add_lam v (gos wraps) + go (WpSubType w) wraps = go w wraps go (WpCompose w1 w2) wraps = go w1 (w2:wraps) go wrap wraps = ([], foldl' (<.>) wrap wraps) @@ -360,124 +376,113 @@ collectHsWrapBinders wrap = go wrap [] add_lam v (vs,w) = (v:vs, w) -optHsWrapper :: HsWrapper -> HsWrapper -optHsWrapper wrap - = foldr (<.>) WpHole (norm wrap []) - -- let wrap' = foldr (<.>) WpHole (norm wrap []) - -- in pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr wrap' ]) $ - -- wrap' +optSubTypeHsWrapper :: HsWrapper -> HsWrapper +optSubTypeHsWrapper wrap + = pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $ + opt wrap where - norm :: HsWrapper -> [HsWrapper] -> [HsWrapper] - -- norm w ws = w <.> (foldr <.> WpHole ws) - -- INVARIANT: ws:[HsWrapper] is normalised - norm WpHole ws = ws - norm (w1 `WpCompose` w2) ws = norm w1 (norm w2 ws) - norm (WpCast co) ws = norm_co co ws - norm (WpEvLam ev) ws = norm_ev_lam ev ws - norm (WpTyLam tv) ws = norm_ty_lam tv ws - norm (WpLet binds) ws = norm_let binds ws - norm (WpFun w1 w2 sty1 ty2) ws = norm_fun w1 w2 sty1 ty2 ws - norm w@(WpTyApp {}) ws = w : ws - norm w@(WpEvApp {}) ws = w : ws + opt :: HsWrapper -> HsWrapper + opt w = foldr (<.>) WpHole (opt1 w []) + + opt1 :: HsWrapper -> [HsWrapper] -> [HsWrapper] + -- opt1 w ws = w <.> (foldr <.> WpHole ws) + -- INVARIANT: ws:[HsWrapper] is optimised + opt1 WpHole ws = ws + opt1 (WpSubType w) ws = opt1 w ws + opt1 (w1 `WpCompose` w2) ws = opt1 w1 (opt1 w2 ws) + 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 (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 ------------------ - norm_let b@(EvBinds bs) ws | isEmptyBag bs = ws - | otherwise = WpLet b : ws - norm_let (TcEvBinds {}) _ = pprPanic "optHsWrapper1" (ppr wrap) + 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 - norm_ty_lam tv (WpTyApp ty : ws) + opt_ty_lam tv (WpTyApp ty : ws) | Just tv' <- getTyVar_maybe ty , tv==tv' = ws -- (WpTyLam a <+> WpCastCo co <+> w) -- = WpCast (ForAllCo a co) (WpTyLam <.> w) - norm_ty_lam tv (WpCast co : ws) - = norm_co (mkHomoForAllCo tv co) (norm_ty_lam tv ws) + opt_ty_lam tv (WpCast co : ws) + = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws) - norm_ty_lam tv (WpLet bs : ws) + opt_ty_lam tv (WpLet bs : ws) | Just ws' <- pushWpLet bs ws - = norm_ty_lam tv ws' + = opt_ty_lam tv ws' - norm_ty_lam tv ws + opt_ty_lam tv ws = WpTyLam tv : ws ----------------- -- (WpEvLam ev <+> WpEvAp ev <+> w) = w - norm_ev_lam ev (WpEvApp ev_tm : ws) + opt_ev_lam ev (WpEvApp ev_tm : ws) | EvExpr (Var ev') <- ev_tm , ev == ev' = ws -- (WpEvLam ev <.> WpCast co <.> w) -- = WpCast (FunCo ev co) (WpEvLam <.> w) - norm_ev_lam ev (WpCast co : ws) - = norm_co fun_co (norm_ev_lam ev ws) + opt_ev_lam ev (WpCast co : ws) + = opt_co fun_co (opt_ev_lam ev ws) where fun_co = mkFunCo Representational FTF_C_T (mkNomReflCo ManyTy) (mkRepReflCo (idType ev)) co - norm_ev_lam ev (WpLet bs : ws) + opt_ev_lam ev (WpLet bs : ws) | Just ws' <- pushWpLet bs ws - = norm_ev_lam ev ws' + = opt_ev_lam ev ws' - norm_ev_lam ev ws + opt_ev_lam ev ws = WpEvLam ev : ws ----------------- -- WpCast co <.> WpCast co' <+> ws = WpCast (co;co') ws - norm_co co (WpCast co' : ws) = norm_co (co `mkTransCo` co') ws - norm_co co ws | isReflexiveCo co = ws - | otherwise = WpCast co : ws + opt_co co (WpCast co' : ws) = opt_co (co `mkTransCo` co') ws + opt_co co ws | isReflexiveCo co = ws + | otherwise = WpCast co : ws ------------------ - norm_fun w1 w2 (Scaled w t1) t2 ws - = case (optHsWrapper w1, optHsWrapper w2) of + mk_wp_fun w1 w2 sty1@(Scaled w t1) ty2 ws + = case (w1, w2) of (WpHole, WpHole) -> ws - (WpLet {}, WpHole) -> ws (WpHole, WpCast co2) -> co_ify (mkRepReflCo t1) co2 - (WpCast co1, WpHole) -> co_ify (mkSymCo co1) (mkRepReflCo t2) + (WpCast co1, WpHole) -> co_ify (mkSymCo co1) (mkRepReflCo ty2) (WpCast co1, WpCast co2) -> co_ify (mkSymCo co1) co2 - (w1', w2') -> WpFun w1' w2' (Scaled w t1) t2 : ws + (w1', w2') -> WpFun w1' w2' sty1 ty2 : ws where - co_ify co1 co2 = norm_co (mk_wp_fun_co w co1 co2) ws + co_ify co1 co2 = opt_co (mk_wp_fun_co w co1 co2) ws pushWpLet :: TcEvBinds -> [HsWrapper] -> Maybe [HsWrapper] pushWpLet tc_ev_binds ws | EvBinds binds <- tc_ev_binds , Just env <- evBindIdSwizzle binds - = case go env ws of - WpLet {} : _ -> Nothing - ws' -> Just ws' + = go env ws | otherwise = Nothing where - go :: IdEnv Id -> [HsWrapper] -> [HsWrapper] - go env (WpTyApp ty : ws') = WpTyApp ty : go env ws' - go env (WpCast co : ws') = WpCast co : go env ws' - go env (WpTyLam tv : ws') - | not (tv_captures env tv) - = WpTyLam tv : go env ws' - - go env (WpEvLam ev : ws') - | not (ev `elemVarEnv` env) -- `ev` must not be in the domain - , not (anyVarEnv (== ev) env) -- or range of `env` - = WpEvLam ev : go env ws' - - go env (WpEvApp (EvExpr (Var v)) : ws') - | Just v' <- swizzleId env v - = WpEvApp (EvExpr (Var v')) : go env ws' - - go _ ws = WpLet tc_ev_binds : ws - - tv_captures :: IdEnv Id -> TyVar -> Bool - tv_captures env tv = anyVarEnv bad env - where - bad id = anyFreeVarsOfType (== tv) (idType id) - + 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 + ; ws' <- go env ws + ; return (WpEvApp (EvExpr (Var v')) : ws') } + + go _ ws = case ws of + [] -> Just [] + (_:_) -> Nothing -- Could not fully eliminate it swizzleId :: IdEnv Id -> Id -> Maybe Id -- Nothing <=> ran out of fuel @@ -1158,7 +1163,8 @@ pprHsWrapper wrap pp_thing_inside -- True <=> appears in function application position -- False <=> appears as body of let or lambda help it WpHole = it - help it (WpCompose f1 f2) = help (help it f2) f1 + help it (WpCompose w1 w2) = help (help it w2) w1 + help it (WpSubType w) = no_parens $ text "subtype" <> braces (help it w False) help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+> help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>" ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -1426,11 +1426,12 @@ tcSubTypeDS :: HsExpr GhcRn -- DeepSubsumption <=> when checking, this type -- is deeply skolemised -> TcM HsWrapper --- Only one call site, in GHC.Tc.Gen.App.tcApp +-- Only one call site, in GHC.Tc.Gen.App.checkResultTy tcSubTypeDS rn_expr act_rho exp_rho - = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho - where - orig = exprCtOrigin rn_expr + = do { wrap <- tc_sub_type_deep Top (unifyExprType rn_expr) + (exprCtOrigin rn_expr) + GenSigCtxt act_rho exp_rho + ; return (mkWpSubType wrap) } --------------- @@ -1503,7 +1504,8 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify ---------------------- tc_sub_type unify inst_orig ctxt ty_actual ty_expected = do { ds_flag <- getDeepSubsumptionFlag - ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected } + ; wrap <- tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected + ; return (mkWpSubType wrap) } ---------------------- tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only) ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -1231,6 +1231,8 @@ zonk_cmd_top (HsCmdTop (CmdTopTc stack_tys ty ids) cmd) ------------------------------------------------------------------------- zonkCoFn :: HsWrapper -> ZonkBndrTcM HsWrapper zonkCoFn WpHole = return WpHole +zonkCoFn (WpSubType w) = do { w' <- zonkCoFn w + ; return (WpSubType w') } zonkCoFn (WpCompose c1 c2) = do { c1' <- zonkCoFn c1 ; c2' <- zonkCoFn c2 ; return (WpCompose c1' c2') } View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce4975ed0c0af9479fc5ab11e25f7f27... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce4975ed0c0af9479fc5ab11e25f7f27... You're receiving this email because of your account on gitlab.haskell.org.