Support modules of non-legacy modes

[riaqn]

Based on #3757 and #3758 and #3824

This PR adds the support for modules of non-legacy modes. Functor parameter and body are still fixed to be legacy.

TODO:

• Improve inclusion error messages
• Add tests reflecting subtle code changes in type checking
• Add tests showing functor application mode error message

The room for improvement shouldn't block preliminary review and discussion. In particular, changes to the existing tests seem correct, and can serve as a good starting point.

[goldfirere]

Took a quick look at the tests, just to understand the design better. Looks good to me, just a few comments as I was scrolling through.

[lukemaurer]

Still not entirely reviewed but just have env.ml and env.mli left.

[goldfirere]

I've resolved my Discussions on this PR

[lukemaurer]

Looks good, other than I think it should say “escapes its region” rather than “escapes region”

[riaqn]

@lukemaurer can you review the new commits:

post rebase fix

include should rebase modalities

change how extension level affects modalities

improve comments

change error message

[lukemaurer]

All good, up to a few comment tweaks

[riaqn]

For backward compatibility, this PR has the following catches:

• The semantics of user-written signatures (default modalities, modalities on include and on module) stay the exact same.
• That also means functor declaration will continue to be nonportable, even though our type checker is now capable of infering it to be portable.

This will be addressed in a future PR (probably under mode_alpha).

[riaqn]

Catch-up review for @lukemaurer
b46c23c
a7d4d54
And please review the following two commits combined: (this is related to #3578 but doesn't affect performance)
722efb0
be7a018