Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC Commits: 1fd25fe1 by Simon Peyton Jones at 2025-10-23T17:42:47+01:00 Working, I think - - - - - 1 changed file: - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -362,9 +362,11 @@ collectHsWrapBinders wrap = go wrap [] 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' where - norm :: HsWrapper -> VarEnv EvVar -> [HsWrapper] -> [HsWrapper] + norm :: HsWrapper -> [HsWrapper] -> [HsWrapper] -- norm w ws = w <.> (foldr <.> WpHole ws) -- INVARIANT: ws:[HsWrapper] is normalised norm WpHole ws = ws @@ -393,6 +395,11 @@ optHsWrapper wrap -- = WpCast (ForAllCo a co) (WpTyLam <.> w) norm_ty_lam tv (WpCast co : ws) = norm_co (mkHomoForAllCo tv co) (norm_ty_lam tv ws) + + norm_ty_lam tv (WpLet bs : ws) + | Just ws' <- pushWpLet bs ws + = norm_ty_lam tv ws' + norm_ty_lam tv ws = WpTyLam tv : ws @@ -412,10 +419,15 @@ optHsWrapper wrap (mkNomReflCo ManyTy) (mkRepReflCo (idType ev)) co + norm_ev_lam ev (WpLet bs : ws) + | Just ws' <- pushWpLet bs ws + = norm_ev_lam ev ws' + norm_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 @@ -424,6 +436,7 @@ optHsWrapper wrap norm_fun w1 w2 (Scaled w t1) t2 ws = case (optHsWrapper w1, optHsWrapper 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, WpCast co2) -> co_ify (mkSymCo co1) co2 @@ -431,6 +444,60 @@ optHsWrapper wrap where co_ify co1 co2 = norm_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' + | 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) + + +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 {- ************************************************************************ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1fd25fe1bfdbcedd9fd2db528aa3b66b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1fd25fe1bfdbcedd9fd2db528aa3b66b... You're receiving this email because of your account on gitlab.haskell.org.