Functor error messages: signatures are not functors

[Octachron]

This PR proposes to add a specialized error message whenever some code tries to use a signature as a functor.

For instance, since OCaml 4.14,

module R = Int(List)

falls in the functor error code path, resulting in this quite long

Error: The functor application is ill-typed.
      These arguments:
        List
      do not match these parameters:
        functor  -> ...
      The following extra argument is provided
          List :
          sig
            type 'a t = 'a list = [] | (::) of 'a * 'a list
            val length : 'a t -> int
            ...
           end

error message. Prior to OCaml 4.13, the error message was more specialized

Error: This module is not a functor; it has type
      sig
        type 'a t = 'a list = [] | (::) of 'a * 'a list
        val length : 'a list -> int
        ...
       end

This PR proposes to go one step further and reduces the error message to

Error: The module Int is not a functor, it cannot be applied.

and similarly for inclusion error

module F(X:sig end): () -> sig end = X

      Modules do not match: sig end is not included in functor () -> sig end
      The first one is a signature whereas the second one is a functor.

under the assumption that in this context it is better to emphasize the module kind mismatch rather than the types of the extraneous arguments.

Along the way, this PR updates the error message for functor applications to display the name of the applicand whenever possible. Previously, this name was only printed for ill-typed functor applications in type expressions:

let f (x:Set.Make(Set)(Int).t) = x

Error: The functor application Set.Make(Set)(Int) is ill-typed.

but not at the module expression level

module R = Set.Make(Set)(Int)

Error: The functor application is ill-typed.

with this PR, this error abstract is amended to

Error: This functor application of Set.Make is ill-typed.

since this change is a low hanging fruit, once the non functor case is already checking if the applicand has a human readable name.

[gasche]

This PR proposes to go one step further and reduces the error message to

Error: The module Int is not a functor, it cannot be applied.

This looks great.

and similarly for inclusion error

module F(X:sig end): () -> sig end = X
(* Modules do not match: sig end is not included in functor () -> sig end
   The first one is a signature whereas the second one is a functor. *)

I don't like the wording here. I use "signature" and "interface" as basically synonyms to mean "the type of a module or functor", so opposing "a signature" and "a functor" makes no sense to me:

• by "a signature" you mean "the signature of a structure (not a functor)"
• by "a functor" you mean "the signature/interface of a functor"

The following wording may work: "The first one is the signature of a structure whereas the second one is the signature of a functor". (I tried first with "a structure signature ... a functor signature" and it read less clearly.) Another wording could be: "The first signature specifies a structure whereas the second signature specifies a functor". ('specifies' or 'classifies' or 'describes')

[xavierleroy]

Terminology police here! Sir, put your hands up and away from this PR!

A signature is the type of a structure. (Notice the parallel between struct...end and sig...end?) The type of a functor is a functor type, not a signature.

An acceptable wording would be "The first one is the type of a structure whereas the second one is the type of a functor".

However "first one" and "second one" are not quite well defined (what is "one", here?) and should perhaps be "The former" and "the latter".

Could also replace "is the type of" by something more pleasant to read, e.g. "denotes", "matches", "corresponds to" ?

[Octachron]

Maybe

  The former is a signature whereas the later is a functor type.

?
A quick poll at the MirageOS retreat seems to indicate that the line is useful (for 90% of people), but that a significant amount of people (20%?) infers the meaning of signature (as non a functor) from the error message rather than the reverse. That seems potentially fine with me since it helps fix a short terminology.

A potentially interesting and quick to implement proposal was to completely shortcut the main error message in this case.

Modules do not match: 
  A signature is incompatible with the required functor type.

since this avoid speaking of the subtyping relation when the two module kinds are incomparable.

But this rejoin a later complaint that is really for people where the module type constraints come from. I will have a look (after my holidays) if we can track the location of both side of the subtyping to remove this issue.

I will propose to split the two commit of this PR since the application error is both the more frequent error and the more consensual change.

[gasche]

Personally I find "type of a structure", as suggested in Xavier's proposal, clearer in this context than "signature" (for the reason given earlier that my own improper terminology use "signature" as a synonym for the more general "type of a module", including possibly functors).

[Octachron]

I have split the inclusion and application part as discussed.

[gasche]

I don't understand the code here. The error message suggests that what is shown is the full functor application (so of the form Foo(Bar)), but the code suggests that lidin fact only denotes the functor part of the application (so only Foo), in the case where it is an application itself. So I would expect the error message to be "off", with a problematic application ((F(x))(Y) being reported as an error on F(X). But in fact the testsuite seems to suggest that the implementation is correct. What am I missing about what lid_app means?

[Octachron]

lid_app is a "best"-effort nominal approximation for the functor application. In particular it is either:

• Some (Lapply _ ) if the functor application can be resumed as a path-with-application F(X(A).B)(Y), in practice we only recover those in the easy case of functor application at the type level (F(X).t)
• Some (<Module path of the leftmost functor>) if we are not in the case above but at least the leftmost functor has a name
• None if there are no name for neither the functor application nor the leftmost functor

I propose to split this option into a specialized ternary variant rather than rely on its content to distinguish the two approximation cases.

[gasche]

Yes please!

[gasche]

I'm not fond of the wording "This functor application of Map.Make". Alternative proposal: "The application of the functor Map.Make".

[Octachron]

I slightly prefer to keep the demonstrative whenever we have a dependency on the context. Nevertheless, I agree that This application of the functor seems simpler (and thus better).

[gasche]

Thanks! The code looks good now. Approved.

[gasche]

I have a hunch that it might be better to keep located identifiers in the error payload. (Something about future programmatic handling of errors in third-party tools, with fixup suggestions etc.) Feel free to act on it or not.

[Octachron]

Possibly. However, I would rather add this information once it is exploitable rather than anticipate many layers of future improvements.