# Infer multiplicity of let expression

## 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 (closed) .

In #18461 (closed) , 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 (closed) .