Linear types syntax: multiplicity annotations on lets

Motivation

This is a continuation of #18460 : we want to support the multiplicity annotation on let and where binders.

let %p x = … in …
let %p x :: a = … in …

The typing rule for let %p x = … in … is that given in Figure 6 in the Linear Haskell paper.

See also the linear types proposal, in particular Section Multiplicities. When I first wrote this paragraph, we had no syntax for multiplicity-annotated lets, so the paragraph only talks of inference. But, as Section Effect on transformations and passes makes clear, by the time the proposal was accepted, we had designed the syntax let x %p = … in …; it's only an oversight that the syntax was not added to the Change specification. The syntax was later modified by the Modifiers proposal.

[EDIT 2022-10-21: change the syntax from x # p to %p x, as designed in the modifiers proposal.]
[EDIT 2022-11-22: add precise references for the design of linear let]

Proposal

There is quite a bit of work here. That's why I made it a separate issue of #18460 . There are a number of shortcuts in the code where we simply assume that let binders have multiplicity Many. Since there is no way to make them otherwise. And even if we had been careful to not make such assumptions, the fact that all let binders are indeed Many means that the code would probably be incorrect.