Integrate changes from upstream review.

ccasin · ccasin · commit 4488fde60e5b · 2024-02-15T17:21:43.000-05:00
diff --git a/ocaml/testsuite/tests/typing-modules/package_constraint.ml b/ocaml/testsuite/tests/typing-modules/package_constraint.ml
@@ -245,3 +245,88 @@ Error: This type string should be an instance of type ('a : immediate)
        But the layout of string must be a sublayout of immediate, because
          of the definition of t at line 5, characters 0-39.
 |}];;
+
+(* Checking such a constraint may require expanding definitions from the module
+   being updated. *)
+module type S = sig
+  module type S1 = sig
+    type t
+  end
+  module M : S1
+end
+
+type t = (module S with type M.t = int)
+[%%expect{|
+module type S = sig module type S1 = sig type t end module M : S1 end
+type t = (module S with type M.t = int)
+|}];;
+
+(* Ghosts haunted type definitions *)
+module type Private_row = sig
+  type a
+  and t = private [< `A | `B ]
+  and b
+  and d = private [< `C ]
+end
+
+(* This is fine, the ghost type `t#row` is removed silently *)
+module type Test = Private_row with type t = [ `A ]
+
+(* This fails currently.  If we ever allow it, make sure the ghost type is
+   removed as above. *)
+type fail = (module Private_row with type t = [ `A ] )
+
+[%%expect{|
+module type Private_row =
+  sig type a and t = private [< `A | `B ] and b and d = private [< `C ] end
+module type Test =
+  sig type a and t = [ `A ] and b and d = private [< `C ] end
+Line 13, characters 12-54:
+13 | type fail = (module Private_row with type t = [ `A ] )
+                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the constrained signature, type t is defined to be [< `A | `B ].
+       Package `with' constraints may only be used on abstract types.
+|}]
+
+(* More row type examples to consider, if we ever start allowing package type
+   constraints to replace compatible manifests. *)
+module type Private_row = sig
+  type t = private [< `A ]
+end
+
+type t1 = (module Private_row with type t = [ `A ])
+[%%expect{|
+module type Private_row = sig type t = private [< `A ] end
+Line 5, characters 10-51:
+5 | type t1 = (module Private_row with type t = [ `A ])
+              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the constrained signature, type t is defined to be [< `A ].
+       Package `with' constraints may only be used on abstract types.
+|}]
+
+type t2 = (module Private_row with type t = [< `A ])
+[%%expect{|
+Line 1, characters 10-52:
+1 | type t2 = (module Private_row with type t = [< `A ])
+              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the constrained signature, type t is defined to be [< `A ].
+       Package `with' constraints may only be used on abstract types.
+|}]
+
+type 'a t3 = (module Private_row with type t = [< `A ]) as 'a
+[%%expect{|
+Line 1, characters 13-55:
+1 | type 'a t3 = (module Private_row with type t = [< `A ]) as 'a
+                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the constrained signature, type t is defined to be [< `A ].
+       Package `with' constraints may only be used on abstract types.
+|}]
+
+type 'a t4 = (module Private_row with type t = [< `A ] as 'a)
+[%%expect{|
+Line 1, characters 13-61:
+1 | type 'a t4 = (module Private_row with type t = [< `A ] as 'a)
+                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the constrained signature, type t is defined to be [< `A ].
+       Package `with' constraints may only be used on abstract types.
+|}]
diff --git a/ocaml/typing/typemod.ml b/ocaml/typing/typemod.ml
@@ -552,11 +552,15 @@ type with_info =
   | With_modsubst of Longident.t loc * Path.t * Types.module_declaration
   | With_modtype of Typedtree.module_type
   | With_modtypesubst of Typedtree.module_type
+  | With_type_package of Typedtree.core_type
+    (* Package with type constraints only use this last case.  Normal module
+       with constraints never use it. *)
 
 let merge_constraint initial_env loc sg lid constr =
   let destructive_substitution =
     match constr with
-    | With_type _ | With_module _ | With_modtype _ -> false
+    | With_type _ | With_type_package _ | With_module _
+    | With_modtype _ -> false
     | With_typesubst _ | With_modsubst _ | With_modtypesubst _  -> true
   in
   let real_ids = ref [] in
@@ -634,7 +638,7 @@ let merge_constraint initial_env loc sg lid constr =
         in
         return ~ghosts
           ~replace_by:(Some (Sig_type(id, newdecl, rs, priv)))
-          (Pident id, lid, Twith_type tdecl)
+          (Pident id, lid, Some (Twith_type tdecl))
     | Sig_type(id, sig_decl, rs, priv) , [s],
        (With_type sdecl | With_typesubst sdecl as constr)
       when Ident.name id = s ->
@@ -651,12 +655,47 @@ let merge_constraint initial_env loc sg lid constr =
           With_type _ ->
             return ~ghosts
               ~replace_by:(Some(Sig_type(id, newdecl, rs, priv)))
-              (Pident id, lid, Twith_type tdecl)
+              (Pident id, lid, Some (Twith_type tdecl))
         | (* With_typesubst *) _ ->
             real_ids := [Pident id];
             return ~ghosts ~replace_by:None
-              (Pident id, lid, Twith_typesubst tdecl)
+              (Pident id, lid, Some (Twith_typesubst tdecl))
         end
+    | Sig_type(id, sig_decl, rs, priv), [s], With_type_package cty
+      when Ident.name id = s ->
+        begin match sig_decl.type_manifest with
+        | None -> ()
+        | Some ty ->
+          raise (Error(loc, outer_sig_env, With_package_manifest (lid.txt, ty)))
+        end;
+        let tdecl =
+          Typedecl.transl_package_constraint ~loc cty.ctyp_type
+        in
+        (* Here we constrain the jkind of "with type" manifest by the jkind from
+           the declaration from the original signature.  Note that this is also
+           checked in [check_type_decl], but there it is check, not constrain,
+           which we need here to deal with type variables in package constraints
+           (see tests in [typing-modules/package_constraint.ml]).  *)
+        begin match
+          Ctype.constrain_decl_jkind initial_env tdecl sig_decl.type_jkind
+        with
+        | Ok _-> ()
+        | Error v ->
+          (* This is morally part of the below [check_type_decl], so we give the
+             same error that would be given there for good error messages. *)
+          let err =
+            Includemod.Error.In_Type_declaration(
+              id, Type_declarations
+                    {got=tdecl;
+                     expected=sig_decl;
+                     symptom=Includecore.Jkind v})
+          in
+          raise Includemod.(Error(initial_env, err))
+        end;
+        check_type_decl outer_sig_env sg_for_env loc id None tdecl sig_decl;
+        let tdecl = { tdecl with type_manifest = None } in
+        return ~ghosts ~replace_by:(Some(Sig_type(id, tdecl, rs, priv)))
+          (Pident id, lid, None)
     | Sig_modtype(id, mtd, priv), [s],
       (With_modtype mty | With_modtypesubst mty)
       when Ident.name id = s ->
@@ -678,15 +717,16 @@ let merge_constraint initial_env loc sg lid constr =
           in
           return
             ~replace_by:(Some(Sig_modtype(id, mtd', priv)))
-            (Pident id, lid, Twith_modtype mty)
+            (Pident id, lid, Some (Twith_modtype mty))
         else begin
           let path = Pident id in
           real_ids := [path];
           begin match mty.mty_type with
           | Mty_ident _ -> ()
           | mty -> unpackable_modtype := Some mty
           end;
-          return ~replace_by:None (Pident id, lid, Twith_modtypesubst mty)
+          return ~replace_by:None
+            (Pident id, lid, Some (Twith_modtypesubst mty))
         end
     | Sig_module(id, pres, md, rs, priv), [s],
       With_module {lid=lid'; md=md'; path; remove_aliases}
@@ -700,7 +740,7 @@ let merge_constraint initial_env loc sg lid constr =
                  newmd.md_type md.md_type);
         return
           ~replace_by:(Some(Sig_module(id, pres, newmd, rs, priv)))
-          (Pident id, lid, Twith_module (path, lid'))
+          (Pident id, lid, Some (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
@@ -709,7 +749,8 @@ let merge_constraint initial_env loc sg lid constr =
           (Includemod.strengthened_module_decl ~loc ~mark:Mark_both
              ~aliasable sig_env md' path md);
         real_ids := [Pident id];
-        return ~replace_by:None (Pident id, lid, Twith_modsubst (path, lid'))
+        return ~replace_by:None
+          (Pident id, lid, Some (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
@@ -743,7 +784,7 @@ let merge_constraint initial_env loc sg lid constr =
       check_usage_after_substitution ~loc ~lid initial_env !real_ids
         !unpackable_modtype sg;
     let sub = match tcstr with
-      | (_, _, Twith_typesubst tdecl) ->
+      | (_, _, Some (Twith_typesubst tdecl)) ->
         let how_to_extend_subst =
           let sdecl =
             match constr with
@@ -768,7 +809,7 @@ let merge_constraint initial_env loc sg lid constr =
         let sub = Subst.change_locs Subst.identity loc in
         let sub = List.fold_left how_to_extend_subst sub !real_ids in
         Some sub
-      | (_, _, Twith_modsubst (real_path, _)) ->
+      | (_, _, Some (Twith_modsubst (real_path, _))) ->
         let sub = Subst.change_locs Subst.identity loc in
         let sub =
           List.fold_left
@@ -777,7 +818,7 @@ let merge_constraint initial_env loc sg lid constr =
             !real_ids
         in
         Some sub
-      | (_, _, Twith_modtypesubst tmty) ->
+      | (_, _, Some (Twith_modtypesubst tmty)) ->
           let add s p = Subst.add_modtype_path p tmty.mty_type s in
           let sub = Subst.change_locs Subst.identity loc in
           let sub = List.fold_left add sub !real_ids in
@@ -805,90 +846,15 @@ let merge_constraint initial_env loc sg lid constr =
   with Includemod.Error explanation ->
     raise(Error(loc, initial_env, With_mismatch(lid.txt, explanation)))
 
-(* A simplified version of [merge_constraint] for the case of packages. Package
-   constraints are much simpler - they must be "with type" constraints for types
-   with no parameters and can only update abstract types. *)
 let merge_package_constraint initial_env loc sg lid cty =
-  let rec patch_item namelist outer_sig_env sg_for_env ~ghosts item =
-    let return replace_by =
-      Some ((), {Signature_group.ghosts; replace_by})
-    in
-    match item, namelist with
-    | Sig_type(id, sig_decl, rs, priv) , [s]
-      when Ident.name id = s ->
-        begin match sig_decl.type_manifest with
-        | None -> ()
-        | Some ty ->
-          raise (Error(loc, outer_sig_env, With_package_manifest (lid.txt, ty)))
-        end;
-        let new_sig_decl =
-          Typedecl.transl_package_constraint ~loc cty.ctyp_type
-        in
-        (* Here we constrain the jkind of "with type" manifest by the jkind from
-           the declaration from the original signature.  Note that this is also
-           checked in [check_type_decl], but there it is check, not constrain,
-           which we need here to deal with type variables in package constraints
-           (see tests in [typing-modules/package_constraint.ml]).  *)
-        begin match
-          Ctype.constrain_decl_jkind initial_env new_sig_decl
-            sig_decl.type_jkind
-        with
-        | Ok _-> ()
-        | Error v ->
-          (* This is morally part of the below [check_type_decl], so we give the
-             same error that would be given there for good error messages. *)
-          let err =
-            Includemod.Error.In_Type_declaration(id,
-              Type_declarations
-                {got=new_sig_decl;
-                 expected=sig_decl;
-                 symptom=Includecore.Jkind v})
-          in
-          raise Includemod.(Error(initial_env, err))
-        end;
-        check_type_decl outer_sig_env sg_for_env loc id None
-          new_sig_decl sig_decl;
-        let new_sig_decl = { new_sig_decl with type_manifest = None } in
-        return (Some(Sig_type(id, new_sig_decl, rs, priv)))
-    | Sig_module(id, _, md, rs, priv) as item, s :: namelist
-      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 ((), newsg) = merge_signature sig_env sg namelist in
-        let item =
-          match md.md_type with
-            Mty_alias _ ->
-              (* A module alias cannot be refined, so keep it
-                 and just check that the constraint is correct *)
-              item
-          | _ ->
-              let newmd = {md with md_type = Mty_signature newsg} in
-              Sig_module(id, Mp_present, newmd, rs, priv)
-        in
-        return (Some item)
-    | _ -> None
-  and merge_signature env sg namelist =
-    match
-      Signature_group.replace_in_place (patch_item namelist env sg) sg
-    with
-    | Some (x,sg) -> x, sg
-    | None -> raise(Error(loc, env, With_no_component lid.txt))
-  in
-  try
-    let names = Longident.flatten lid.txt in
-    let (tcstr, sg) = merge_signature initial_env sg names in
-    check_well_formed_module initial_env loc "this instantiated signature"
-      (Mty_signature sg);
-    (tcstr, sg)
-  with Includemod.Error explanation ->
-    raise(Error(loc, initial_env, With_mismatch(lid.txt, explanation)))
+  let _, s = merge_constraint initial_env loc sg lid (With_type_package cty) in
+  s
 
 let check_package_with_type_constraints loc env mty constraints =
   let sg = extract_sig env loc mty in
   let sg =
     List.fold_left
-      (fun sg (lid, cty) ->
-         snd (merge_package_constraint env loc sg lid cty))
+      (fun sg (lid, cty) -> merge_package_constraint env loc sg lid cty)
       sg constraints
   in
   let scope = Ctype.create_scope () in
@@ -1602,8 +1568,10 @@ and transl_with ~loc env remove_aliases (rev_tcstrs,sg) constr =
         let mty = transl_modtype env smty in
         l, With_modtypesubst mty
   in
-  let (tcstr, sg) = merge_constraint env loc sg lid with_info in
-  (tcstr :: rev_tcstrs, sg)
+  let ((path, lid, tcstr), sg) = merge_constraint env loc sg lid with_info in
+  (* Only package with constraints result in None here. *)
+  let tcstr = Option.get tcstr in
+  ((path, lid, tcstr) :: rev_tcstrs, sg)
 
 
 
@@ -3782,8 +3750,8 @@ let report_error ~loc _env = function
         (Path.name p) Printtyp.modtype mty
   | With_package_manifest (lid, ty) ->
       Location.errorf ~loc
-        "@[In the constrained signature, type %a is defined to be %a.@ \
-         Package `with' constraints may only be used on abstract types.@]"
+        "In the constrained signature, type %a is defined to be %a.@ \
+         Package `with' constraints may only be used on abstract types."
         longident lid
         Printtyp.type_expr ty
   | Repeated_name(kind, name) ->
