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.

6 files changed, 112 insertions, 77 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75..0b8272b43 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -238,17 +238,26 @@ and module_body =
   { mod_mp : module_path; (** absolute path of the module *)
     mod_expr : module_implementation; (** implementation *)
     mod_type : module_signature; (** expanded type *)
-    (** algebraic type, kept if it's relevant for extraction *)
-    mod_type_alg : module_expression option;
-    (** set of all universes constraints in the module  *)
-    mod_constraints : Univ.ContextSet.t;
-    (** quotiented set of equivalent constants and inductive names *)
-    mod_delta : Mod_subst.delta_resolver;
+    mod_type_alg : module_expression option; (** algebraic type *)
+    mod_constraints : Univ.ContextSet.t; (**
+      set of all universes constraints in the module  *)
+    mod_delta : Mod_subst.delta_resolver; (**
+      quotiented set of equivalent constants and inductive names *)
     mod_retroknowledge : Retroknowledge.action list }
 
+(** For a module, there are five possible situations:
+    - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
+    - [Module M := E] then [mod_expr = Algebraic E; mod_type_alg = None]
+    - [Module M : T := E] then [mod_expr = Algebraic E; mod_type_alg = Some T]
+    - [Module M. ... End M] then [mod_expr = FullStruct; mod_type_alg = None]
+    - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
+    And of course, all these situations may be functors or not. *)
+
 (** A [module_type_body] is just a [module_body] with no
     implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge] *)
+    an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+    the algebraic definition of this module type, or [None]
+    if it has been built interactively. *)
 
 and module_type_body = module_body
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bd7ee7b33..8a1634881 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
 open Mod_subst
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 let rec mp_from_mexpr = function
   | MEident mp -> mp
@@ -183,8 +183,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
 	  begin
             try
               let mtb_old = module_type_of_module old in
-              Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
-	    with Failure _ -> error_incorrect_with_constraint lab
+              let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+              Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+	    with Failure _ ->
+              (* TODO: where can a Failure come from ??? *)
+              error_incorrect_with_constraint lab
 	  end
 	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
@@ -238,104 +241,89 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
-
 let check_with env mp (sign,alg,reso,cst) = function
   |WithDef(idl,c) ->
     let struc = destr_nofunctor sign in
     let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
