Linear let and where bindings

For expediency, the initial implementation of linear types in GHC made it so that let and where binders would always be considered unrestricted. This was rather unpleasant, and probably a big obstacle to adoption. At any rate, this was not how the proposal was designed.

This patch fixes this infelicity. It was surprisingly difficult to build, which explains, in part, why it took so long to materialise.

As of this patch, let or where bindings marked with %1 will be linear (respectively %p for an arbitrary multiplicity p). Unmarked let will infer their multiplicity.

Here is a prototypical example of program that used to be rejected and is accepted with this patch:

f :: A %1 -> B
g :: B %1 -> C

h :: A %1 -> C
h x = g y
  where
    y = f x

Exceptions:

• Recursive let are unrestricted, as there isn't a clear semantics of what a linear recursive binding would be.
• Destructive lets with lazy bindings are unrestricted, as their desugaring isn't linear (see also #23461).
• (Strict) destructive lets with inferred polymorphic type are unrestricted. Because the desugaring isn't linear (See #18461 (closed) down-thread). For this reason, -XLinearTypes now implies -XMonoLocalBinds.

Breaking changes:

That -XLinearTypes implies -XMonoLocalBinds is a breaking change. But I expect to affect very few packages. Linear types are still pretty niche, and you'd need to use them without either GADTs or Type Families (rare) and use let/where bindings at different types.

This is a collaboration with @jackohughes.

This also restores the desugaring of non-recursive lets to non-recursive lets (which is necessary for linear lets) whose first iteration was incorrect (see #23550 (closed)). Thanks @simonpj for helping me figure out the right solution for this.

Excluding tests:

• The main commit is 500loc, half in GHC.Tc.Gen.Binds
• The whole MR (including reverts) is 750loc, half in GHC.Tc.Gen.Binds and GHC.HsToCore.Binds

A lot of the non-local changes is due to the fact that tcSubmult isn't a constraint, and uses a wrapper to check, at desugar time, that indeed we don't need evidence in Core. Living outside of the constraint implication framework of OutsideIn is also a problem (in our case, it created a new .hs-boot file for instance). I'll be quite relieved when we manage to repay this technical debt. The code from this PR will simplify quite a lot. But as far as I understand, this is blocked on !2857, which, considering it's been in progress for years, is probably harder than it sounds. So, for now, we pay the price…

Closes #18461 (closed) and #18739 (closed)

TODO (which shouldn't affect code reviews):

• updates the users guide
• mentions new features in the release notes for the next release
• fix the syntax. I'm pretty sure I use at least two different syntaxes (parser vs printer). I need to come back to the Modifiers proposal to figure out what is the syntax we finally settled on (if I remember correctly, last time I checked I found that the modifiers on let bindings were not clearly specified, so there's some interpreting to do to figure out what was intended).
• what should I do with multiplicity annotations on binders in the Core pretty-printer? They should definitely be printable, because they're relevant when debugging the desugarer. But they're only relevant, currently, for the desugarer. Maybe they should be controlled by a separate flag, and turned off by default? (this affects a few tests whose output would be changed if we display the multiplicity annotations)
• locally, so I assume we'll see that on CI, the branch currently doesn't build. This is as off my latest rebase. I get a Core Lint error in Sequence.Internal. The lint error looks incorrect to me, and because it occurs after the simple optimiser, I don't think my patch is the cause (since it doesn't change Core at all). To investigate.