GitLab

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