Merge pull request #10382 from lpw25/clean-envs-check-type-decl

Don't repeat environment entries in Typemod.check_type_decl

Changes

@@ -178,6 +178,9 @@ Working version
   type
   (Nicolas Chataing, review by Gabriel Scherer)
 
+- #10382: Don't repeat environment entries in Typemod.check_type_decl
+  (Leo White, review by Gabriel Scherer and Florian Angeletti)
+
 - #10472: refactor caml_sys_random_seed to ease future Multicore changes
   (Gabriel Scherer, review by Xavier Leroy)
 

testsuite/tests/shadow_include/cannot_shadow_error.compilers.reference

@@ -1,7 +1,7 @@
 File "cannot_shadow_error.ml", line 24, characters 2-36:
 24 |   include Comparable with type t = t
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: Illegal shadowing of included type t/9 by t/13
+Error: Illegal shadowing of included type t/9 by t/14
        File "cannot_shadow_error.ml", line 23, characters 2-19:
          Type t/9 came from this include
        File "cannot_shadow_error.ml", line 14, characters 2-23:

testsuite/tests/typing-modules/merge_constraint.ml

@@ -246,3 +246,177 @@ module type Weird =
     module P : sig module M : sig type t = M.t type u = M.u end end
   end
 |}]
+
+(* Recursion issues *)
+
+(* Should fail rather than stack overflow *)
+module type S = sig
+    type 'a t = 'a
+      constraint 'a = < m : r >
+    and r = (< m : r >) t
+  end
+
+module type T = S with type 'a t = 'b constraint 'a = < m : 'b >;;
+[%%expect{|
+module type S =
+  sig type 'a t = 'a constraint 'a = < m : r > and r = < m : r > t end
+Uncaught exception: Stack overflow
+
+|}]
+
+(* Correct *)
+module type S = sig
+    type t = Foo of r
+    and r = t
+  end
+
+type s = Foo of s
+
+module type T = S with type t = s
+[%%expect{|
+module type S = sig type t = Foo of r and r = t end
+type s = Foo of s
+module type T = sig type t = s = Foo of r and r = t end
+|}]
+
+(* Correct *)
+module type S = sig
+    type r = t
+    and t = Foo of r
+  end
+
+type s = Foo of s
+
+module type T = S with type t = s
+[%%expect{|
+module type S = sig type r = t and t = Foo of r end
+type s = Foo of s
+module type T = sig type r = t and t = s = Foo of r end
+|}]
+
+(* Should succeed *)
+module type S = sig
+    module rec M : sig
+      type t = Foo of M.r
+      type r = t
+    end
+  end
+
+type s = Foo of s
+
+module type T = S with type M.t = s
+[%%expect{|
+module type S = sig module rec M : sig type t = Foo of M.r type r = t end end
+type s = Foo of s
+Line 10, characters 23-35:
+10 | module type T = S with type M.t = s
+                            ^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type s
+       Constructors do not match:
+         Foo of s
+       is not the same as:
+         Foo of M.r
+       The type s is not equal to the type M.r = M.t
+|}]
+
+(* Should succeed *)
+module type S = sig
+    module rec M : sig
+      type t = private [`Foo of M.r]
+      type r = t
+    end
+  end
+
+type s = [`Foo of s]
+
+module type T = S with type M.t = s
+[%%expect{|
+module type S =
+  sig module rec M : sig type t = private [ `Foo of M.r ] type r = t end end
+type s = [ `Foo of s ]
+Line 10, characters 16-35:
+10 | module type T = S with type M.t = s
+                     ^^^^^^^^^^^^^^^^^^^
+Error: In this `with' constraint, the new definition of M.t
+       does not match its original definition in the constrained signature:
+       Type declarations do not match:
+         type t = s
+       is not included in
+         type t = private [ `Foo of M.r ]
+       The type s = [ `Foo of s ] is not equal to the type [ `Foo of M.r ]
+       Type s = [ `Foo of s ] is not equal to type M.r = M.t
+       Types for tag `Foo are incompatible
+|}]
+
+(* Should succeed *)
+module type S = sig
+  module rec M : sig
+    module N : sig type t = private [`Foo of M.r] end
+    type r = M.N.t
+  end
+end
+
+module X = struct type t = [`Foo of t] end
+
+module type T = S with module M.N = X
+[%%expect{|
+module type S =
+  sig
+    module rec M :
+      sig
+        module N : sig type t = private [ `Foo of M.r ] end
+        type r = M.N.t
+      end
+  end
+module X : sig type t = [ `Foo of t ] end
+Line 10, characters 16-37:
+10 | module type T = S with module M.N = X
+                     ^^^^^^^^^^^^^^^^^^^^^
+Error: In this `with' constraint, the new definition of M.N
+       does not match its original definition in the constrained signature:
+       Modules do not match:
+         sig type t = [ `Foo of t ] end
+       is not included in
+         sig type t = private [ `Foo of M.r ] end
+       Type declarations do not match:
+         type t = [ `Foo of t ]
+       is not included in
+         type t = private [ `Foo of M.r ]
+       The type [ `Foo of t ] is not equal to the type [ `Foo of M.r ]
+       Type t = [ `Foo of t ] is not equal to type M.r = M.N.t
+       Types for tag `Foo are incompatible
+|}]
+
+(* Should succeed *)
+module type S = sig
+    module rec M : sig
+      module N : sig type t = M.r type s end
+      type r = N.s
+    end
+  end
+
+module X = struct type t type s = t end
+
+module type T = S with module M.N = X
+[%%expect{|
+module type S =
+  sig
+    module rec M :
+      sig module N : sig type t = M.r type s end type r = N.s end
+  end
+module X : sig type t type s = t end
+Line 10, characters 16-37:
+10 | module type T = S with module M.N = X
+                     ^^^^^^^^^^^^^^^^^^^^^
+Error: In this `with' constraint, the new definition of M.N
+       does not match its original definition in the constrained signature:
+       Modules do not match:
+         sig type t = X.t type s = t end
+       is not included in
+         sig type t = M.r type s end
+       Type declarations do not match:
+         type t = X.t
+       is not included in
+         type t = M.r
+       The type X.t is not equal to the type M.r = M.N.s
+|}]

