GitLab

Motivation

In GHC 9.0, guards in case expressions or equations cannot contain linear variables (see fixes for #18439 (closed) and #19120 (closed)).

The following, for instance, will refuse to typecheck

f1 :: Bool %1 -> Int
f1 x
  | x = 0
  | otherwise = 1

However, guards are “just” another syntax for case and if expressions, where linear variable make perfect sense:

f2 :: Bool %1 -> Int
f2 x = if x then 0 else 1

In principle, at least, it seems reasonable and idiomatic to allow f1, and such functions.

Proposal

The high-level proposal is easily written: make the type-checker aware of when a guard really consumes a value linearly.

But there are many things to understand

• We must make sure that such linear guards desugar to linear Core (by which I mean: the linter recognises that the code is properly linear). Maybe it is, maybe we may need to tweak it a little. See also #18806 which has similar issues.
• In pattern guards, we need to make sure that if the guard is linear, the bound variables are correspondingly linear. This is connected to #18738 .
• Is f3 linear?

  f3 :: Bool %1 -> Int
  f3 x | x = 0
  f3 x | otherwise = 1

  It's very similar to f1. Though it is typechecked and desugared differently. Does it matter in practice? Is this even reasonable to ask in theory? If the answer is no, though, let me note that around me there are people which consider f1 and f3 to be synonymous, and it may be surprising.
• Is f4 linear?

  f4 :: Bool %1 -> Int
  f4 x | x = 0
  f4 x = 1

  It looks a lot like f3 too. But it is also different in subtle ways. Here again, some will consider f3 and f4 synonymous. But it's not necessarily clear that typechecking f4 as linear is reasonable in practice (I hope it would be though).

I'm probably forgetting other interesting special cases. But the point is: there is some pen-and-paper work to be done to specify what it even means to specify that a guard is linear. It may be easy, it may be hard; I don't know: I really haven't tried yet. The recent Lower your guard paper may offer a framework to think about these things.

(cc @monoidal @rae )