Lazy pattern matches not inferred as linear
Summary
I noticed that linearbase
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: [GHC18872]
• 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: