Refactor new mode syntax

[riaqn]

This PR refactors the new mode syntax (@ and @@).

• With this PR, @ always means modes, and @@ always mean modalities. Previously, @@ can mean modes in some position for disambiguition. For example, x : a -> a @@ local says x is local, and x : b -> a @ local says a is local). After this PR, the first example will write x : (a -> a) @ local. The second example doesn't change. You can also write x : a @ local.
• To ensure certain parsing-printing roundtrip, we print modes in legacy position only if the whole mode annotation contains old modes only. That means local_ a @ portable -> b will print back a @ local portable -> b, while local_ a -> b prints back the same. The idea is that "if the user already knows about and uses the new mode syntax, then we should print back new mode syntax". This is done in both pprintast.ml and printtyp.ml.
• fun a b : ty @@ modes -> .. was introduced by Supports mode annotation on function body #3327 , and would be changed to fun a b : ty @ modes -> ... Note the ambiguity: the arrow could be arrow type. We decide to remove this for simplicity.
• Refactoring and fixes in parser.mly and pprintast.ml, so that some missing corner cases are covered, and diff to the upstream is minimized. For example, labeled_simple_pattern is now almost identical to upstream. This allows systematic enumeration of all possible syntax, which helps with user documentation, and test coverage.
• The mode section in source_jane_street.ml is rewritten to cover all possible syntax.

Suggestions to reviewers

• First look at the mode section of source_jane_street.ml, to get a sense of the new syntax (don't look at the type errors - they are fine).
• Then look at parser.mly.
• Then look at pprintast.ml and printtyp.ml. The former should be functionally "most fine" as tested by source_jane_street.ml, but other aspects such as coding style should be inspected.
• Changes in tests, except source_jane_street.ml, are all mechanical and can be skipped.

[github-actions]

Parser Change Checklist

This PR modifies the parser. Please check that the following tests are updated:

• parsetree/source_jane_street.ml

This test should have examples of every new bit of syntax you are adding. Feel free to just check the box if your PR does not actually change the syntax (because it is refactoring the parser, say).

[tdelvecchio-jsc]

It's a bit sad that this PR is 3 different changes in one, but all in heavily overlapping code:

• switching local_ x @ portable to x @ local portable
• switching (x : t @@ local) to (x : t @ local)
• changes some logic related to curry syntax? not sure what this is about.

Alas, thing at least looked reasonable on my first pass. Left some comments.

[riaqn]

Thanks for the review.

It's a bit sad that this PR is 3 different changes in one, but all in heavily overlapping code

Yeah I agree this is sad; but also due to the overlapping, it wouldn't make sense to separate them into PRs.

[riaqn]

Note to myself: add default modalities to syntax.md.
DONE