Incorrect linearity checking of non-exhaustive named field puns in pattern matches

Summary

According to the documentation for -XLinearTypes, a function that linearly consumes a conventional record and pattern-matches on it must "consume" all of its fields exactly once (for example, by returning them unmodified in a tuple).

However, when using named field puns, GHC mistakenly lets the function "forget" about fields that aren't "punned", letting them go unconsumed.

Steps to reproduce

Try to compile this program:

{-# LANGUAGE LinearTypes #-}
module Main where

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

foo :: R %1 -> (Int,Int)
foo (R {a,b}) = (a,b)

main :: IO ()
main = pure ()

It will compile without an error.

Expected behavior

The program should fail to compile, and GHC should emit a linearity-related error about the field c.

If we use RecordWildCards instead of NamedFieldPuns, the linearity error is detected. The program

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE RecordWildCards #-}
module Main where

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

foo :: R %1 -> (Int,Int)
foo (R {..}) = (a,b)

main :: IO ()
main = pure ()

Fails to compile, with error

Main.hs:12:9: error: [GHC-18872]
    • Couldn't match type ‘Many’ with ‘One’
        arising from multiplicity of ‘c’
    • In the pattern: R {..}
      In an equation for ‘foo’: foo (R {..}) = (a, b)
   |
12 | foo (R {..}) = (a,b)
   |         ^^

Environment

• GHC version used: 9.10.1