LinearTypes: Spurious multiplicity error when wrapping an empty-case lambda in a data/newtype constructor

Summary

When using -XLinearTypes and -XEmptyCase, a lambda that eliminates Void via case void of {} type-checks correctly when used directly as the body of a linear function, but is rejected with a multiplicity mismatch when the same lambda is passed as an argument to a data or newtype constructor.

Steps to reproduce

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LinearTypes #-}

import Data.Void

ok1 :: a %1 -> Void %1 -> ()
ok1 a void = case void of {}

ok2 :: a %1 -> Void %1 -> ()
ok2 a = \void -> case void of {}

data DT = DT (Void %1 -> ())

newtype NT = NT (Void %1 -> ())

ng1 :: a %1 -> DT
ng1 a = DT (\void -> case void of {})

ng2 :: a %1 -> NT
ng2 a = NT (\void -> case void of {})

When I load the code above, I get the following error:

LinearHaskellMystery.hs:17:5: error: [GHC-18872]
    • Couldn't match type ‘Many’ with ‘One’
        arising from multiplicity of ‘a’
    • In an equation for ‘ng1’: ng1 a = DT (\ void -> case void of {})
   |
17 | ng1 a = DT (\void -> case void of {})
   |     ^

LinearHaskellMystery.hs:20:5: error: [GHC-18872]
    • Couldn't match type ‘Many’ with ‘One’
        arising from multiplicity of ‘a’
    • In an equation for ‘ng2’: ng2 a = NT (\ void -> case void of {})
   |
20 | ng2 a = NT (\void -> case void of {})
   |     ^

Expected behavior

All four definitions (ok1, ok2, ng1, ng2) should be accepted. In all cases, a is bound linearly but the body is an empty case analysis on Void. Since there are zero branches, it vacuously satisfies the linearity requirement (there is no branch where a is not consumed exactly once, because there are no branches at all).

Environment

• GHC version used: 9.14.1

Optional:

• Operating System: macOS Sequoia 15.7.4
• System Architecture: Apple M4