Skip to content

Strict unit pattern in a local let binding breaks linearity

Summary

The title says it all. Strict tuple patterns work fine but the unit doesn't.

Steps to reproduce

Compiling the program

{-# language LinearTypes #-}

f :: Int %1 -> ()
f = undefined

g :: Int %1 -> Int
g x = let
    !() = f x
  in 1

g' :: Int %1 -> Int
g' x = case f x of
  () -> 1

I get:

LinearUnitPattern.hs:7:3: error: [GHC-18872]
    • Couldn't match type ‘Many’ with ‘One’
        arising from multiplicity of ‘x’
    • In an equation for ‘g’: g x = let !() = f x in 1
  |
7 | g x = let
  |   ^

Note that the case equivalent in g' compiles fine.

Expected behavior

No error.

Environment

  • GHC version used: 9.10.1

Optional:

  • Operating System: NixOS 24.05
  • System Architecture: x86_64

cc @aspiwack

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information