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

Krzysztof Gogolewski (@monoidal) gitlab at gitlab.haskell.org
Tue May 23 10:29:58 UTC 2023



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


Commits:
b8641ffb by Krzysztof Gogolewski at 2023-05-23T12:29:30+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.

- - - - -


6 changed files:

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


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1194,13 +1194,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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1551,17 +1551,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
 
@@ -3184,9 +3191,14 @@ inCasePat = LintM $ \ env errs -> fromBoxedLResult (Just (is_case_pat env), errs
 
 addInScopeId :: Id -> LintedType -> LintM a -> LintM a
 addInScopeId id linted_ty m
-  = LintM $ \ env@(LE { le_ids = id_set, le_joins = join_set }) errs ->
+  = LintM $ \ env@(LE { le_ids = id_set, le_joins = join_set, le_ue_aliases = aliases }) errs ->
     unLintM m (env { le_ids   = extendVarEnv id_set id (id, linted_ty)
-                   , le_joins = add_joins join_set }) errs
+                   , le_joins = add_joins join_set
+                   , le_ue_aliases = delFromNameEnv aliases (idName id) }) errs
+                   -- When shadowing an alias, we need to make sure the Id is no longer
+                   -- classified as such. E.g. in
+                   -- let x = <e1> in case x of x { _DEFAULT -> <e2> }
+                   -- Occurrences of 'x' in e2 shouldn't count as occurrences of e1.
   where
     add_joins join_set
       | isJoinId id = extendVarSet join_set id -- Overwrite with new arity


=====================================
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


=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -1175,7 +1175,7 @@ desugarRecordUpd record_expr possible_parents rbnds res_ty
        -- e.g. (x', e1), (y', e2), ...
        ; let mk_upd_id :: Name -> LHsFieldBind GhcTc fld (LHsExpr GhcRn) -> TcM (Name, (TcId, LHsExpr GhcRn))
              mk_upd_id fld_nm (L _ rbind)
-               = do { let Scaled m arg_ty = lookupNameEnv_NF arg_ty_env fld_nm
+               = do { let Scaled _ arg_ty = lookupNameEnv_NF arg_ty_env fld_nm
                           nm_occ = rdrNameOcc . nameRdrName $ fld_nm
                           actual_arg_ty = substTy subst arg_ty
                           rhs = hfbRHS rbind
@@ -1186,11 +1186,17 @@ desugarRecordUpd record_expr possible_parents rbnds res_ty
                       -- (As we will typecheck the let-bindings later, we can drop this coercion here.)
                       -- See RepPolyRecordUpdate test.
                     ; nm <- newNameAt nm_occ generatedSrcSpan
-                    ; let id = mkLocalId nm m actual_arg_ty
+                    ; let id = mkLocalId nm ManyTy actual_arg_ty
                       -- NB: create fresh names to avoid any accidental shadowing
                       -- occurring in the RHS expressions when creating the let bindings:
                       --
                       --  let x1 = e1; x2 = e2; ...
+                      --
+                      -- Above, we use multiplicity Many rather than the one associated to arg_ty.
+                      -- Normally, there shouldn't be a difference, since it's a let binding.
+                      -- But -XStrict can convert the let to a case, and this causes issues
+                      -- in test LinearRecUpd. Since we don't support linear record updates,
+                      -- using Many is simple and safe.
                     ; return (fld_nm, (id, rhs))
                     }
              arg_ty_env = mkNameEnv


=====================================
testsuite/tests/linear/should_compile/LinearRecUpd.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE Strict #-}
+module LinearRecUpd where
+
+nextM :: Env -> Env
+nextM e = e{dfsE=0}
+
+data Env = Env {dfsE :: Int}


=====================================
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,5 @@ 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'])
+test('LinearRecUpd', normal, compile, [''])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b8641ffbda26198c73618c8cd0dd64be189a8ae4
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/20230523/5ddadaa7/attachment-0001.html>


More information about the ghc-commits mailing list