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

added needs triage label

mentioned in issue #23461

removed needs triage label

added BangPatterns LinearTypes Pnormal Tbug labels

@aspiwack, @monoidal, perhaps you could comment here? This indeed looks suspicious.

Yes, it's presumably a bug. Artem told me about it earlier, I asked him to write an issue. I won't be able to follow up on it quite immediately, though.

What seems to be happening is that a pattern with no variable bypasses -XMonoLocalBinds and generates an InferGen plan (which, I believe, tries to generalise the type all of the 0 variables that we introduce).

As it happens, generalising pattern bindings and linearity really aren't friends, so the type system makes the pattern unrestricted then. You can observe that by writing

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

Which makes the binding non-generalisable (and is higher priority than the other condition). So this typechecks (and uses a NoGen plan).

I believe the condition that we trigger to be

      | IsGroupClosed _ True <- closed = True

My instinct is to return another value for bindings with no variables, but I don't know the consequences yet.

(well, the consequences are probably very controllable: these seem to be a single call to isClosedBndrGroup, probably it's used for other tests though, but the effects are very localised)

mentioned in merge request !13629 (closed)

I've pushed a fix in !13629 (closed) . I'm not completely sure that it's the right way to go about it. But I'm pretty sure that it is a good solution.

mentioned in commit dc7952b3

mentioned in commit 6b1c6b95

mentioned in commit e6c957e4

closed with commit 52d97f4e

mentioned in commit 52d97f4e

mentioned in commit d7d9aa07

mentioned in commit 2e3ce607

mentioned in commit a0cc8121

mentioned in commit 68d3ab8b