diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2022-05-13 11:24:24 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2022-05-13 17:39:43 +0100 |
| commit | 857654c08e06da97141e5632bf021086010c901a (patch) | |
| tree | a9d7aaf7297295d7dc0c6367b4bdcaa82e4fb6bb | |
| parent | 3bf938b6c5e1190f3a55e149deaec2f6309d398f (diff) | |
| download | haskell-wip/spj-wibbles.tar.gz | |
Comments only around HsWrapperwip/spj-wibbles
| -rw-r--r-- | compiler/GHC/HsToCore/Binds.hs | 19 | ||||
| -rw-r--r-- | 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 c6c0c7b0ca..886a4655a9 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -219,6 +219,8 @@ maybeTcSymCo NotSwapped co = co ************************************************************************ -} +-- We write wrap :: t1 ~> t2 +-- if wrap[ e::t1 ] :: t2 data HsWrapper = WpHole -- The identity coercion @@ -227,12 +229,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 |