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