Fix bug #4661: Cannot mask the absolute name.

The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.

4 files changed, 38 insertions, 6 deletions

diff --git a/printing/printmod.ml b/printing/printmod.ml
index c939f54e80..dfa66d4376 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -247,19 +247,24 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
   | _ -> raise Not_found
 
 let nametab_register_modparam mbid mtb =
+  let id = MBId.to_id mbid in
   match mtb.mod_type with
-  | MoreFunctor _ -> () (* functorial param : nothing to register *)
+  | MoreFunctor _ -> id (* functorial param : nothing to register *)
   | NoFunctor struc ->
     (* We first try to use the algebraic type expression if any,
        via a Declaremods function that converts back to module entries *)
     try
-      Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
+      let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+      id
     with e when CErrors.noncritical e ->
       (* Otherwise, we try to play with the nametab ourselves *)
       let mp = MPbound mbid in
-      let dir = DirPath.make [MBId.to_id mbid] in
+      let check id = Nametab.exists_dir (DirPath.make [id]) in
+      let id = Namegen.next_ident_away_from id check in
+      let dir = DirPath.make [id] in
       nametab_register_dir mp;
-      List.iter (nametab_register_body mp dir) struc
+      List.iter (nametab_register_body mp dir) struc;
+      id
 
 let print_body is_impl env mp (l,body) =
   let name = pr_label l in
@@ -353,7 +358,7 @@ let print_mod_expr env mp locals = function
 let rec print_functor fty fatom is_type env mp locals = function
   |NoFunctor me -> fatom is_type env mp locals me
   |MoreFunctor (mbid,mtb1,me2) ->
-      nametab_register_modparam mbid mtb1;
+      let id = nametab_register_modparam mbid mtb1 in
       let mp1 = MPbound mbid in
       let pr_mtb1 = fty env mp1 locals mtb1 in
       let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
@@ -361,7 +366,7 @@ let rec print_functor fty fatom is_type env mp locals = function
       let kwd = if is_type then "Funsig" else "Functor" in
       hov 2
         (keyword kwd ++ spc () ++
-	 str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++
 	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
 
 let rec print_expression x =
diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v
new file mode 100644
index 0000000000..03d2350a69
--- /dev/null
+++ b/test-suite/bugs/closed/4661.v
@@ -0,0 +1,10 @@
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : Type.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
 
 Module N : S with Module T := K := M
 
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a9862..5f30f7cda6 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
 Print Module N.
 
 End BAR.
+
+Module QUX.
+
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.