Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)

3 files changed, 19 insertions, 16 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index eef83ce74..c03c5175f 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -351,12 +351,20 @@ let translate_module env mp inl = function
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
     finalize_module env mp t restype
 
-let rec translate_mse_incl env mp inl = function
+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
   |MEapply (fe,arg) ->
-    let ftrans = translate_mse_incl env mp inl fe in
+    let ftrans = translate_mse_inclmod env mp inl fe in
     translate_apply env inl ftrans arg (fun _ _ -> None)
   |MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let translate_mse_incl is_mod env mp inl me =
+  if is_mod then
+    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
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0c3fb2ba7..bc0e20205 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -36,14 +36,14 @@ val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
-(** [translate_mse_incl] translate the mse of a real module (no
-    module type here) given to an Include *)
-
-val translate_mse_incl :
-  env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
-
 val finalize_module :
   env -> module_path -> module_expression translation ->
   (module_type_entry * inline) option ->
   module_body
+
+(** [translate_mse_incl] translate the mse of a module or
+    module type given to an Include *)
+
+val translate_mse_incl :
+  bool -> env -> module_path -> inline -> module_struct_entry ->
+    module_alg_expr translation
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fdacbb365..ec245b064 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,13 +682,8 @@ 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,cst,resolver =
-    if is_module then
-      let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
-      sign,cst,reso
-    else
-      let mtb = translate_modtype senv.env mp_sup inl ([],me) in
-      mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
+  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
   (* Include Self support  *)