Linear types syntax: multiplicity annotations on lambdas and patterns

Motivation

The linear types proposal introduces a syntax to annotate a lambda binder (or more generally a pattern) with a multiplicity, when -XScopedTypeVarialbes is on (that is, whenever a type annotation is allowed).

The syntax is

\ x # p -> …
\ x # p :: a -> …

This is, I believe, fully specified by the following type annotation grammar rule for pattern:

pat -> pat [# btype] [:: type]

Proposal

I expect that a lot of the necessary material is there already. This does change the typechecking algorithm a little, which will now have the ability to generate linear functions outside of checking mode.

In this issue, I suggest that we make annotating let expression thus an error. As it's a harder issue. I've made it #18461 (closed) .