[Git][ghc/ghc][wip/T23025] linear lint: Add missing processing of DEFAULT

[Krzysztof Gogolewski (@monoidal)]

Krzysztof Gogolewski pushed to branch wip/T23025 at Glasgow Haskell Compiler / GHC


Commits:
eda0d0da by Krzysztof Gogolewski at 2023-05-10T16:16:58+02:00
linear lint: Add missing processing of DEFAULT

In this correct program

f :: a %1 -> a
f x = case x of x { _DEFAULT -> x }

after checking the alternative we weren't popping the case binder 'x'
from the usage environment, which meant that the lambda-bound 'x'
was counted twice: in the scrutinee and (incorrectly) in the alternative.
In fact, we weren't checking the usage of 'x' at all.
Now the code for handling _DEFAULT is similar to the one handling
data constructors.

Fixes #23025.

- - - - -


4 changed files:

- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/UsageEnv.hs
- + testsuite/tests/linear/should_compile/T23025.hs
- testsuite/tests/linear/should_compile/all.T


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1195,13 +1195,13 @@ checkCanEtaExpand _ _ _
 checkLinearity :: UsageEnv -> Var -> LintM UsageEnv
 checkLinearity body_ue lam_var =
   case varMultMaybe lam_var of
-    Just mult -> do ensureSubUsage lhs mult (err_msg mult)
-                    return $ deleteUE body_ue lam_var
+    Just mult -> do
+      let (lhs, body_ue') = popUE body_ue lam_var
+          err_msg = text "Linearity failure in lambda:" <+> ppr lam_var
+                    $$ ppr lhs <+> text "⊈" <+> ppr mult
+      ensureSubUsage lhs mult err_msg
+      return body_ue'
     Nothing    -> return body_ue -- A type variable
-  where
-    lhs = lookupUE body_ue lam_var
-    err_msg mult = text "Linearity failure in lambda:" <+> ppr lam_var
-                $$ ppr lhs <+> text "⊈" <+> ppr mult
 
 {- Note [Join points and casts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1552,17 +1552,24 @@ lintCoreAlt :: Var              -- Case binder
             -> LintM UsageEnv
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoreAlt _ _ _ alt_ty (Alt DEFAULT args rhs) =
+lintCoreAlt case_bndr _ scrut_mult alt_ty (Alt DEFAULT args rhs) =
   do { lintL (null args) (mkDefaultArgsMsg args)
-     ; lintAltExpr rhs alt_ty }
-
-lintCoreAlt _case_bndr scrut_ty _ alt_ty (Alt (LitAlt lit) args rhs)
+     ; rhs_ue <- lintAltExpr rhs alt_ty
+     ; let (case_bndr_usage, rhs_ue') = popUE rhs_ue case_bndr
+           err_msg = text "Linearity failure in the DEFAULT clause:" <+> ppr case_bndr
+                     $$ ppr case_bndr_usage <+> text "⊈" <+> ppr scrut_mult
+     ; ensureSubUsage case_bndr_usage scrut_mult err_msg
+     ; return rhs_ue' }
+
+lintCoreAlt case_bndr scrut_ty _ alt_ty (Alt (LitAlt lit) args rhs)
   | litIsLifted lit
   = failWithL integerScrutinisedMsg
   | otherwise
   = do { lintL (null args) (mkDefaultArgsMsg args)
        ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
-       ; lintAltExpr rhs alt_ty }
+       ; rhs_ue <- lintAltExpr rhs alt_ty
+       ; return (deleteUE rhs_ue case_bndr) -- No need for linearity checks
+       }
   where
     lit_ty = literalType lit
 


=====================================
compiler/GHC/Core/UsageEnv.hs
=====================================
@@ -6,6 +6,7 @@ module GHC.Core.UsageEnv
   , bottomUE
   , deleteUE
   , lookupUE
+  , popUE
   , scaleUE
   , scaleUsage
   , supUE
@@ -104,5 +105,8 @@ lookupUE (UsageEnv e has_bottom) x =
     Just w  -> MUsage w
     Nothing -> if has_bottom then Bottom else Zero
 
+popUE :: NamedThing n => UsageEnv -> n -> (Usage, UsageEnv)
+popUE ue x = (lookupUE ue x, deleteUE ue x)
+
 instance Outputable UsageEnv where
   ppr (UsageEnv ne b) = text "UsageEnv:" <+> ppr ne <+> ppr b


=====================================
testsuite/tests/linear/should_compile/T23025.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes, BangPatterns #-}
+module T23025 where
+
+import Data.Void
+
+f :: a %1 -> a
+f !x = x
+
+g :: Void %m -> Maybe ()
+g a = Just (case a of {})


=====================================
testsuite/tests/linear/should_compile/all.T
=====================================
@@ -40,3 +40,4 @@ test('T18731', normal, compile, [''])
 test('T19400', unless(compiler_debugged(), skip), compile, [''])
 test('T20023', normal, compile, [''])
 test('T22546', normal, compile, [''])
+test('T23025', normal, compile, ['-dlinear-core-lint'])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eda0d0da324842d5fed390bc04bbda29cd71cde2
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/20230510/a8340ec9/attachment-0001.html>