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:

1. The pattern match binds at least one variable.
2. Each of the variables bound in the pattern is used exactly once.

Environment

• GHC version used: 9.6.1

Optional:

• Operating System:
• System Architecture: