diff options
author | Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io> | 2021-07-30 20:23:15 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-08-04 01:33:38 -0400 |
commit | 9b719549fda563fb80b197fb47d9e508c7989d2d (patch) | |
tree | e2677be214d9b81bbd223090eb4d852d83bdc60d | |
parent | 2c714f07f4ab6823de50aaa4947e86326799f44f (diff) | |
download | haskell-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.hs | 34 | ||||
-rw-r--r-- | testsuite/tests/linear/should_compile/all.T | 2 |
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, ['']) |