Inclusion of functors with restricted signature is now forbidden (fix #3746)

 The previous behavior was to include the interface of such a functor,
 possibly leading to the creation of unexpected axioms, see bug report #3746.
 In the case of non-functor module with restricted signature, we could
 simply refer to the original objects (strengthening), but for a functor,
 the inner objects have no existence yet. As said in the new error message,
 a simple workaround is hence to first instantiate the functor, then include
 the local instance:

  Module LocalInstance := Funct(Args).
  Include LocalInstance.

 By the way, the mod_type_alg field is now filled more systematically,
 cf new comments in declarations.mli. This way, we could use it to know
 whether a module had been given a restricted signature (via ":"). Earlier,
 some mod_type_alg were None in situations not handled by the extraction
 (MEapply of module type).

 Some code refactoring on the fly.

1 files changed, 17 insertions, 7 deletions

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index bc0e20205..d07d59dd9 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -14,9 +14,18 @@ open Names
 
 (** Main functions for translating module entries *)
 
+(** [translate_module] produces a [module_body] out of a [module_entry].
+    In the output fields:
+    - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
+    - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.
+*)
+
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
+(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
+    cannot be [None] (and of course [mod_expr] is [Abstract]). *)
+
 val translate_modtype :
   env -> module_path -> inline -> module_type_entry -> module_type_body
 
@@ -24,20 +33,21 @@ val translate_modtype :
     - We translate to a module when a [module_path] is given,
       otherwise to a module type.
     - The first output is the expanded signature
-    - The second output is the algebraic expression, kept for the extraction.
-      It is never None when translating to a module, but for module type
-      it could not be contain applications or functors.
-*)
+    - The second output is the algebraic expression, kept mostly for
+      the extraction. *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
+(** From an already-translated (or interactive) implementation and
+    an (optional) signature entry, produces a final [module_body] *)
+
 val finalize_module :
-  env -> module_path -> module_expression translation ->
+  env -> module_path -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
   module_body
 
@@ -46,4 +56,4 @@ val finalize_module :
 
 val translate_mse_incl :
   bool -> env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
+    unit translation