Lazy pattern matches not inferred as linear
Summary
I noticed that linear-base
defines
splitAt :: Int -> [a] %1 -> ([a], [a])
splitAt i = Unsafe.toLinear (Prelude.splitAt i)
Is that just for convenience? No! The usual lazy splitAt
will not compile with a linear type. My belief is that it should.
Steps to reproduce
Copy the definition of Data.List.splitAt
, and give it (and its helper) linear types.
splitAt :: Int -> [a] %1-> ([a], [a])
splitAt n ls
| n <= 0 = ([], ls)
| otherwise = splitAt' n ls
where
splitAt' :: Int -> [a] %1-> ([a], [a])
splitAt' _ [] = ([], [])
splitAt' 1 (x:xs) = ([x], xs)
splitAt' m (x:xs) = (x:xs', xs'')
where
(xs', xs'') = splitAt' (m - 1) xs
This gives an error,
src/Data/ScheduledQueue/Linear.hs:56:24: error: [GHC-18872]
• Couldn't match type ‘Many’ with ‘One’
arising from multiplicity of ‘xs’
• In the pattern: x : xs
In an equation for ‘splitAt'’:
splitAt' m (x : xs)
= (x : xs', xs'')
where
(xs', xs'') = splitAt' (m - 1) xs
In an equation for ‘splitAt’:
splitAt n ls
| n <= 0 = ([], ls)
| otherwise = splitAt' n ls
where
splitAt' :: Int -> [a] %1 -> ([a], [a])
splitAt' _ [] = ([], [])
splitAt' 1 (x : xs) = ([x], xs)
splitAt' m (x : xs)
= (x : xs', xs'')
where
(xs', xs'') = splitAt' (m - 1) xs
|
56 | splitAt' m (x:xs) = (x:xs', xs'')
It's angry about the lazy pattern match in the where
(though there's also a less serious issue causing the code to be rejected if that pattern match is banged).
Expected behavior
I expect the code to be accepted. Specifically, I expect the linearity checker to consider a value matched lazily to be used exactly once if and only if both of the following hold:
- The pattern match binds at least one variable.
- Each of the variables bound in the pattern is used exactly once.
Environment
- GHC version used: 9.6.1
Optional:
- Operating System:
- System Architecture: