clarify meaning of "non-path module type"

[smuenzel]

The error produced when we do the following:

module type fst = sig
  module type t := sig end
  val x: (module t)
end

uses the term "non-path module type", which is not defined in the manual. This PR replaces it with "a module type which does not have a name", which I think is equivalent, and should be more understandable to those who are not as familiar with module types.

I don't believe this needs a changes entry, since it's just a small wording change.

[gasche]

Technically users may not understand that F(X).T counts as a "name". Also, in your example, it is not clear why t does not have a name -- its name is t, right?

I think you have a good sense of the issue but I am not sure that your proposed change is really an improvement. Should we maybe consider writing a more detailed explanation somewhere in the manual, and linking to this in the error message?

[smuenzel]

Here's a possible way of improving it:

1. Change the wording in the manual at section 12.7.3 to include the syntactic definition of the path

If the right hand side of the substitution is not a @modtype-path@,
then the destructive substitution is only valid if the left-hand side of the
substitution is never used as the type of a first-class module in the original
module type.

2. Change the wording of the error message to refer to the destructive substitution (to show that t is not available for naming in the final module type). Maybe:

 Error: The module type "t" is not a valid type for a packed module:
        destructive substitution of "t" is not possible since the resulting
        packed module type cannot be named using a module type
        path. (see manual section 12.7.3)

I guess this error message is more "correct", not sure if it's actually more helpful.

[gasche]

We can include examples and more detailed explanations in the manual, and give a more nuanced explanation than a beginner-friendly-but-also-confusing-in-some-cases wording choice.

Your proposed wording seems good, but is it actually the case that this error can only be caused by destructive substitution and packed modules?

You could maybe improve clarity for beginners by showing some concrete syntax: "destructive substitution (module type t := ...)" instead of just "destructive substitution".

[Octachron]

I tend to find the name local substitution (used in the manual) a little clearer than destructive substitution in this context. Maybe something like

 Error: The name "t" is a temporary local name for an anonymous module type 
    which cannot be used as a type for a packed module (see manual section 12.7.3).

?

[smuenzel]

I changed the wording of the error message and added some details to the manual. In the manual, there are two relevant sections, so I only included the information once.

[gasche]

This is solid work, but I am bit disturbed by the fact that the error message (as suggested by @Octachron) says "temporary local name" instead of "local substitution", when the manual says "local substitution".

I would be please if either:

• the manual also contained "temporary local name" somewhere in its text, so that someone grepping the wording of the error message would the right paragraphs to read
• the error message used both forms, for example "it is defined as a local substitution (temporary local name) for an anonymous module type" or "it is defined as a temporary local name (a local substitution) for an anonymous module type".

[gasche]

(I don't think you need the "Draft" status anymore.)

[smuenzel]

I updated the wording.
I think ideally, we'd only have a single name for each concept.

[gasche]

I think that local substitution is the precise name for the feature, and temporary local name is the beginner-friendly explanation for the status of a name t when bound uusing this feature.

@Octachron if the proposed wording also works for you, I think we can merge -- the implementation is fine.

[Octachron]

The use of removal sounds potentially confusing since it is not clear what we are removing and when we are removing it. Similarly, extended paths are also allowed in types:

module type s = sig
  type t := Set.Make(String).t
end

Maybe we should provide both examples

Local substitutions can also be used to give a local name to a type or a module type introduced by a functor application:

module type F = sig
  type set := Set.Make(Int).t

  module type Type = sig type t end (* introduced to avoid using `module type of` *)
  module Nest : Type -> sig module type T = Type end

  module type T := Nest(Int).T

  val set: set
  val m : (module T)
end;;

?

[Octachron]

Indeed, the temporary adjective is trying to give more context to the error: we have a requirement conflict between a name that is going out-of-scope soon and a first-class module type that needs to be anchored to some name.

Pedantically, temporary and local are clashing metaphors and redundant, but I have the feeling that it may help
non-expert users a lot without a notable conciseness cost.

Maybe we could drop the local part in temporary local name since we are now using the more precise local substitution name:

it is defined as a local substitution (temporary name)

like this we are using a spatial metaphor on the expert side and a temporal one on the beginner side without layering the two on top of another?

[gasche]

I could discuss the precise wording of the error message for a couple extra weeks, there are so many nuances! But I am in favor of merging the current state which seems fine.