Add short syntax for dependent functor types

[yallop]

Brief summary

This PR adds a concise variant of functor type syntax. In brief, it allows (but does not require) the keyword functor to be omitted in functor types (but not in functor terms).

In other words, the current functor syntax looks like this:

functor (X:A) -> S

and this PR extends the syntax to also allow writing this:

(X:A) -> S

The new syntax is commonly used in dependently-typed languages such as Agda and Idris.

Previous episodes

The PR is the latest installment in an occasional series of functor type syntax simplifications. Previous episodes:

1. Simplify functor sig types #16 (OCaml 4.02.0) added shorter syntax for functor signatures, allowing -> functor to be omitted for type parameters after the first:

   Before:

   functor (X:A) -> functor (Y:B) -> F(X)(Y)

   After:

   functor (X:A) (Y:B) -> F(X)(Y)

2. Short functor type syntax #42 (OCaml 4.03.0) added shorter syntax for non-dependent functor parameters, allowing parameter names to be omitted
   :

   Before:

   functor (X:A) (Y:B) -> C

   After:

   A -> B -> C

3. Add short syntax for generative functor types: () -> ... #11694 (OCaml 5.1.0) added similarly short syntax for generative functor types:

   Before:

   functor () -> S

   After:

   () -> S

Motivation

Functor types occur occasionally in programs, but appear quite often in error messages and top-level printing, where the full syntax can make them rather difficult to read. Here is a fairly typical example from the test suite:

        Modules do not match:
          sig
            module F :
             functor
               (X : functor (A : sig type xaa end) (B : sig type xz end) ->
                      sig end)
               (Y : functor (A : sig type ya end) (B : sig type ybb end) ->
                      sig end)
               (Z : functor (A : sig type za end) (B : sig type zbb end) ->
                      sig end)
               -> sig end
          end
        is not included in
          sig
            module F :
             functor
               (X : functor (A : sig type xa end) (B : sig type xz end) ->
                      sig end)
               (Y : functor (A : sig type ya end) (B : sig type yb end) ->
                      sig end)
               (Z : functor (A : sig type za end) (B : sig type zb end) ->
                      sig end)
               -> sig end

After this PR the message is shorter:

        Modules do not match:
          sig
            module F :
             (X : (A : sig type xaa end) (B : sig type xz end) -> sig end)
             (Y : (A : sig type ya end) (B : sig type ybb end) -> sig end)
             (Z : (A : sig type za end) (B : sig type zbb end) -> sig end) ->
               sig end
          end
        is not included in
          sig
            module F :
             (X : (A : sig type xa end) (B : sig type xz end) -> sig end)
             (Y : (A : sig type ya end) (B : sig type yb end) -> sig end)
             (Z : (A : sig type za end) (B : sig type zb end) -> sig end) ->
               sig end

Omitting functor makes the error message significantly shorter (15 lines rather than 23) because it allows the parameter types to fit on a single line.

[nojb]

This PR

• is coherent with the other simplifications that have been done in the functor syntax,
• the actual diff is tiny,
• it aligns the module language with the core language (no keyword used to introduce function types)
• improves readability

In short, it looks like an excellent change, I'm wholly in favour!

[gasche]

I don't personally see functor types enough to perceive a real need for this syntactic sugar, but I see no harm with it either, and it is consistent with the previous shortcut syntaxes we introduced as @yallop recalled. I am tempted to vote in favor, unless someone comes with a counter-argument.

[yallop]

I've rebased to resolve conflicts, and credited @nojb as reviewer.

[garrigue]

This is a big change in terms of modified outputs, but I agree this looks nicer. The functor keyword does not seem to bring any useful information here.

[nojb]

There seems to be a consensus in favour, and no strong objections. @yallop: if you can

• resolve the conflict, and
• address @gasche's comment above

then I think we can move to merge.

[yallop]

I've fixed the conflict, incorporated @gasche's proposed change (which I'd somehow completely missed; sorry!) and credited him as a reviewer.

[nojb]

LGTM