[Git][ghc/ghc][master] Don't restrict eta-reduction of linear functions

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
e9496000 by Arnaud Spiwack at 2024-08-14T14:28:20-04:00
Don't restrict eta-reduction of linear functions

This commit simply removes code. All the supporting implementation has
been done as part of !12883.

Closes #25129

- - - - -


2 changed files:

- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -3170,6 +3170,19 @@ examples are documented in the linear-type implementation wiki page
 
     The rule "ex" must match . So the linter must accept `m' f`.
 
+* EXAMPLE 4: eta-reduction
+   Eta-expansion can change linear functions into unrestricted functions
+
+     f :: A %1 -> B
+
+     g :: A %Many -> B
+     g = \x -> f x
+
+   Eta-reduction undoes this and produces:
+
+     g :: A %Many -> B
+     g = f
+
 Historical note: In the original linear-types implementation, we had tried to
 make every optimisation pass produce code that passes `-dlinear-core-lint`. It
 had proved very difficult. We kept finding corner case after corner


=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -2507,14 +2507,6 @@ case where `e` is trivial):
 And here are a few more technical criteria for when it is *not* sound to
 eta-reduce that are specific to Core and GHC:
 
-(L) With linear types, eta-reduction can break type-checking:
-      f :: A ⊸ B
-      g :: A -> B
-      g = \x. f x
-    The above is correct, but eta-reducing g would yield g=f, the linter will
-    complain that g and f don't have the same type. NB: Not unsound in the
-    dynamic semantics, but unsound according to the static semantics of Core.
-
 (J) We may not undersaturate join points.
     See Note [Invariants on join points] in GHC.Core, and #20599.
 
@@ -2774,7 +2766,7 @@ tryEtaReduce rec_ids bndrs body eval_sd
       | fun `elemUnVarSet` rec_ids          -- Criterion (R)
       = False -- Don't eta-reduce in fun in its own recursive RHSs
 
-      | cantEtaReduceFun fun                -- Criteria (L), (J), (W), (B)
+      | cantEtaReduceFun fun                -- Criteria (J), (W), (B)
       = False -- Function can't be eta reduced to arity 0
               -- without violating invariants of Core and GHC
 
@@ -2844,7 +2836,7 @@ tryEtaReduce rec_ids bndrs body eval_sd
     ok_arg _ _ _ _ = Nothing
 
 -- | Can we eta-reduce the given function
--- See Note [Eta reduction soundness], criteria (B), (J), (W) and (L).
+-- See Note [Eta reduction soundness], criteria (B), (J), and (W).
 cantEtaReduceFun :: Id -> Bool
 cantEtaReduceFun fun
   =    hasNoBinding fun -- (B)
@@ -2858,11 +2850,6 @@ cantEtaReduceFun fun
        -- Don't undersaturate StrictWorkerIds.
        -- See Note [CBV Function Ids] in GHC.Types.Id.Info.
 
-    ||  isLinearType (idType fun) -- (L)
-       -- Don't perform eta reduction on linear types.
-       -- If `f :: A %1-> B` and `g :: A -> B`,
-       -- then `g x = f x` is OK but `g = f` is not.
-
 
 {- *********************************************************************
 *                                                                      *



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e9496000ae32e6375c940e9e3c31beaf0ebcca07

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e9496000ae32e6375c940e9e3c31beaf0ebcca07
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240814/19b3d3cb/attachment-0001.html>