properly scope idents

- when including: the elements are rescoped to the current level (as
well as being given a fresh stamp, which was already the case)
- extension constructors idents cannot be local: they can be used as
types when the constructor's argument is an inlined record. They must be
given a scope
- in check_recmod_inclusion: create a new scope at each iteration
- when checking that type declarations inside recursive modules are well
founded, we now take a generic instance of the declaration (this is
reminiscent of what is done in Ctype.moregeneral)

Author: trefis

typing/ctype.ml

@@ -1192,6 +1192,13 @@ let instance_declaration decl =
   cleanup_types ();
   decl
 
+let generic_instance_declaration decl =
+  let old = !current_level in
+  current_level := generic_level;
+  let decl = instance_declaration decl in
+  current_level := old;
+  decl
+
 let instance_class params cty =
   let rec copy_class_type =
     function

typing/ctype.mli

@@ -130,6 +130,8 @@ val instance_parameterized_type_2:
         type_expr list -> type_expr list -> type_expr ->
         type_expr list * type_expr list * type_expr
 val instance_declaration: type_declaration -> type_declaration
+val generic_instance_declaration: type_declaration -> type_declaration
+        (* Same as instance_declaration, but new nodes at generic_level *)
 val instance_class:
         type_expr list -> class_type -> type_expr list * class_type
 val instance_poly:

typing/subst.ml

@@ -439,6 +439,7 @@ and signature s sg =
   (* ... then apply it to each signature component in turn *)
   List.map2 (signature_component s') sg new_idents
 
+
 and signature_component s comp newid =
   match comp with
     Sig_value(_id, d) ->
@@ -470,6 +471,33 @@ and modtype_declaration s decl  =
     mtd_loc = loc s decl.mtd_loc;
   }
 
+(* Same as [signature] except than instead of making the items local, we rescope
+   them. *)
+let refresh_signature ~scope sg =
+  let rec refresh_bound_idents s idents = function
+      [] -> (List.rev idents, s)
+    | Sig_type(id, _, _) :: sg ->
+        let id' = Ident.create_scoped ~scope (Ident.name id) in
+        refresh_bound_idents (add_type id (Pident id') s) (id' :: idents) sg
+    | Sig_module(id, _, _) :: sg ->
+        let id' = Ident.create_scoped ~scope (Ident.name id) in
+        refresh_bound_idents (add_module id (Pident id') s) (id' :: idents) sg
+    | Sig_modtype(id, _) :: sg ->
+        let id' = Ident.create_scoped ~scope (Ident.name id) in
+        refresh_bound_idents (add_modtype id (Mty_ident(Pident id')) s)
+                            (id' :: idents) sg
+    | (Sig_class(id, _, _) | Sig_class_type(id, _, _)) :: sg ->
+        (* cheat and pretend they are types cf. PR#6650 *)
+        let id' = Ident.create_scoped ~scope (Ident.name id) in
+        refresh_bound_idents (add_type id (Pident id') s) (id' :: idents) sg
+    | (Sig_value(id, _) | Sig_typext(id, _, _)) :: sg ->
+        let id' = Ident.create_scoped ~scope (Ident.name id) in
+        refresh_bound_idents s (id' :: idents) sg
+  in
+  let (new_idents, s') = refresh_bound_idents identity [] sg in
+  List.map2 (signature_component s') sg new_idents
+
+
 (* For every binding k |-> d of m1, add k |-> f d to m2
    and return resulting merged map. *)
 

typing/subst.mli

@@ -61,6 +61,8 @@ val modtype_declaration: t -> modtype_declaration -> modtype_declaration
 val module_declaration: t -> module_declaration -> module_declaration
 val class_signature: t -> class_signature -> class_signature
 
+val refresh_signature: scope:int -> signature -> signature
+
 (* Composition of substitutions:
      apply (compose s1 s2) x = apply s2 (apply s1 x) *)
 val compose: t -> t -> t

typing/typedecl.ml

@@ -775,7 +775,7 @@ let check_well_founded_decl env loc path decl to_check =
   let it =
     {type_iterators with
      it_type_expr = (fun _ -> check_well_founded env loc path to_check)} in
-  it.it_type_declaration it (Ctype.instance_declaration decl)
+  it.it_type_declaration it (Ctype.generic_instance_declaration decl)
 
 (* Check for ill-defined abbrevs *)
 
@@ -1411,7 +1411,8 @@ let transl_type_decl env rec_flag sdecl_list =
 
 let transl_extension_constructor env type_path type_params
                                  typext_params priv sext =
-  let id = Ident.create_local sext.pext_name.txt in
+  let scope = Ctype.get_current_level () in
+  let id = Ident.create_scoped ~scope sext.pext_name.txt in
   let args, ret_type, kind =
     match sext.pext_kind with
       Pext_decl(sargs, sret_type) ->

typing/typemod.ml

@@ -742,7 +742,7 @@ and approx_sig env ssg =
       | Psig_include sincl ->
           let smty = sincl.pincl_mod in
           let mty = approx_modtype env smty in
-          let sg = Subst.signature Subst.identity
+          let sg = Subst.refresh_signature ~scope:(Ctype.get_current_level ())
               (extract_sig env smty.pmty_loc mty) in
           let newenv = Env.add_signature sg env in
           sg @ approx_sig newenv srem
@@ -1114,7 +1114,7 @@ and transl_signature env sg =
                 (fun () -> transl_modtype env smty)
             in
             let mty = tmty.mty_type in
-            let sg = Subst.signature Subst.identity
+            let sg = Subst.refresh_signature ~scope:(Ctype.get_current_level ())
                        (extract_sig env smty.pmty_loc mty) in
             List.iter
               (fun i -> check_sig_item names item.psig_loc i to_be_removed)
@@ -1403,11 +1403,13 @@ let check_recmodule_inclusion env bindings =
   let rec check_incl first_time n env s =
     if n > 0 then begin
       (* Generate fresh names Y_i for the rec. bound module idents X_i *)
+      let scope = Ctype.get_current_level () in
       let bindings1 =
         List.map
-          (fun (id, _, _mty_decl, _modl, mty_actual, _attrs, _loc) ->
-             (id, Ident.rename id, mty_actual))
+          (fun (id, name, _mty_decl, _modl, mty_actual, _attrs, _loc) ->
+             (id, Ident.create_scoped ~scope name.txt, mty_actual))
           bindings in
+      Ctype.init_def (scope + 1);
       (* Enter the Y_i in the environment with their actual types substituted
          by the input substitution s *)
       let env' =
@@ -1953,7 +1955,7 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
             (fun () -> type_module true funct_body None env smodl)
         in
         (* Rename all identifiers bound by this signature to avoid clashes *)
-        let sg = Subst.signature Subst.identity
+        let sg = Subst.refresh_signature ~scope:(Ctype.get_current_level ())
             (extract_sig_open env smodl.pmod_loc modl.mod_type) in
         List.iter (fun item -> check_sig_item names loc item to_be_removed)
           (List.rev sg);