Linear types: fix linting of multiplicities (#19165)wip/T19165-part2

The previous version did not substitute the type used in the scrutinee.

2 files changed, 21 insertions, 15 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index f20dbcc62b..3b3a7232c0 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1430,10 +1430,10 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh
         -- We've already check
       lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
     ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
-          ; ex_tvs_n = length (dataConExTyCoVars con)
-          -- See Note [Alt arg multiplicities]
-          ; multiplicities = replicate ex_tvs_n Many ++
-                             map scaledMult (dataConRepArgTys con) }
+          ; binderMult (Named _)   = Many
+          ; binderMult (Anon _ st) = scaledMult st
+          -- See Note [Validating multiplicities in a case]
+          ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty }
 
         -- And now bring the new binders into scope
     ; lintBinders CasePatBind args $ \ args' -> do
@@ -1447,6 +1447,22 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh
   | otherwise   -- Scrut-ty is wrong shape
   = zeroUE <$ addErrL (mkBadAltMsg scrut_ty alt)
 
+{-
+Note [Validating multiplicities in a case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose 'MkT :: a %m -> T m a'.
+If we are validating 'case (x :: T Many a) of MkT y -> ...',
+we have to substitute m := Many in the type of MkT - in particular,
+y can be used Many times and that expression would still be linear in x.
+We do this by looking at con_payload_ty, which is the type of the datacon
+applied to the surrounding arguments.
+Testcase: linear/should_compile/MultConstructor
+
+Data constructors containing existential tyvars will then have
+Named binders, which are always multiplicity Many.
+Testcase: indexed-types/should_compile/GADT1
+-}
+
 lintLinearBinder :: SDoc -> Mult -> Mult -> LintM ()
 lintLinearBinder doc actual_usage described_usage
   = ensureSubMult actual_usage described_usage err_msg
@@ -1457,16 +1473,6 @@ lintLinearBinder doc actual_usage described_usage
                 $$ text "Annotation:" <+> ppr described_usage)
 
 {-
-Note [Alt arg multiplicities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It is necessary to use `dataConRepArgTys` so you get the arg tys from
-the wrapper if there is one.
-
-You also need to add the existential ty vars as they are passed are arguments
-but not returned by `dataConRepArgTys`. Without this the test `GADT1` fails.
--}
-
-{-
 ************************************************************************
 *                                                                      *
 \subsection[lint-types]{Types}
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index b9d4215793..49171262e4 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -28,7 +28,7 @@ test('LinearConstructors', normal, compile, [''])
 test('Linear1Rule', normal, compile, [''])
 test('LinearEmptyCase', normal, compile, [''])
 test('Tunboxer', normal, compile, [''])
-test('MultConstructor', expect_broken(19165), compile, [''])
+test('MultConstructor', normal, compile, [''])
 test('LinearLetRec', expect_broken(18694), compile, ['-O -dlinear-core-lint'])
 test('LinearTH1', normal, compile, [''])
 test('LinearTH2', normal, compile, [''])