-    let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
-    (NoFunctor struc'),alg',reso, cst+++cst'
+    let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
+    NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
-    let alg' = mk_alg_with alg wd in
-    (NoFunctor struc'),alg',reso', cst+++cst'
+    NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
 
-let mk_alg_app mpo alg arg = match mpo, alg with
-  | Some _, Some alg -> Some (MEapply (alg,arg))
-  | _ -> None
+let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
+  let farg_id, farg_b, fbody_b = destr_functor sign in
+  let mtb = module_type_of_module (lookup_module mp1 env) in
+  let cst2 = Subtyping.check_subtypes env mtb farg_b in
+  let mp_delta = discr_resolver mtb in
+  let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+  let subst = map_mbid farg_id mp1 mp_delta in
+  let body = subst_signature subst fbody_b in
+  let alg' = mkalg alg mp1 in
+  let reso' = subst_codom_delta_resolver subst reso in
+  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
 
 (** Translation of a module struct entry :
     - 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 [SEBapply] or [SEBfunctor].
 *)
 
+let mk_alg_app alg arg = MEapply (alg,arg)
+
 let rec translate_mse env mpo inl = function
-  |MEident mp1 ->
-    let sign,reso = match mpo with
-      |Some mp ->
-        let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
-        mb.mod_type, mb.mod_delta
-      |None ->
-        let mtb = lookup_modtype mp1 env in
-        mtb.mod_type, mtb.mod_delta
+  |MEident mp1 as me ->
+    let mb = match mpo with
+      |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
+      |None -> lookup_modtype mp1 env
     in
-    sign,Some (MEident mp1),reso,Univ.ContextSet.empty
+    mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
-    translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+    translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
   |MEwith(me, with_decl) ->
     assert (mpo == None); (* No 'with' syntax for modules *)
     let mp = mp_from_mexpr me in
     check_with env mp (translate_mse env None inl me) with_decl
 
-and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
-  let farg_id, farg_b, fbody_b = destr_functor sign in
-  let mtb = module_type_of_module (lookup_module mp1 env) in
-  let cst2 = Subtyping.check_subtypes env mtb farg_b in
-  let mp_delta = discr_resolver mtb in
-  let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
-  let subst = map_mbid farg_id mp1 mp_delta in
-  let body = subst_signature subst fbody_b in
-  let alg' = mkalg alg mp1 in
-  let reso' = subst_codom_delta_resolver subst reso in
-  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
-
-let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
-  | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
-  | _ -> None
-
-let mk_mod mp e ty ty' cst reso =
+let mk_mod mp e ty cst reso =
   { mod_mp = mp;
     mod_expr = e;
     mod_type = ty;
-    mod_type_alg = ty';
+    mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = reso;
     mod_retroknowledge = [] }
 
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
 
 let rec translate_mse_funct env mpo inl mse = function
   |[] ->
     let sign,alg,reso,cst = translate_mse env mpo inl mse in
-    sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+    sign, NoFunctor alg, reso, cst
   |(mbid, ty) :: params ->
     let mp_id = MPbound mbid in
     let mtb = translate_modtype env mp_id inl ([],ty) in
     let env' = add_module_type mp_id mtb env in
     let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
-    let alg' = mk_alg_funct mpo mbid mtb alg in
+    let alg' = MoreFunctor (mbid,mtb,alg) in
     MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
 
 and translate_modtype env mp inl (params,mte) =
   let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
   let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
   let mtb' = subst_modtype_and_resolver mtb mp in
-  { mtb' with mod_type_alg = alg }
+  { mtb' with mod_type_alg = Some alg }
 
 (** [finalize_module] :
-    from an already-translated (or interactive) implementation
-    and a signature entry, produce a final [module_expr] *)
+    from an already-translated (or interactive) implementation and
+    an (optional) signature entry, produces a final [module_body] *)
 
 let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
   |None ->
     let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
-    mk_mod mp impl sign None cst reso
+    mk_mod mp impl sign cst reso
   |Some (params_mte,inl) ->
     let res_mtb = translate_modtype env mp inl params_mte in
     let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
@@ -344,33 +332,59 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
-      (** cst from module body typing, cst' from subtyping, 
-          and constraints from module type. *)
-      mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+      (** cst from module body typing,
+          cst' from subtyping,
+          constraints from module type. *)
+      mod_constraints =
+        Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
     let mtb = translate_modtype env mp inl (params,ty) in
     module_body_of_type mp mtb
   |MExpr (params,mse,oty) ->
-    let t = translate_mse_funct env (Some mp) inl mse params in
+    let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
-    finalize_module env mp t restype
+    finalize_module env mp (sg,Some alg,reso,cst) restype
+
+(** We now forbid any Include of functors with restricted signatures.
+    Otherwise, we could end with the creation of undesired axioms
+    (see #3746). Note that restricted non-functorized modules are ok,
+    thanks to strengthening. *)
+
+let rec unfunct = function
+  |NoFunctor me -> me
+  |MoreFunctor(_,_,me) -> unfunct me
+
+let rec forbid_incl_signed_functor env = function
+  |MEapply(fe,_) -> forbid_incl_signed_functor env fe
+  |MEwith _ -> assert false (* No 'with' syntax for modules *)
+  |MEident mp1 ->
+    let mb = lookup_module mp1 env in
+    match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
+    |MoreFunctor _, Some _, _ ->
+      (* functor + restricted signature = error *)
+      error_include_restricted_functor mp1
+    |MoreFunctor _, None, Algebraic me ->
+      (* functor, no signature yet, a definition which may be restricted *)
+      forbid_incl_signed_functor env (unfunct me)
+    |_ -> ()
 
 let rec translate_mse_inclmod env mp inl = function
   |MEident mp1 ->
     let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr mb.mod_type in
-    sign,None,mb.mod_delta,Univ.ContextSet.empty
+    sign,(),mb.mod_delta,Univ.ContextSet.empty
   |MEapply (fe,arg) ->
     let ftrans = translate_mse_inclmod env mp inl fe in
-    translate_apply env inl ftrans arg (fun _ _ -> None)
+    translate_apply env inl ftrans arg (fun _ _ -> ())
   |MEwith _ -> assert false (* No 'with' syntax for modules *)
 
 let translate_mse_incl is_mod env mp inl me =
   if is_mod then
+    let () = forbid_incl_signed_functor env me in
     translate_mse_inclmod env mp inl me
   else
     let mtb = translate_modtype env mp inl ([],me) in
     let sign = clean_bounded_mod_expr mtb.mod_type in
-    sign,None,mtb.mod_delta,mtb.mod_constraints
+    sign,(),mtb.mod_delta,mtb.mod_constraints
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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index cbb796331..341c3993a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,15 +67,13 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
+  | IncludeRestrictedFunctor of module_path
 
 exception ModuleTypingError of module_typing_error
 
 let error_existing_label l =
   raise (ModuleTypingError (LabelAlreadyDeclared l))
 
-let error_application_to_not_path mexpr =
-  raise (ModuleTypingError (ApplicationToNotPath mexpr))
-
 let error_not_a_functor () =
   raise (ModuleTypingError NotAFunctor)
 
@@ -112,6 +110,9 @@ let error_generative_module_expected l =
 let error_no_such_label_sub l l1 =
   raise (ModuleTypingError (LabelMissing (l,l1)))
 
+let error_include_restricted_functor mp =
+  raise (ModuleTypingError (IncludeRestrictedFunctor mp))
+
 (** {6 Operations on functors } *)
 
 let is_functor = function
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a335ad9b4..86aae598c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,13 +126,12 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
+  | IncludeRestrictedFunctor of module_path
 
 exception ModuleTypingError of module_typing_error
 
 val error_existing_label : Label.t -> 'a
 
-val error_application_to_not_path : module_struct_entry -> 'a
-
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
@@ -152,3 +151,5 @@ val error_incorrect_with_constraint : Label.t -> 'a
 val error_generative_module_expected : Label.t -> 'a
 
 val error_no_such_label_sub : Label.t->string->'a
+
+val error_include_restricted_functor : module_path -> 'a
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e0a07dcc3..036555309 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -746,7 +746,7 @@ let end_modtype l senv =
 let add_include me is_module inl senv =
   let open Mod_typing in
   let mp_sup = senv.modpath in
-  let sign,_,resolver,cst =
+  let sign,(),resolver,cst =
     translate_mse_incl is_module senv.env mp_sup inl me
   in
   let senv = add_constraints (Now (false, cst)) senv in