Fix linearity checking in Lintwip/T22546

Lint was not able to see that x*y <= x*y, because this inequality
was decomposed to x <= x*y && y <= x*y, but there was no rule
to see that x <= x*y.

Fixes #22546.

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, [''])