diff options
| -rw-r--r-- | compiler/GHC/Core/Lint.hs | 37 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_compile/T22546.hs | 12 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_compile/all.T | 1 |
3 files changed, 35 insertions, 15 deletions
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index e299eb9171..e541058cc7 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -3235,22 +3235,29 @@ ensureSubUsage Zero described_mult err_msg = ensureSubMult ManyTy describe ensureSubUsage (MUsage m) described_mult err_msg = ensureSubMult m described_mult err_msg ensureSubMult :: Mult -> Mult -> SDoc -> LintM () -ensureSubMult actual_usage described_usage err_msg = do +ensureSubMult actual_mult described_mult err_msg = do flags <- getLintFlags - when (lf_check_linearity flags) $ case actual_usage' `submult` described_usage' of - Submult -> return () - Unknown -> case isMultMul actual_usage' of - Just (m1, m2) -> ensureSubMult m1 described_usage' err_msg >> - ensureSubMult m2 described_usage' err_msg - Nothing -> when (not (actual_usage' `eqType` described_usage')) (addErrL err_msg) - - where actual_usage' = normalize actual_usage - described_usage' = normalize described_usage - - normalize :: Mult -> Mult - normalize m = case isMultMul m of - Just (m1, m2) -> mkMultMul (normalize m1) (normalize m2) - Nothing -> m + when (lf_check_linearity flags) $ + unless (deepSubMult actual_mult described_mult) $ + addErrL err_msg + where + -- Check for submultiplicity using the following rules: + -- 1. x*y <= z when x <= z and y <= z. + -- This rule follows from the fact that x*y = sup{x,y} for any + -- multiplicities x,y. + -- 2. x <= y*z when x <= y or x <= z. + -- This rule is not complete: when x = y*z, we cannot + -- change y*z <= y*z to y*z <= y or y*z <= z. + -- However, we eliminate products on the LHS in step 1. + -- 3. One <= x and x <= Many for any x, as checked by 'submult'. + -- 4. x <= x. + -- Otherwise, we fail. + deepSubMult :: Mult -> Mult -> Bool + deepSubMult m n + | Just (m1, m2) <- isMultMul m = deepSubMult m1 n && deepSubMult m2 n + | Just (n1, n2) <- isMultMul n = deepSubMult m n1 || deepSubMult m n2 + | Submult <- m `submult` n = True + | otherwise = m `eqType` n lintRole :: Outputable thing => thing -- where the role appeared diff --git a/testsuite/tests/linear/should_compile/T22546.hs b/testsuite/tests/linear/should_compile/T22546.hs new file mode 100644 index 0000000000..c1b2041519 --- /dev/null +++ b/testsuite/tests/linear/should_compile/T22546.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE LinearTypes, GADTSyntax #-} + +module T22546 where + +import GHC.Types (Multiplicity (..)) +import Data.Kind (Type) + +data T :: Multiplicity -> Type where + MkT :: () %m-> T m + +unMkT :: T m %n-> () +unMkT (MkT x) = x diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T index 3b73636071..d0f16080d8 100644 --- a/testsuite/tests/linear/should_compile/all.T +++ b/testsuite/tests/linear/should_compile/all.T @@ -39,3 +39,4 @@ test('LinearDataConSections', normal, compile, ['']) test('T18731', normal, compile, ['']) test('T19400', unless(compiler_debugged(), skip), compile, ['']) test('T20023', normal, compile, ['']) +test('T22546', normal, compile, ['']) |