From aed356e1b68b2201fa6e3c5bf14079f3f3366b44 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Fri, 13 May 2022 11:24:24 +0100 Subject: Comments only around HsWrapper --- compiler/GHC/HsToCore/Binds.hs | 19 ++++++++++++++++--- compiler/GHC/Tc/Types/Evidence.hs | 15 +++++++++++---- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs index fe7747a4a1..44bb82312f 100644 --- a/compiler/GHC/HsToCore/Binds.hs +++ b/compiler/GHC/HsToCore/Binds.hs @@ -1105,6 +1105,21 @@ So for now, we ban them altogether as requested by #13290. See also #7398. * * ************************************************************************ +Note [Desugaring WpFun] +~~~~~~~~~~~~~~~~~~~~~~~ +See comments on WpFun in GHC.Tc.Types.Evidence for what WpFun means. +Roughly: + + (WpFun w_arg w_res)[ e ] = \x. w_res[ e w_arg[x] ] + +This eta-expansion risk duplicating work, if `e` is not in HNF. +At one stage I thought we could avoid that by desugaring to + let f = e in \x. w_res[ f w_arg[x] ] +But that /fundamentally/ doesn't work, because `w_res` may bind +evidence that is used in `e`. + +This question arose when thinking about deep subsumption; see +https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1125419649). -} dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr) @@ -1117,9 +1132,7 @@ dsHsWrapper (WpLet ev_binds) = do { bs <- dsTcEvBinds ev_binds dsHsWrapper (WpCompose c1 c2) = do { w1 <- dsHsWrapper c1 ; w2 <- dsHsWrapper c2 ; return (w1 . w2) } - -- See comments on WpFun in GHC.Tc.Types.Evidence for an explanation of what - -- the specification of this clause is -dsHsWrapper (WpFun c1 c2 (Scaled w t1)) +dsHsWrapper (WpFun c1 c2 (Scaled w t1)) -- See Note [Desugaring WpFun] = do { x <- newSysLocalDs w t1 ; w1 <- dsHsWrapper c1 ; w2 <- dsHsWrapper c2 diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 837903a0f7..dfe332eb08 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -221,6 +221,8 @@ maybeTcSymCo NotSwapped co = co ************************************************************************ -} +-- We write wrap :: t1 ~> t2 +-- if wrap[ e::t1 ] :: t2 data HsWrapper = WpHole -- The identity coercion @@ -229,12 +231,17 @@ data HsWrapper -- -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) + -- + -- If wrap1 :: t2 ~> t3 + -- wrap2 :: t1 ~> t2 + --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3 | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) - -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ] - -- So note that if wrap1 :: exp_arg <= act_arg - -- wrap2 :: act_res <= exp_res - -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) + -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ] + -- So note that if e :: act_arg -> act_res + -- wrap1 :: exp_arg ~> act_arg + -- wrap2 :: act_res ~> exp_res + -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res) -- This isn't the same as for mkFunCo, but it has to be this way -- because we can't use 'sym' to flip around these HsWrappers -- The TcType is the "from" type of the first wrapper -- cgit v1.2.1