Infer multiplicity of let expression
In a let expression
let x = rhs in u,
x is always bound with multiplicity
Many (and, correspondingly,
u is consumed with multiplicity
This also holds of where expression
u where x = rhs.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect
let x = y in u to be the same as
u[x\y], but if the latter consumes
y linearly, the former never does in the current GHC).
Infer the multiplicity of
let binders instead of choosing
Many systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in
let pat = rhs in u, the outermost pattern of
pat is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .