Run linear Lint on the desugarer output (part of #19165)wip/T19165

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

8 files changed, 82 insertions, 19 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 382851a1e5..40de306802 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 665a665cc4..c4e9a3297c 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 425940624b..a007faa823 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 7c452887f1..fbee6b4120 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,
 
@@ -411,6 +412,57 @@ mkErrorAppDs err_id ty msg = do
     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'.
 
 Note [Desugaring seq]
diff --git a/compiler/GHC/Tc/Types/EvTerm.hs b/compiler/GHC/Tc/Types/EvTerm.hs
index d1a0f56531..19afec031a 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 4869db0f2f..17e04ca94a 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 9e3f4184ea..7825071aea 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 a9da295e8b..a8fa8e58e8 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}