[Git][ghc/ghc][wip/T23814] Fix MultiWayIf linearity checking (#23814)

[Krzysztof Gogolewski (@monoidal)]

Krzysztof Gogolewski pushed to branch wip/T23814 at Glasgow Haskell Compiler / GHC


Commits:
be1e506d by Krzysztof Gogolewski at 2023-08-22T12:59:13+02:00
Fix MultiWayIf linearity checking (#23814)

Co-authored-by: Thomas BAGREL <thomas.bagrel at tweag.io>

- - - - -


6 changed files:

- compiler/GHC/Tc/Gen/Expr.hs
- + testsuite/tests/linear/should_compile/T23814.hs
- testsuite/tests/linear/should_compile/all.T
- + testsuite/tests/linear/should_fail/T23814fail.hs
- + testsuite/tests/linear/should_fail/T23814fail.stderr
- testsuite/tests/linear/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -396,9 +396,34 @@ tcExpr (HsIf x pred b1 b2) res_ty
        ; tcEmitBindingUsage (supUE u1 u2)
        ; return (HsIf x pred' b1' b2') }
 
+{-
+Note [MultiWayIf linearity checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we'd like to compute the usage environment for
+
+if | b1 -> e1
+   | b2 -> e2
+   | otherwise -> e3
+
+and let u1, u2, v1, v2, v3 denote the usage env for b1, b2, e1, e2, e3
+respectively.
+
+Since a multi-way if is mere sugar for nested if expressions, the usage
+environment should ideally be u1 + sup(v1, u2 + sup(v2, v3)).
+However, currently we don't support linear guards (#19193). All variables
+used in guards from u1 and u2 will have multiplicity Many.
+But in that case, we have equality u1 + sup(x,y) = sup(u1 + x, y),
+                      and likewise u2 + sup(x,y) = sup(u2 + x, y) for any x,y.
+Using this identity, we can just compute sup(u1 + v1, u2 + v2, v3) instead.
+This is simple to do, since we get u_i + v_i directly from tcGRHS.
+If we add linear guards, this code will have to be revisited.
+Not using 'sup' caused #23814.
+-}
+
 tcExpr (HsMultiIf _ alts) res_ty
-  = do { alts' <- mapM (wrapLocMA $ tcGRHS match_ctxt res_ty) alts
+  = do { (ues, alts') <- mapAndUnzipM (\alt -> tcCollectingUsage $ wrapLocMA (tcGRHS match_ctxt res_ty) alt) alts
        ; res_ty <- readExpType res_ty
+       ; tcEmitBindingUsage (supUEs ues)  -- See Note [MultiWayIf linearity checking]
        ; return (HsMultiIf res_ty alts') }
   where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
 


=====================================
testsuite/tests/linear/should_compile/T23814.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE MultiWayIf #-}
+
+module T23814 where
+
+f :: Bool -> Int %1 -> Int
+f b x =
+  if
+    | b -> x
+    | otherwise -> x
+
+g :: Bool -> Bool -> Int %1 -> Int %1 -> (Int, Int)
+g b c x y =
+  if
+    | b -> (x,y)
+    | c -> (y,x)
+    | otherwise -> (x,y)


=====================================
testsuite/tests/linear/should_compile/all.T
=====================================
@@ -42,3 +42,4 @@ test('T20023', normal, compile, [''])
 test('T22546', normal, compile, [''])
 test('T23025', normal, compile, ['-dlinear-core-lint'])
 test('LinearRecUpd', normal, compile, [''])
+test('T23814', normal, compile, [''])


=====================================
testsuite/tests/linear/should_fail/T23814fail.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE MultiWayIf #-}
+
+module T23814fail where
+
+f' :: Bool -> Int %1 -> Int
+f' b x =
+  if
+    | b -> x
+    | otherwise -> 0
+
+g' :: Bool -> Bool -> Int %1 -> Int
+g' b c x =
+   if
+     | b -> x
+     | c -> 0
+     | otherwise -> 0


=====================================
testsuite/tests/linear/should_fail/T23814fail.stderr
=====================================
@@ -0,0 +1,17 @@
+
+T23814fail.hs:7:6: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f'’:
+          f' b x
+            = if | b -> x
+                 | otherwise -> 0
+
+T23814fail.hs:13:8: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘g'’:
+          g' b c x
+            = if | b -> x
+                 | c -> 0
+                 | otherwise -> 0


=====================================
testsuite/tests/linear/should_fail/all.T
=====================================
@@ -41,3 +41,4 @@ test('T19120', normal, compile_fail, [''])
 test('T20083', normal, compile_fail, ['-XLinearTypes'])
 test('T19361', normal, compile_fail, [''])
 test('T21278', normal, compile_fail, ['-XLinearTypes'])
+test('T23814fail', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be1e506dec368e1b9f706f96a882c144abdbbcb6

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be1e506dec368e1b9f706f96a882c144abdbbcb6
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230822/2aca52d3/attachment-0001.html>