Guards should accept linear variables
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 (closed) 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 (closed) .
- Is
f3
linear?f3 :: Bool %1 -> Int f3 x | x = 0 f3 x | otherwise = 1
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 considerf1
andf3
to be synonymous, and it may be surprising. - Is
f4
linear?f4 :: Bool %1 -> Int f4 x | x = 0 f4 x = 1
f3
too. But it is also different in subtle ways. Here again, some will considerf3
andf4
synonymous. But it's not necessarily clear that typecheckingf4
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.