Hi all, I've reviewed Arnaud's https://github.com/ghc-proposals/ghc-proposals/pull/624 https://github.com/ghc-proposals/ghc-proposals/pull/624 and wish to recommend acceptance. The proposal is an amendment to the proposal for linear types, adding support for linear let bindings. Today, if you have f :: T %1-> T f t = let t2 = t in t2 you'll get an error because t2 is not linear. The only way to bind a linear variable is via a `case`, never a `let` or `where`. This is annoying. With this proposal, the little program above is accepted, with an inferred linearity restriction on t2. Users can also annotated their lets like `let %1 x = ... in ...`. Bindings in `where` clauses can also be inferred or annotated as linear. There is a downside, of course: linear bindings have various restrictions, chiefly that they must be strict bindings (because projections are hard with linear types) and that bindings cannot be generalized. I'm a little unsure that the choices in the proposal (particularly around generalization) are the best for users, but I think the best way to learn is to experiment. In my understanding, the community knows that -XLinearTypes is subject to revision, and so I think we should just blast ahead, revising if and when necessary. Please share your thoughts! Thanks, Richard