Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: f108a972 by Arnaud Spiwack at 2026-02-27T12:53:01-05:00 Make list comprehension completely non-linear Fixes #25081 From the note: The usefulness of list comprehension in conjunction with linear types is dubious. After all, statements are made to be run many times, for instance in ```haskell [u | y <- [0,1], stmts] ``` both `u` and `stmts` are going to be run several times. In principle, though, there are some position in a monad comprehension expression which could be considered linear. We could try and make it so that these positions are considered linear by the typechecker, but in practice the desugarer doesn't take enough care to ensure that these are indeed desugared to linear sites. We tried in the past, and it turned out that we'd miss a desugaring corner case (#25772). Until there's a demand for this very specific improvement, let's instead be conservative, and consider list comprehension to be completely non-linear. - - - - - 5 changed files: - compiler/GHC/Tc/Gen/Match.hs - − testsuite/tests/linear/should_compile/LinearListComprehension.hs - testsuite/tests/linear/should_compile/all.T - testsuite/tests/linear/should_fail/T25081.hs - testsuite/tests/linear/should_fail/T25081.stderr Changes: ===================================== compiler/GHC/Tc/Gen/Match.hs ===================================== @@ -543,9 +543,29 @@ tcGuardStmt _ stmt _ _ -- potential for non-trivial coercions in tcMcStmt {- -Note [Binding in list comprehension isn't linear] +Note [List comprehension isn't linear] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In principle, [ y | () <- xs, y <- [0,1]] could be linear in `xs`. +The usefulness of list comprehension in conjunction with linear types is dubious. +After all, statements are made to be run many times, for instance in + +[u | y <- [0,1], stmts] + +both u and stmts are going to be run several times. + +In principle, though, there are some positions in a monad comprehension +expressions which could be considered linear. We could try and make it so that +these positions are considered linear by the typechecker, but in practice the +desugarer doesn't take enough care to ensure that these are indeed desugared to +linear sites. We tried in the past, and it turned out that we'd miss a +desugaring corner case (#25772). + +Until there's a demand for this very specific improvement, let's instead be +conservative, and consider list comprehension to be completely non-linear. + +Here are the case where list comprehension could be linear, together with the +known challenges. + +(LCL1) [ y | () <- xs, y <- [0,1]] could be linear in `xs`. But, the way the desugaring works, we get something like case xs of @@ -566,21 +586,31 @@ isn't linear in `xs` since the elements of `xs` are ignored. So we'd still have to call `tcScalingUsage` on `xs` in `tcLcStmt`, we'd just have to create a fresh multiplicity variable. We'd also use the same multiplicity variable in the call to `tcCheckPat` instead of `unrestricted`. + +(LCL2) [ y | b, y <- [0,1]] could be linear in `b`. This actually works fine +with -O0 (as far as anybody knows), but -O and higher desugar list comprehension +using the `build` combinator (this was the cause of #25772). But `build` isn't +defined to be linear. The consequences of making `build` linear are +unknown. It's not worth trying until a real need arises. + +(LCL3) [ x | ] could be linear in x. But it's unclear why anybody would want to +write this instead of [ x ]. Besides, this syntax is currently rejected by the +parser. The `build` obstacle of (LCL2) applies here too. -} tcLcStmt :: TyCon -- The list type constructor ([]) -> TcExprStmtChecker tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside - = do { body' <- tcMonoExprNC body elt_ty + = do { -- see (LCL3) in Note [List comprehension isn't linear] + body' <- tcScalingUsage ManyTy $ tcMonoExprNC body elt_ty ; thing <- thing_inside (panic "tcLcStmt: thing_inside") ; return (LastStmt x body' noret noSyntaxExpr, thing) } -- A generator, pat <- rhs tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside = do { pat_ty <- newFlexiTyVarTy liftedTypeKind - -- About the next `tcScalingUsage ManyTy` and unrestricted - -- see Note [Binding in list comprehension isn't linear] + -- see (LCL1) in Note [List comprehension isn't linear] ; rhs' <- tcScalingUsage ManyTy $ tcCheckMonoExpr rhs (mkTyConApp m_tc [pat_ty]) ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $ tcScalingUsage ManyTy $ @@ -589,7 +619,9 @@ tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside -- A boolean guard tcLcStmt _ _ (BodyStmt _ rhs _ _) elt_ty thing_inside - = do { rhs' <- tcCheckMonoExpr rhs boolTy + = do { -- Regarding the `tcScalingUsage ManyTy` on the `rhs`, + -- see (LCL2) in Note [List comprehension isn't linear] + rhs' <- tcScalingUsage ManyTy $ tcCheckMonoExpr rhs boolTy ; thing <- tcScalingUsage ManyTy $ thing_inside elt_ty ; return (BodyStmt boolTy rhs' noSyntaxExpr noSyntaxExpr, thing) } ===================================== testsuite/tests/linear/should_compile/LinearListComprehension.hs deleted ===================================== @@ -1,14 +0,0 @@ -{-# LANGUAGE LinearTypes #-} - -module LinearListComprehension where - --- Probably nobody actually cares if monad comprehension realised that it can be --- linear in the first statement. But it can, so we might as well. - -guard :: a %1 -> (a %1 -> Bool) %1 -> [Int] -guard x g = [ y | g x, y <- [0,1] ] - --- This isn't correct syntax, but a singleton list comprehension would --- presumably work too --- last :: a %1 -> [a] --- last x = [ x | ] ===================================== testsuite/tests/linear/should_compile/all.T ===================================== @@ -47,7 +47,6 @@ test('LinearRecUpd', normal, compile, ['']) test('T23814', normal, compile, ['']) test('LinearLet', normal, compile, ['']) test('LinearLetPoly', normal, compile, ['']) -test('LinearListComprehension', normal, compile, ['-dlinear-core-lint']) test('OmitFieldPat', normal, compile, ['-dcore-lint']) test('T25515', normal, compile, ['-dcore-lint']) test('T25428', normal, compile, ['']) ===================================== testsuite/tests/linear/should_fail/T25081.hs ===================================== @@ -22,11 +22,16 @@ guard_bind x = [ () | False, _ <- [x]] guard_guard :: a %1 -> (a %1 -> Bool) %1 -> [()] guard_guard x g = [ () | False, g x ] --- This could, in principle, be linear. But see Note [Binding in list +-- This could, in principle, be linear. But see (LCL1) in Note [List -- comprehension isn't linear] in GHC.Tc.Gen.Match. first_bind :: [()] %1 -> [Int] first_bind xs = [ y | () <- xs, y <- [0,1]] +-- This could, in principle, be linear. But see (LCL2) in Note [List +-- comprehension isn't linear] in GHC.Tc.Gen.Match. +first_guard :: a %1 -> (a %1 -> Bool) %1 -> [Int] +first_guard x g = [ y | g x, y <- [0,1] ] + parallel :: a %1 -> [(a, Bool)] parallel x = [(y,z) | y <- [x] | z <- [True]] ===================================== testsuite/tests/linear/should_fail/T25081.stderr ===================================== @@ -44,20 +44,32 @@ T25081.hs:28:12: error: [GHC-18872] • In an equation for ‘first_bind’: first_bind xs = [y | () <- xs, y <- [0, 1]] -T25081.hs:31:10: error: [GHC-18872] +T25081.hs:33:13: error: [GHC-18872] + • Couldn't match type ‘Many’ with ‘One’ + arising from multiplicity of ‘x’ + • In an equation for ‘first_guard’: + first_guard x g = [y | g x, y <- [0, 1]] + +T25081.hs:33:15: error: [GHC-18872] + • Couldn't match type ‘Many’ with ‘One’ + arising from multiplicity of ‘g’ + • In an equation for ‘first_guard’: + first_guard x g = [y | g x, y <- [0, 1]] + +T25081.hs:36:10: error: [GHC-18872] • Couldn't match type ‘Many’ with ‘One’ arising from multiplicity of ‘x’ • In an equation for ‘parallel’: parallel x = [(y, z) | y <- [x] | z <- [True]] -T25081.hs:34:16: error: [GHC-18872] +T25081.hs:39:16: error: [GHC-18872] • Couldn't match type ‘Many’ with ‘One’ arising from multiplicity of ‘x’ • In an equation for ‘parallel_guard’: parallel_guard x g = [(y, z) | g x, y <- [0, 1] | z <- [True, False]] -T25081.hs:37:11: error: [GHC-18872] +T25081.hs:42:11: error: [GHC-18872] • Couldn't match type ‘Many’ with ‘One’ arising from multiplicity of ‘x’ • In an equation for ‘transform’: View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f108a9722b8ff80d2462fb6835a3944f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f108a9722b8ff80d2462fb6835a3944f... You're receiving this email because of your account on gitlab.haskell.org.