Motivation

In a let expression let x = rhs in u, x is always bound with multiplicity Many (and, correspondingly, u is consumed with multiplicity Many).

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).

Proposal

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 .