testsuite/tests/typing-sigsubst/sigsubst.ml

@@ -24,7 +24,7 @@ end
 Line 3, characters 2-36:
 3 |   include Comparable with type t = t
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: Illegal shadowing of included type t/100 by t/104
+Error: Illegal shadowing of included type t/100 by t/105
        Line 2, characters 2-19:
          Type t/100 came from this include
        Line 3, characters 2-23:

typing/signature_group.ml

@@ -133,7 +133,7 @@ let replace_in_place f sg =
     match current with
     | [] -> next_group f (commit ghosts) sg
     | a :: q ->
-        match f ~rec_group:q ~ghosts a.src with
+        match f ~ghosts a.src with
         | Some (info, {ghosts; replace_by}) ->
             let after = List.concat_map flatten q @ sg in
             let after = match recursive_sigitem a.src, replace_by with

typing/signature_group.mli

@@ -80,6 +80,6 @@ type in_place_patch = {
    [component]
 *)
 val replace_in_place:
-  ( rec_group:sig_item list -> ghosts:Types.signature -> Types.signature_item
+  ( ghosts:Types.signature -> Types.signature_item
     -> ('a * in_place_patch) option )
   -> Types.signature -> ('a * Types.signature) option

typing/typemod.ml

@@ -240,20 +240,30 @@ let check_recmod_typedecls env decls =
 
 (* Merge one "with" constraint in a signature *)
 
-let check_type_decl env loc id row_id newdecl decl rec_group =
-  let env = Env.add_type ~check:true id newdecl env in
-  let env =
+let check_type_decl env sg loc id row_id newdecl decl =
+  let fresh_id = Ident.rename id in
+  let path = Pident fresh_id in
+  let sub = Subst.add_type id path Subst.identity in
+  let fresh_row_id, sub =
     match row_id with
-    | None -> env
-    | Some id -> Env.add_type ~check:false id newdecl env
+    | None -> None, sub
+    | Some id ->
+      let fresh_row_id = Some (Ident.rename id) in
+      let sub = Subst.add_type id (Pident fresh_id) sub in
+      fresh_row_id, sub
   in
+  let newdecl = Subst.type_declaration sub newdecl in
+  let decl = Subst.type_declaration sub decl in
+  let sg = List.map (Subst.signature_item Keep sub) sg in
+  let env = Env.add_type ~check:false fresh_id newdecl env in
   let env =
-    let add_sigitem env x =
-      Env.add_signature Signature_group.(x.src :: x.post_ghosts) env
-    in
-    List.fold_left add_sigitem env rec_group in
-  Includemod.type_declarations ~mark:Mark_both ~loc env id newdecl decl;
-  Typedecl.check_coherence env loc (Path.Pident id) newdecl
+    match fresh_row_id with
+    | None -> env
+    | Some fresh_row_id -> Env.add_type ~check:false fresh_row_id newdecl env
+  in
+  let env = Env.add_signature sg env in
+  Includemod.type_declarations ~mark:Mark_both ~loc env fresh_id newdecl decl;
+  Typedecl.check_coherence env loc path newdecl
 
 let make_variance p n i =
   let open Variance in
@@ -508,7 +518,7 @@ let merge_constraint initial_env loc sg lid constr =
     in
     split [] ghosts
   in
-  let rec patch_item constr namelist sig_env ~rec_group ~ghosts item =
+  let rec patch_item constr namelist outer_sig_env sg_for_env ~ghosts item =
     let return ?(ghosts=ghosts) ~replace_by info =
       Some (info, {Signature_group.ghosts; replace_by})
     in
@@ -551,13 +561,14 @@ let merge_constraint initial_env loc sg lid constr =
         let initial_env =
           Env.add_type ~check:false id_row decl_row initial_env
         in
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let tdecl =
           Typedecl.transl_with_constraint id ~fixed_row_path:(Pident id_row)
             ~sig_env ~sig_decl:decl ~outer_env:initial_env sdecl in
         let newdecl = tdecl.typ_type in
         let before_ghosts, row_id, after_ghosts = split_row_id s ghosts in
-        check_type_decl sig_env sdecl.ptype_loc id row_id newdecl decl
-          rec_group;
+        check_type_decl outer_sig_env sg_for_env sdecl.ptype_loc
+          id row_id newdecl decl;
         let decl_row = {decl_row with type_params = newdecl.type_params} in
         let rs' = if rs = Trec_first then Trec_not else rs in
         let ghosts =
@@ -570,13 +581,15 @@ let merge_constraint initial_env loc sg lid constr =
     | Sig_type(id, sig_decl, rs, priv) , [s],
        (With_type sdecl | With_typesubst sdecl as constr)
       when Ident.name id = s ->
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let tdecl =
           Typedecl.transl_with_constraint id
             ~sig_env ~sig_decl ~outer_env:initial_env sdecl in
         let newdecl = tdecl.typ_type and loc = sdecl.ptype_loc in
         let before_ghosts, row_id, after_ghosts = split_row_id s ghosts in
         let ghosts = List.rev_append before_ghosts after_ghosts in
-        check_type_decl sig_env loc id row_id newdecl sig_decl rec_group;
+        check_type_decl outer_sig_env sg_for_env loc
+          id row_id newdecl sig_decl;
         begin match constr with
           With_type _ ->
             return ~ghosts
@@ -590,6 +603,7 @@ let merge_constraint initial_env loc sg lid constr =
     | Sig_modtype(id, mtd, priv), [s],
       (With_modtype mty | With_modtypesubst mty)
       when Ident.name id = s ->
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let () = match mtd.mtd_type with
           | None -> ()
           | Some previous_mty ->
@@ -620,6 +634,7 @@ let merge_constraint initial_env loc sg lid constr =
     | Sig_module(id, pres, md, rs, priv), [s],
       With_module {lid=lid'; md=md'; path; remove_aliases}
       when Ident.name id = s ->
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let mty = md'.md_type in
         let mty = Mtype.scrape_for_type_of ~remove_aliases sig_env mty in
         let md'' = { md' with md_type = mty } in
@@ -631,6 +646,7 @@ let merge_constraint initial_env loc sg lid constr =
           (Pident id, lid, Twith_module (path, lid'))
     | Sig_module(id, _, md, _rs, _), [s], With_modsubst (lid',path,md')
       when Ident.name id = s ->
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let aliasable = not (Env.is_functor_arg path sig_env) in
         ignore
           (Includemod.strengthened_module_decl ~loc ~mark:Mark_both
@@ -639,6 +655,7 @@ let merge_constraint initial_env loc sg lid constr =
         return ~replace_by:None (Pident id, lid, Twith_modsubst (path, lid'))
     | Sig_module(id, _, md, rs, priv) as item, s :: namelist, constr
       when Ident.name id = s ->
+        let sig_env = Env.add_signature sg_for_env outer_sig_env in
         let sg = extract_sig sig_env loc md.md_type in
         let ((path, _, tcstr), newsg) = merge_signature sig_env sg namelist in
         let path = path_concat id path in
@@ -656,12 +673,11 @@ let merge_constraint initial_env loc sg lid constr =
         return ~replace_by:(Some item) (path, lid, tcstr)
     | _ -> None
   and merge_signature env sg namelist =
-    let sig_env = Env.add_signature sg env in
     match
-      Signature_group.replace_in_place (patch_item constr namelist sig_env) sg
+      Signature_group.replace_in_place (patch_item constr namelist env sg) sg
     with
     | Some (x,sg) -> x, sg
-    | None -> raise(Error(loc, sig_env, With_no_component lid.txt))
+    | None -> raise(Error(loc, env, With_no_component lid.txt))
   in
   try
     let names = Longident.flatten lid.txt in