https://github.com/effectfully-ou/sketches/tree/master/exhaustive-unordered-pattern-matching

LinearMatchTroubles.hs

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
module Main where

import Data.Unrestricted.Linear (move, unur, Ur(..)) -- from linear-base

data R = R 
    { a :: Int
    , b :: Int
    -- , c :: Int
    }

serializeT :: R %1 -> (Int, Int)
serializeT (R a b) = (a,b)

-- | Doesn't work. Why?
serializeR :: R %1 -> IO ()
serializeR (R {a,b}) = 
        let a' = unur (move a)
            b' = unur (move b)
        in do
            serializeA do a'
            serializeB do b'

serializeA :: Int -> IO ()
serializeA = print

serializeB :: Int -> IO ()
serializeB = print

main :: IO ()
main = pure ()

ThisActuallyWorks.hs

-- Requires GHC 9.10.1
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LinearTypes #-}
-- Can't use NamedFieldPuns because of https://gitlab.haskell.org/ghc/ghc/-/issues/24961
{-# LANGUAGE RecordWildCards #-}

module Main where

import Data.Unrestricted.Linear (Ur (..), move) -- from linear-base

data R = R
  { a :: Int,
    b :: Int
    -- Adding this field will cause 'serializeR' to fail to compile.
    -- , c :: Int
  }

serializeR :: R %1 -> IO ()
serializeR (R {..}) =
  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html
  -- The pattern match must be strict, it seems.
  -- The %1s seem to be optional. Maybe multiplicity is inferred as One even without them?
  -- https://hachyderm.io/@DiazCarrete/112581730831289011
  -- https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/strict.html#strict-bindings
  -- https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/linear_types.html#bindings  
  -- What does it mean to have a linear let with a non-linear body?
  let %1 !(Ur a') = move a
      %1 !(Ur b') = move b
   in do
        serializeA a'
        serializeB b'

serializeA :: Int -> IO ()
serializeA = print

serializeB :: Int -> IO ()
serializeB = print

main :: IO ()
main = pure ()