Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC
Commits:
-
2004c1aa
by Simon Peyton Jones at 2025-10-26T23:43:34+00:00
5 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
| ... | ... | @@ -809,7 +809,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args |
| 809 | 809 | = do { let herald = case fun_ctxt of
|
| 810 | 810 | VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
|
| 811 | 811 | _ -> ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
|
| 812 | - ; (wrap, arg_ty, res_ty) <-
|
|
| 812 | + ; (fun_co, arg_ty, res_ty) <-
|
|
| 813 | 813 | -- NB: matchActualFunTy does the rep-poly check.
|
| 814 | 814 | -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
|
| 815 | 815 | -- In an application (f x), we need 'x' to have a fixed runtime
|
| ... | ... | @@ -820,7 +820,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args |
| 820 | 820 | (n_val_args, fun_sigma) fun_ty
|
| 821 | 821 | |
| 822 | 822 | ; arg' <- quickLookArg do_ql ctxt arg arg_ty
|
| 823 | - ; let acc' = arg' : addArgWrap wrap acc
|
|
| 823 | + ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
|
|
| 824 | 824 | ; go (pos+1) acc' res_ty rest_args }
|
| 825 | 825 | |
| 826 | 826 | new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
|
| ... | ... | @@ -765,13 +765,13 @@ tcInferOverLit lit@(OverLit { ol_val = val |
| 765 | 765 | thing = NameThing from_name
|
| 766 | 766 | mb_thing = Just thing
|
| 767 | 767 | herald = ExpectedFunTyArg thing (HsLit noExtField hs_lit)
|
| 768 | - ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
|
|
| 768 | + ; (co2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
|
|
| 769 | 769 | |
| 770 | 770 | ; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
|
| 771 | 771 | -- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
|
| 772 | 772 | ; let lit_expr = L (l2l loc) $ mkHsWrapCo co $
|
| 773 | 773 | HsLit noExtField hs_lit
|
| 774 | - from_expr = mkHsWrap (wrap2 <.> wrap1) $
|
|
| 774 | + from_expr = mkHsWrap (mkWpCastN co2 <.> wrap1) $
|
|
| 775 | 775 | mkHsVar (L loc from_id)
|
| 776 | 776 | witness = HsApp noExtField (L (l2l loc) from_expr) lit_expr
|
| 777 | 777 | lit' = OverLit { ol_val = val
|
| ... | ... | @@ -701,7 +701,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of |
| 701 | 701 | |
| 702 | 702 | -- Expression must be a function
|
| 703 | 703 | ; let herald = ExpectedFunTyViewPat $ unLoc expr
|
| 704 | - ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
|
|
| 704 | + ; (expr_co1, Scaled _mult inf_arg_ty, inf_res_sigma)
|
|
| 705 | 705 | <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho
|
| 706 | 706 | -- See Note [View patterns and polymorphism]
|
| 707 | 707 | -- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma)
|
| ... | ... | @@ -722,7 +722,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of |
| 722 | 722 | -- NB: pat_ty comes from matchActualFunTy, so it has a
|
| 723 | 723 | -- fixed RuntimeRep, as needed to call mkWpFun.
|
| 724 | 724 | |
| 725 | - expr_wrap = expr_wrap2' <.> expr_wrap1
|
|
| 725 | + expr_wrap = expr_wrap2' <.> mkWpCastN expr_co1
|
|
| 726 | 726 | |
| 727 | 727 | ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
|
| 728 | 728 |
| ... | ... | @@ -290,19 +290,24 @@ mkWpFun :: HsWrapper -> HsWrapper |
| 290 | 290 | -> TcType -- ^ Either "from" type or "to" type of the second wrapper
|
| 291 | 291 | -- (used only when the second wrapper is the identity)
|
| 292 | 292 | -> HsWrapper
|
| 293 | -mkWpFun WpHole WpHole _ _ = WpHole
|
|
| 294 | -mkWpFun w_arg w_res t1 t2 = WpFun w_arg w_res t1 t2
|
|
| 295 | - -- In this case, we will desugar to a lambda
|
|
| 296 | - --
|
|
| 297 | - -- \x. w_res[ e w_arg[x] ]
|
|
| 298 | - --
|
|
| 299 | - -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
|
|
| 300 | - -- it must be the case that both the lambda bound variable x and the function
|
|
| 301 | - -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
|
|
| 302 | - -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
|
|
| 303 | - --
|
|
| 304 | - -- Unfortunately, we can't check this with an assertion here, because of
|
|
| 305 | - -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
|
|
| 293 | +mkWpFun w1 w2 st1@(Scaled m1 t1) t2
|
|
| 294 | + = case (w1,w2) of
|
|
| 295 | + (WpHole, WpHole) -> WpHole
|
|
| 296 | + (WpHole, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkRepReflCo t1) co2)
|
|
| 297 | + (WpCast co1, WpHole) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) (mkRepReflCo t2))
|
|
| 298 | + (WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) co2)
|
|
| 299 | + (_, _) -> WpFun w1 w2 st1 t2
|
|
| 300 | + -- In the WpFun case, we will desugar to a lambda
|
|
| 301 | + --
|
|
| 302 | + -- \x. w_res[ e w_arg[x] ]
|
|
| 303 | + --
|
|
| 304 | + -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
|
|
| 305 | + -- it must be the case that both the lambda bound variable x and the function
|
|
| 306 | + -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
|
|
| 307 | + -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
|
|
| 308 | + --
|
|
| 309 | + -- Unfortunately, we can't check this with an assertion here, because of
|
|
| 310 | + -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
|
|
| 306 | 311 | |
| 307 | 312 | mkWpSubType :: HsWrapper -> HsWrapper
|
| 308 | 313 | -- See (DSST2) in Note [Deep subsumption and WpSubType]
|
| ... | ... | @@ -446,7 +451,7 @@ optSubTypeHsWrapper wrap |
| 446 | 451 | opt1 (WpEvLam ev) ws = opt_ev_lam ev ws
|
| 447 | 452 | opt1 (WpTyLam tv) ws = opt_ty_lam tv ws
|
| 448 | 453 | opt1 (WpLet binds) ws = pushWpLet binds ws
|
| 449 | - opt1 (WpFun w1 w2 sty1 ty2) ws = mk_wp_fun (opt w1) (opt w2) sty1 ty2 ws
|
|
| 454 | + opt1 (WpFun w1 w2 sty1 ty2) ws = opt_fun w1 w2 sty1 ty2 ws
|
|
| 450 | 455 | opt1 w@(WpTyApp {}) ws = w : ws
|
| 451 | 456 | opt1 w@(WpEvApp {}) ws = w : ws
|
| 452 | 457 | |
| ... | ... | @@ -459,6 +464,7 @@ optSubTypeHsWrapper wrap |
| 459 | 464 | opt_ty_lam tv (WpTyApp ty : ws)
|
| 460 | 465 | | Just tv' <- getTyVar_maybe ty
|
| 461 | 466 | , tv==tv'
|
| 467 | + , all (not_in tv) ws
|
|
| 462 | 468 | = ws
|
| 463 | 469 | |
| 464 | 470 | -- (WpTyLam a <+> WpCastCo co <+> w)
|
| ... | ... | @@ -475,6 +481,7 @@ optSubTypeHsWrapper wrap |
| 475 | 481 | opt_ev_lam ev (WpEvApp ev_tm : ws)
|
| 476 | 482 | | EvExpr (Var ev') <- ev_tm
|
| 477 | 483 | , ev == ev'
|
| 484 | + , all (not_in ev) ws
|
|
| 478 | 485 | = ws
|
| 479 | 486 | |
| 480 | 487 | -- (WpEvLam ev <.> WpCast co <.> w)
|
| ... | ... | @@ -497,15 +504,28 @@ optSubTypeHsWrapper wrap |
| 497 | 504 | | otherwise = WpCast co : ws
|
| 498 | 505 | |
| 499 | 506 | ------------------
|
| 500 | - mk_wp_fun w1 w2 sty1@(Scaled w t1) ty2 ws
|
|
| 501 | - = case (w1, w2) of
|
|
| 502 | - (WpHole, WpHole) -> ws
|
|
| 503 | - (WpHole, WpCast co2) -> co_ify (mkRepReflCo t1) co2
|
|
| 504 | - (WpCast co1, WpHole) -> co_ify (mkSymCo co1) (mkRepReflCo ty2)
|
|
| 505 | - (WpCast co1, WpCast co2) -> co_ify (mkSymCo co1) co2
|
|
| 506 | - (w1', w2') -> WpFun w1' w2' sty1 ty2 : ws
|
|
| 507 | - where
|
|
| 508 | - co_ify co1 co2 = opt_co (mk_wp_fun_co w co1 co2) ws
|
|
| 507 | + opt_fun w1 w2 sty1 ty2 ws
|
|
| 508 | + = case mkWpFun (opt w1) (opt w2) sty1 ty2 of
|
|
| 509 | + WpHole -> ws
|
|
| 510 | + WpCast co -> opt_co co ws
|
|
| 511 | + w -> w : ws
|
|
| 512 | + |
|
| 513 | + ------------------
|
|
| 514 | + -- Tiresome check that the lambda-bound type/evidence variable that we
|
|
| 515 | + -- want to eta-reduce isn't free in the rest of the wrapper
|
|
| 516 | + not_in :: TyVar -> HsWrapper -> Bool
|
|
| 517 | + not_in _ WpHole = True
|
|
| 518 | + not_in v (WpCast co) = not (anyFreeVarsOfCo (== v) co)
|
|
| 519 | + not_in v (WpTyApp ty) = not (anyFreeVarsOfType (== v) ty)
|
|
| 520 | + not_in v (WpFun w1 w2 _ _) = not_in v w1 && not_in v w2
|
|
| 521 | + not_in v (WpSubType w) = not_in v w
|
|
| 522 | + not_in v (WpCompose w1 w2) = not_in v w1 && not_in v w2
|
|
| 523 | + not_in v (WpEvApp (EvExpr e)) = not (v `elemVarSet` exprFreeVars e)
|
|
| 524 | + not_in _ (WpEvApp (EvTypeable {})) = False -- Giving up; conservative
|
|
| 525 | + not_in _ (WpEvApp (EvFun {})) = False -- Giving up; conservative
|
|
| 526 | + not_in _ (WpTyLam {}) = False -- Give up; conservative
|
|
| 527 | + not_in _ (WpEvLam {}) = False -- Ditto
|
|
| 528 | + not_in _ (WpLet {}) = False -- Ditto
|
|
| 509 | 529 | |
| 510 | 530 | pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper]
|
| 511 | 531 | -- See if we can transform
|
| ... | ... | @@ -147,7 +147,7 @@ matchActualFunTy |
| 147 | 147 | -- (Both are used only for error messages)
|
| 148 | 148 | -> TcRhoType
|
| 149 | 149 | -- ^ Type to analyse: a TcRhoType
|
| 150 | - -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
|
|
| 150 | + -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
|
|
| 151 | 151 | -- This function takes in a type to analyse (a RhoType) and returns
|
| 152 | 152 | -- an argument type and a result type (splitting apart a function arrow).
|
| 153 | 153 | -- The returned argument type is a SigmaType with a fixed RuntimeRep;
|
| ... | ... | @@ -171,13 +171,13 @@ matchActualFunTy herald mb_thing err_info fun_ty |
| 171 | 171 | -- hide the forall inside a meta-variable
|
| 172 | 172 | go :: TcRhoType -- The type we're processing, perhaps after
|
| 173 | 173 | -- expanding type synonyms
|
| 174 | - -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
|
|
| 174 | + -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
|
|
| 175 | 175 | go ty | Just ty' <- coreView ty = go ty'
|
| 176 | 176 | |
| 177 | 177 | go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
|
| 178 | 178 | = assert (isVisibleFunArg af) $
|
| 179 | 179 | do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty
|
| 180 | - ; return (idHsWrapper, Scaled w arg_ty, res_ty) }
|
|
| 180 | + ; return (mkNomReflCo fun_ty, Scaled w arg_ty, res_ty) }
|
|
| 181 | 181 | |
| 182 | 182 | go ty@(TyVarTy tv)
|
| 183 | 183 | | isMetaTyVar tv
|
| ... | ... | @@ -209,7 +209,7 @@ matchActualFunTy herald mb_thing err_info fun_ty |
| 209 | 209 | ; res_ty <- newOpenFlexiTyVarTy
|
| 210 | 210 | ; let unif_fun_ty = mkScaledFunTys [arg_ty] res_ty
|
| 211 | 211 | ; co <- unifyType mb_thing fun_ty unif_fun_ty
|
| 212 | - ; return (mkWpCastN co, arg_ty, res_ty) }
|
|
| 212 | + ; return (co, arg_ty, res_ty) }
|
|
| 213 | 213 | |
| 214 | 214 | ------------
|
| 215 | 215 | mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, ErrCtxtMsg)
|
| ... | ... | @@ -248,8 +248,8 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected |
| 248 | 248 | -> Arity
|
| 249 | 249 | -> TcSigmaType
|
| 250 | 250 | -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
|
| 251 | --- If matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
|
|
| 252 | --- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
|
|
| 251 | +-- If matchActualFunTys n fun_ty = (wrap, [t1,..,tn], res_ty)
|
|
| 252 | +-- then wrap : fun_ty ~> (t1 -> ... -> tn -> res_ty)
|
|
| 253 | 253 | -- and res_ty is a RhoType
|
| 254 | 254 | -- NB: the returned type is top-instantiated; it's a RhoType
|
| 255 | 255 | matchActualFunTys herald ct_orig n_val_args_wanted top_ty
|
| ... | ... | @@ -264,15 +264,13 @@ matchActualFunTys herald ct_orig n_val_args_wanted top_ty |
| 264 | 264 | go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
|
| 265 | 265 | |
| 266 | 266 | go n so_far fun_ty
|
| 267 | - = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
|
|
| 268 | - herald Nothing
|
|
| 269 | - (n_val_args_wanted, top_ty)
|
|
| 270 | - fun_ty
|
|
| 271 | - ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
|
|
| 267 | + = do { (co1, arg_ty1, res_ty1) <- matchActualFunTy herald Nothing
|
|
| 268 | + (n_val_args_wanted, top_ty) fun_ty
|
|
| 269 | + ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
|
|
| 272 | 270 | ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
|
| 273 | 271 | -- NB: arg_ty1 comes from matchActualFunTy, so it has
|
| 274 | - -- a syntactically fixed RuntimeRep as needed to call mkWpFun.
|
|
| 275 | - ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
|
|
| 272 | + -- a syntactically fixed RuntimeRep
|
|
| 273 | + ; return (wrap_fun2 <.> mkWpCastN co1, arg_ty1:arg_tys, res_ty) }
|
|
| 276 | 274 | |
| 277 | 275 | {-
|
| 278 | 276 | ************************************************************************
|