summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKrzysztof Gogolewski <krzysztof.gogolewski@tweag.io>2021-07-30 20:23:15 +0200
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-08-04 01:33:38 -0400
commit9b719549fda563fb80b197fb47d9e508c7989d2d (patch)
treee2677be214d9b81bbd223090eb4d852d83bdc60d
parent2c714f07f4ab6823de50aaa4947e86326799f44f (diff)
downloadhaskell-9b719549fda563fb80b197fb47d9e508c7989d2d.tar.gz
Linear types: fix linting of multiplicities (#19165)
The previous version did not substitute the type used in the scrutinee.
-rw-r--r--compiler/GHC/Core/Lint.hs34
-rw-r--r--testsuite/tests/linear/should_compile/all.T2
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, [''])