Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC Commits: 076f9021 by Simon Peyton Jones at 2025-10-27T10:51:28+00:00 Comments and one test wibble - - - - - 3 changed files: - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/simplCore/should_compile/rule2.stderr Changes: ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -188,6 +188,40 @@ that it is a no-op. Here's our solution (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`. + +Note [Smart contructor for WpFun] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In `matchExpectedFunTys` (and the moribund `matchActualFunTys`) we use the smart +constructor `mkWpFun` to optimise away a `WpFun`. This is important (T1753b, T15105). +Suppose we have `type instance F Int = Type`, and we are typechecking this: + (\x. True) :: (a :: F Int) -> a +We cannot desugar this to + \(x::a::F Int). True +because then `x` does not have a fixed runtime representation. +See Note [Representation polymorphism invariants] in GHC.Core. + +So we must cast the entire lambda first. We want to end up with + (\(x::(a |> kco). x) |> (FunCo co <Bool>) +where + kco :: F Int ~ Type = ... -- From the type instance + co :: (a |> kco) ~ a = GRefl a kco +Note that we /cast/ the lambda with a /coercion/. We must not +/wrap/ it in a /WpFun/ because the latter generates a lambda that won't obey +the runtime-rep rules. + +The check is done by the `hasFixedRuntimeRep` magic in `matchExpectedFunTys`. + +QUESTIONS: + +* What happens if we can't build a cast? What error is produced, and how? + +* What about mkWpFun (WpCast co) (WpTyLam ...), which might arise from + (a :: F Int -> forall b. b->b) + Will we generate a cast and then a WpFun. Surely we should? + Test case? + +* I think it's really only matchExpectedFunTys that is implicated here. + (Apart from matchActualFunTys.) Anything else? -} -- We write wrap :: t1 ~> t2 @@ -276,20 +310,31 @@ WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1) -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2). c1 <.> c2 = c1 `WpCompose` c2 --- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing --- a lambda abstraction if the two supplied wrappers are either identities or --- casts. --- --- PRECONDITION: either: --- --- 1. both of the 'HsWrapper's are identities or casts, or --- 2. both the "from" and "to" types of the first wrapper have a syntactically --- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete). mkWpFun :: HsWrapper -> HsWrapper -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper -> TcType -- ^ Either "from" type or "to" type of the second wrapper -- (used only when the second wrapper is the identity) -> HsWrapper +-- ^ Smart constructor to create a 'WpFun' 'HsWrapper' +-- See Note [Smart contructor for WpFun] for why we need a smart constructor +-- +-- PRECONDITION: either: +-- +-- 1. Both of the 'HsWrapper's are WpHole or WpCast. +-- In this we optimise away the WpFun entirely +-- OR +-- 2. Both the "from" and "to" types of the first wrapper have a syntactically +-- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete). +-- If we retain the WpFun (i.e. not case 1), it will desugar to a lambda +-- \x. w_res[ e w_arg[x] ] +-- To satisfy Note [Representation polymorphism invariants] in GHC.Core, +-- it must be the case that both the lambda bound variable x and the function +-- argument w_arg[x] have a fixed runtime representation, i.e. that both the +-- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime +-- representation. +-- +-- Unfortunately, we can't check precondition (2) with an assertion here, because of +-- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. mkWpFun w1 w2 st1@(Scaled m1 t1) t2 = case (w1,w2) of (WpHole, WpHole) -> WpHole @@ -297,17 +342,6 @@ mkWpFun w1 w2 st1@(Scaled m1 t1) t2 (WpCast co1, WpHole) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) (mkRepReflCo t2)) (WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) co2) (_, _) -> WpFun w1 w2 st1 t2 - -- In the WpFun case, we will desugar to a lambda - -- - -- \x. w_res[ e w_arg[x] ] - -- - -- To satisfy Note [Representation polymorphism invariants] in GHC.Core, - -- it must be the case that both the lambda bound variable x and the function - -- argument w_arg[x] have a fixed runtime representation, i.e. that both the - -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation. - -- - -- 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 -- See (DSST2) in Note [Deep subsumption and WpSubType] ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -248,6 +248,8 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected -> Arity -> TcSigmaType -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType) +-- NB: Called only from `tcSynArgA`, and hence scheduled for destruction +-- -- If matchActualFunTys n fun_ty = (wrap, [t1,..,tn], res_ty) -- then wrap : fun_ty ~> (t1 -> ... -> tn -> res_ty) -- and res_ty is a RhoType @@ -868,6 +870,7 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside res_ty ; let wrap_arg = mkWpCastN arg_co fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty + -- mkWpFun: see Note [Smart contructor for WpFun] in GHC.Tc.Types.Evidence ; return (fun_wrap, result) } ---------------------------- ===================================== testsuite/tests/simplCore/should_compile/rule2.stderr ===================================== @@ -10,18 +10,15 @@ ==================== Grand total simplifier statistics ==================== -Total ticks: 13 +Total ticks: 11 -2 PreInlineUnconditionally - 1 ds - 1 f +1 PreInlineUnconditionally 1 f 2 UnfoldingDone 1 GHC.Internal.Base.id 1 Roman.bar 1 RuleFired 1 foo/bar 1 LetFloatFromLet 1 -7 BetaReduction - 1 ds +6 BetaReduction 1 f 1 a 1 m View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/076f9021e43c04f875ae48f735ad9dc7... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/076f9021e43c04f875ae48f735ad9dc7... You're receiving this email because of your account on gitlab.haskell.org.