Linear Types confusing error message
Summary
When implementing a partition function I tried adding a polymorphic linear type annotation, which gave a very strange error message: "Couldn't match type ‘'Many’ with ‘'Many".
Steps to reproduce
Here is my code:
{-# LANGUAGE LinearTypes #-}
part :: (a -> Bool) -> [a] %p -> ([a], [a])
part _ [] = ([],[])
part f (x : xs)
| f x = (x : l, r)
| otherwise = (l, x : r)
where
~(l, r) = part f xs
This gives the error message:
QS.hs:22:13: error:
• Couldn't match type ‘'Many’ with ‘'Many’
arising from multiplicity of ‘xs’
‘p’ is a rigid type variable bound by
the type signature for:
part :: forall a. (a -> Bool) -> [a] -> ([a], [a])
at QS.hs:20:1-43
• In the pattern: x : xs
In an equation for ‘part’:
part f (x : xs)
| f x = (x : l, r)
| otherwise = (l, x : r)
where
~(l, r) = part f xs
• Relevant bindings include
part :: (a -> Bool) -> [a] -> ([a], [a]) (bound at QS.hs:21:1)
Expected behavior
Compile without errors or with a more sensible error. Why can't Many be matched with Many?
Environment
- GHC version used: 9.0.1