Why doesn't GHC recognize the function as linear?

I have a very simple snippet:

{-# LANGUAGE LinearTypes #-}

module Lib where

data Peer st = Peer { data :: String } deriving Show

data Idle
data Busy

sendToPeer :: Peer Idle %1-> Int -> IO (Peer Busy)
sendToPeer c n = case c of Peer d -> pure $ Peer d

I am on resolver: ghc-9.0.1.

From the documentation:

A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once. Intuitively, it means that in every branch of the definition of f, its argument x must be used exactly once. Which can be done by

Returning x unmodified

Passing x to a linear function

Pattern-matching on x and using each argument exactly once in the same fashion.

Calling it as a function and using the result exactly once in the same fashion.

and my function sendToPeer does exactly this - pattern-matches on c and its argument d is used once - in Peer d which is linear:

By default, all fields in algebraic data types are linear (even if -XLinearTypes is not turned on).

but I got an error:

• Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘c’
• In an equation for ‘sendToPeer’:
          sendToPeer c n = case c of { Peer d -> pure $ Peer d }
   |
11 | sendToPeer c n =
   |            ^

Without pure:

sendToPeer :: Peer Idle %1-> Int -> Peer Busy
sendToPeer c n = case c of Peer d -> Peer d

but the error is the same.

Solution

You are bumping up against multiple problems:

Prelude.pure isn't linear. You need to use the linear Applicative class and associated method function pure from Control.Functor.Linear in linear-base.
Prelude.IO isn't linear (i.e., doesn't have an instance of the linear Applicative class). You need to use the linear IO from System.IO.Linear in linear-base.
(In GHC versions older than 9.2) case statements simply didn't work properly with the current LinearTypes extension.

With respect tot the last point, the GHC manual states:

A case expression may consume its scrutinee One time, or Many times. But the inference is still experimental, and may over-eagerly guess that it ought to consume the scrutinee Many times.

The User's Guide for linear-base is blunter. It includes a section titled Case statements are not linear which suggests that you just can't use them for linear functions.

For now, you have to avoid scrutinizing an expression with case if you want to retain it's Oneness. On GHC version 9.2 or newer this workaround is no longer necessary.

The following appears to type-check. I think I've got the imports set up in the recommended manner. Note that there are versions of pure in both Data.Functor.Linear and Control.Functor.Linear, and they work differently. See the comments at the top of the documentation for the Data.Functor.Linear module.

{-# LANGUAGE LinearTypes #-}

module Lib where

import Prelude.Linear
import Control.Functor.Linear as Control
import qualified Prelude as NonLinear
import qualified System.IO.Linear as Linear

data Peer st = Peer String deriving Show

data Idle
data Busy

sendToPeer :: Peer Idle %1-> Int -> Linear.IO (Peer Busy)
sendToPeer (Peer d) n = Control.pure (Peer d)