Infer multiplicity in case expressions

This is a first step towards #18738.

3 files changed, 7 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index dfb9d6abd9..dc0d244fc1 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -372,9 +372,7 @@ tcExpr (HsCase x scrut matches) res_ty
            --
            -- But now, in the GADT world, we need to typecheck the scrutinee
            -- first, to get type info that may be refined in the case alternatives
-          let mult = Many
-            -- There is not yet syntax or inference mechanism for case
-            -- expressions to be anything else than unrestricted.
+          mult <- newFlexiTyVarTy multiplicityTy
 
           -- Typecheck the scrutinee.  We use tcInferRho but tcInferSigma
           -- would also be possible (tcMatchesCase accepts sigma-types)
diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
index a989d3b610..30c7968854 100644
--- a/docs/users_guide/exts/linear_types.rst
+++ b/docs/users_guide/exts/linear_types.rst
@@ -153,8 +153,10 @@ missing pieces.
   have success using it, or you may not. Expect it to be really unreliable.
 - There is currently no support for multiplicity annotations such as
   ``x :: a %p``, ``\(x :: a %p) -> ...``.
-- All ``case`` expressions consume their scrutinee ``Many`` times.
-  All ``let`` and ``where`` statements consume their right hand side
+- A ``case`` expression may consume its scrutinee ``One`` time,
+  or ``Many`` times. But the inference is still experimental, and may
+  over-eagerly guess that it ought to consume the scrutinee ``Many`` times.
+- All ``let`` and ``where`` statements consume their right hand side
   ``Many`` times. That is, the following will not type check:
 
   ::
@@ -164,8 +166,7 @@ missing pieces.
 
       f :: A %1 -> C
       f x =
-        case g x of
-          (y, z) -> h y z
+        let (y, z) = g x in h y z
 
   This can be worked around by defining extra functions which are
   specified to be linear, such as:
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index fd44aef367..4869db0f2f 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -20,7 +20,7 @@ test('Linear14', normal, compile, [''])
 test('Linear15', normal, compile, [''])
 test('Linear16', normal, compile, [''])
 test('Linear3', normal, compile, [''])
-test('Linear4', expect_broken(20), compile, [''])
+test('Linear4', normal, compile, [''])
 test('Linear6', normal, compile, [''])
 test('Linear8', normal, compile, [''])
 test('LinearGuards', normal, compile, [''])