From 4cd98bd2c91cac4a10831ab7111c7be8153bdd33 Mon Sep 17 00:00:00 2001
From: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
Date: Fri, 26 Feb 2021 14:51:59 +0100
Subject: [PATCH] Run linear Lint on the desugarer output (part of #19165)
This addresses points (1a) and (1b) of #19165.
- Move mkFailExpr to HsToCore/Utils, as it can be shared
- Desugar incomplete patterns and holes to an empty case,
as in Note [Incompleteness and linearity]
- Enable linear linting of desugarer output
- Mark MultConstructor as broken. It fails Lint, but I'd like to fix this
separately.
Metric Decrease:
T6048
---
compiler/GHC/Core/Lint.hs | 16 ++++--
compiler/GHC/HsToCore/Arrows.hs | 4 --
compiler/GHC/HsToCore/Match.hs | 5 +-
compiler/GHC/HsToCore/Utils.hs | 52 +++++++++++++++++++
compiler/GHC/Tc/Types/EvTerm.hs | 7 ++-
testsuite/tests/linear/should_compile/all.T | 2 +-
.../simplCore/should_compile/T9400.stderr | 10 ++--
.../should_compile/spec-inline.stderr | 5 +-
8 files changed, 82 insertions(+), 19 deletions(-)
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 382851a1e55f..40de30680205 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -488,7 +488,8 @@ lintCoreBindings dflags pass local_in_scope binds
flags = (defaultLintFlags dflags)
{ lf_check_global_ids = check_globals
, lf_check_inline_loop_breakers = check_lbs
- , lf_check_static_ptrs = check_static_ptrs }
+ , lf_check_static_ptrs = check_static_ptrs
+ , lf_check_linearity = check_linearity }
-- See Note [Checking for global Ids]
check_globals = case pass of
@@ -510,6 +511,12 @@ lintCoreBindings dflags pass local_in_scope binds
CorePrep -> AllowAtTopLevel
_ -> AllowAnywhere
+ -- See Note [Linting linearity]
+ check_linearity = gopt Opt_DoLinearCoreLinting dflags || (
+ case pass of
+ CoreDesugar -> True
+ _ -> False)
+
(_, dups) = removeDups compare binders
-- dups_ext checks for names with different uniques
@@ -2641,11 +2648,12 @@ to work with Linear Lint:
in f True
uses 'x' linearly, but this is not seen by the linter.
Plan: make let-bound variables remember the usage environment.
- See test LinearLetRec and https://github.com/tweag/ghc/issues/405.
+ See ticket #18694.
We plan to fix both of the issues in the very near future.
-For now, linear Lint is disabled by default and
-has to be enabled manually with -dlinear-core-lint.
+For now, -dcore-lint enables only linting output of the desugarer,
+and full Linear Lint has to be enabled separately with -dlinear-core-lint.
+Ticket #19165 concerns enabling Linear Lint with -dcore-lint.
-}
instance Applicative LintM where
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 665a665cc4a7..c4e9a3297c52 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -166,10 +166,6 @@ do_premap :: DsCmdEnv -> Type -> Type -> Type ->
do_premap ids b_ty c_ty d_ty f g
= do_compose ids b_ty c_ty d_ty (do_arr ids b_ty c_ty f) g
-mkFailExpr :: HsMatchContext GhcRn -> Type -> DsM CoreExpr
-mkFailExpr ctxt ty
- = mkErrorAppDs pAT_ERROR_ID ty (matchContextErrString ctxt)
-
-- construct CoreExpr for \ (a :: a_ty, b :: b_ty) -> a
mkFstExpr :: Type -> Type -> DsM CoreExpr
mkFstExpr a_ty b_ty = do
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 425940624b79..a007faa8236b 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -812,11 +812,10 @@ matchEquations :: HsMatchContext GhcRn
-> [MatchId] -> [EquationInfo] -> Type
-> DsM CoreExpr
matchEquations ctxt vars eqns_info rhs_ty
- = do { let error_doc = matchContextErrString ctxt
+ = do { match_result <- match vars rhs_ty eqns_info
- ; match_result <- match vars rhs_ty eqns_info
+ ; fail_expr <- mkFailExpr ctxt rhs_ty
- ; fail_expr <- mkErrorAppDs pAT_ERROR_ID rhs_ty error_doc
; extractMatchResult match_result fail_expr }
-- | @matchSimply@ is a wrapper for 'match' which deals with the
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index 7c452887f1e9..fbee6b412025 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -30,6 +30,7 @@ module GHC.HsToCore.Utils (
wrapBind, wrapBinds,
mkErrorAppDs, mkCoreAppDs, mkCoreAppsDs, mkCastDs,
+ mkFailExpr,
seqVar,
@@ -410,6 +411,57 @@ mkErrorAppDs err_id ty msg = do
-- mkLitString returns a result of type String#
return (mkApps (Var err_id) [Type (getRuntimeRep ty), Type ty, core_msg])
+{-
+Note [Incompleteness and linearity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The default branch of an incomplete pattern match is compiled to a call
+to 'error'.
+Because of linearity, we wrap it with an empty case. Example:
+
+f :: a %1 -> Bool -> a
+f x True = False
+
+Adding 'f x False = error "Non-exhaustive pattern..."' would violate
+the linearity of x.
+Instead, we use 'f x False = case error "Non-exhausive pattern..." :: () of {}'.
+This case expression accounts for linear variables by assigning bottom usage
+(See Note [Bottom as a usage] in GHC.Core.Multiplicity).
+This is done in mkFailExpr.
+We use '()' instead of the original return type ('a' in this case)
+because there might be levity polymorphism, e.g. in
+
+g :: forall (a :: TYPE r). (() -> a) %1 -> Bool -> a
+g x True = x ()
+
+adding 'g x False = case error "Non-exhaustive pattern" :: a of {}'
+would create an illegal levity-polymorphic case binder.
+This is important for pattern synonym matchers, which often look like this 'g'.
+
+Similarly, a hole
+h :: a %1 -> a
+h x = _
+is desugared to 'case error "Hole" :: () of {}'. Test: LinearHole.
+
+Instead of () we could use Data.Void.Void, but that would require
+moving Void to GHC.Types: partial pattern matching is used in modules
+that are compiled before Data.Void.
+We can use () even though it has a constructor, because
+Note [Case expression invariants] point 4 in GHC.Core is satisfied
+when the scrutinee is bottoming.
+
+You might wonder if this change slows down compilation, but the
+performance testsuite did not show up any regressions.
+
+For uniformity, calls to 'error' in both cases are wrapped even if -XLinearTypes
+is disabled.
+-}
+
+mkFailExpr :: HsMatchContext GhcRn -> Type -> DsM CoreExpr
+mkFailExpr ctxt ty
+ = do fail_expr <- mkErrorAppDs pAT_ERROR_ID unitTy (matchContextErrString ctxt)
+ return $ mkWildCase fail_expr (unrestricted unitTy) ty []
+ -- See Note [Incompleteness and linearity]
+
{-
'mkCoreAppDs' and 'mkCoreAppsDs' handle the special-case desugaring of 'seq'.
diff --git a/compiler/GHC/Tc/Types/EvTerm.hs b/compiler/GHC/Tc/Types/EvTerm.hs
index d1a0f56531c0..19afec031add 100644
--- a/compiler/GHC/Tc/Types/EvTerm.hs
+++ b/compiler/GHC/Tc/Types/EvTerm.hs
@@ -13,6 +13,7 @@ import GHC.Tc.Types.Evidence
import GHC.Unit
import GHC.Builtin.Names
+import GHC.Builtin.Types ( liftedRepTy, unitTy )
import GHC.Core.Type
import GHC.Core
@@ -32,7 +33,11 @@ import GHC.Data.FastString
evDelayedError :: Type -> FastString -> EvTerm
evDelayedError ty msg
= EvExpr $
- Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
+ let fail_expr = Var errorId `mkTyApps` [liftedRepTy, unitTy] `mkApps` [litMsg]
+ in mkWildCase fail_expr (unrestricted unitTy) ty []
+ -- See Note [Incompleteness and linearity] in GHC.HsToCore.Utils
+ -- c.f. mkFailExpr in GHC.HsToCore.Utils
+
where
errorId = tYPE_ERROR_ID
litMsg = Lit (LitString (bytesFS msg))
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index 4869db0f2f35..17e04ca94ac6 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -29,7 +29,7 @@ test('LinearConstructors', normal, compile, [''])
test('Linear1Rule', normal, compile, [''])
test('LinearEmptyCase', normal, compile, [''])
test('Tunboxer', normal, compile, [''])
-test('MultConstructor', normal, compile, [''])
+test('MultConstructor', expect_broken(19165), compile, [''])
test('LinearLetRec', expect_broken(405), compile, ['-O -dlinear-core-lint'])
test('LinearTH1', normal, compile, [''])
test('LinearTH2', normal, compile, [''])
diff --git a/testsuite/tests/simplCore/should_compile/T9400.stderr b/testsuite/tests/simplCore/should_compile/T9400.stderr
index 9e3f4184eaaa..7825071aea67 100644
--- a/testsuite/tests/simplCore/should_compile/T9400.stderr
+++ b/testsuite/tests/simplCore/should_compile/T9400.stderr
@@ -9,7 +9,7 @@ T9400.hs:18:9: warning: [-Woverlapping-patterns (in -Wdefault)]
==================== Tidy Core ====================
Result size of Tidy Core
- = {terms: 37, types: 22, coercions: 0, joins: 0/0}
+ = {terms: 38, types: 22, coercions: 0, joins: 0/0}
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule1 :: Addr#
@@ -36,7 +36,7 @@ T9400.$trModule :: Module
[GblId, Unf=OtherCon []]
T9400.$trModule = GHC.Types.Module $trModule2 $trModule4
--- RHS size: {terms: 22, types: 15, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 23, types: 15, coercions: 0, joins: 0/0}
main :: IO ()
[GblId]
main
@@ -64,8 +64,10 @@ main
@()
@()
(putStrLn (unpackCString# "efg"#))
- (Control.Exception.Base.patError
- @'LiftedRep @(IO ()) "T9400.hs:(17,5)-(18,29)|case"#))))
+ (case Control.Exception.Base.patError
+ @'LiftedRep @() "T9400.hs:(17,5)-(18,29)|case"#
+ of wild {
+ }))))
diff --git a/testsuite/tests/simplCore/should_compile/spec-inline.stderr b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
index a9da295e8b91..a8fa8e58e84e 100644
--- a/testsuite/tests/simplCore/should_compile/spec-inline.stderr
+++ b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
@@ -45,10 +45,11 @@ lvl :: GHC.Prim.Addr#
lvl = "spec-inline.hs:(19,5)-(29,25)|function go"#
-- RHS size: {terms: 2, types: 2, coercions: 0, joins: 0/0}
-Roman.foo3 :: Int
+Roman.foo3 :: ()
[GblId, Str=b, Cpr=b]
Roman.foo3
- = Control.Exception.Base.patError @'GHC.Types.LiftedRep @Int lvl
+ = Control.Exception.Base.patError
+ @'GHC.Types.LiftedRep @() lvl
Rec {
-- RHS size: {terms: 40, types: 5, coercions: 0, joins: 0/0}
--
GitLab