Fix more cases of zero_alloc / modality variables getting into sign…

…atures (#2827)

ocaml/testsuite/tests/typing-zero-alloc/signatures.ml

@@ -1225,3 +1225,117 @@ module N :
     module type S_plain = sig module M : sig val f : int -> int end end
   end
 |}]
+
+(******************************************)
+(* Test 15: destructive type substitution *)
+
+module M_outer = struct
+  module M_inner = struct
+    type t
+    let f () = () (* this has a zero_alloc variable (and a modality variable) *)
+  end
+end
+
+(* In [M_outer_strong], the type of [M_inner] will be
+   [Mty_alias M_outer.M_inner] *)
+module type M_outer_strong = sig
+  module M_inner = M_outer.M_inner
+end
+
+(* As a result of the destructive substition, we'll eliminate the alias.  When
+   this happens, we shouldn't keep the zero_alloc variables on [f] *)
+module type M_outer_subst = M_outer_strong
+  with type M_inner.t := M_outer.M_inner.t
+
+(* If we had kept the zero_alloc or modality variables, this would give an
+   error. *)
+module M : M_outer_subst = struct
+  module M_inner = struct
+    let f () = ()
+  end
+end
+[%%expect{|
+module M_outer : sig module M_inner : sig type t val f : unit -> unit end end
+module type M_outer_strong = sig module M_inner = M_outer.M_inner end
+module type M_outer_subst =
+  sig module M_inner : sig val f : unit -> unit end end
+module M : M_outer_subst
+|}]
+
+(********************************************)
+(* Test 16: destructive module substitution *)
+
+module M_outer = struct
+  module M_inner = struct
+    module M_innest = struct end
+    let f () = () (* this has a zero_alloc variable (and a modality variable) *)
+  end
+end
+
+(* In [M_outer_strong], the type of [M_inner] will be
+   [Mty_alias M_outer.M_inner] *)
+module type S_outer_strong = sig
+  module M_inner = M_outer.M_inner
+end
+
+(* As a result of the destructive substition, we'll eliminate the alias.  When
+   this happens, we shouldn't keep the zero_alloc variables on [f] *)
+module type S_outer_subst = S_outer_strong
+  with module M_inner.M_innest := M_outer.M_inner.M_innest
+
+(* If we had kept the zero_alloc or modality variables, this would give an
+   error. *)
+module M : S_outer_subst = struct
+  module M_inner = struct
+    let f () = ()
+  end
+end
+[%%expect{|
+module M_outer :
+  sig
+    module M_inner : sig module M_innest : sig end val f : unit -> unit end
+  end
+module type S_outer_strong = sig module M_inner = M_outer.M_inner end
+module type S_outer_subst =
+  sig module M_inner : sig val f : unit -> unit end end
+module M : S_outer_subst
+|}]
+
+(*************************************************)
+(* Test 17: destructive module type substitution *)
+
+module M_outer = struct
+  module M_inner = struct
+    module type S = sig end
+    let f () = () (* this has a zero_alloc variable (and a modality variable *)
+  end
+end
+
+(* In [M_outer_strong], the type of [M_inner] will be
+   [Mty_alias M_outer.M_inner] *)
+module type S_outer_strong = sig
+  module M_inner = M_outer.M_inner
+end
+
+(* As a result of the destructive substition, we'll eliminate the alias.  When
+   this happens, we shouldn't keep the zero_alloc variables on [f] *)
+module type S_outer_subst = S_outer_strong
+  with module type M_inner.S := M_outer.M_inner.S
+
+(* If we had kept the zero_alloc or modality variables, this would give an
+   error. *)
+module M : S_outer_subst = struct
+  module M_inner = struct
+    let f () = ()
+  end
+end
+[%%expect{|
+module M_outer :
+  sig
+    module M_inner : sig module type S = sig end val f : unit -> unit end
+  end
+module type S_outer_strong = sig module M_inner = M_outer.M_inner end
+module type S_outer_subst =
+  sig module M_inner : sig val f : unit -> unit end end
+module M : S_outer_subst
+|}]

ocaml/tools/debug_printers.ml

@@ -6,3 +6,4 @@ let ctype_global_state = Ctype.print_global_state
 let sort = Jkind.Sort.Debug_printers.t
 let sort_var = Jkind.Sort.Debug_printers.var
 let jkind = Jkind.Debug_printers.t
+let zero_alloc_var = Zero_alloc.debug_printer

ocaml/typing/typemod.ml

@@ -827,6 +827,13 @@ let merge_constraint initial_env loc sg lid constr =
         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 newsg =
+          if destructive_substitution then
+            remove_modality_and_zero_alloc_variables_sg sig_env
+              ~zap_modality:Mode.Modality.Value.zap_to_id newsg
+          else
+            newsg
+        in
         let path = path_concat id path in
         real_ids := path :: !real_ids;
         let item =

ocaml/typing/zero_alloc.ml

@@ -37,6 +37,24 @@ type t =
   | Const of const
   | Var of var
 
+let debug_printer ppf t =
+  let head c = match c with
+    | Default_zero_alloc -> "Default"
+    | Ignore_assert_all -> "Ignore"
+    | Check _ -> "Check"
+    | Assume _ -> "Assume"
+  in
+  match t with
+  | Const c -> Format.fprintf ppf "Const %s" (head c)
+  | Var v ->
+    let print_desc ppf desc =
+      match desc with
+      | None -> Format.fprintf ppf "None"
+      | Some desc ->
+        Format.fprintf ppf "{ strict = %b; opt = %b }" desc.strict desc.opt
+    in
+    Format.fprintf ppf "Var { arity = %d; desc = %a }" v.arity print_desc v.desc
+
 (* For backtracking *)
 type change = desc option * var
 let undo_change (d, v) = v.desc <- d

ocaml/typing/zero_alloc.mli

@@ -53,3 +53,5 @@ val print_error : Format.formatter -> error -> unit
    zero_alloc check t2. It returns [Ok ()] if so, and [Error e] if not.  If [t1]
    is a variable, it may be set to make the relation hold. *)
 val sub : t -> t -> (unit, error) Result.t
+
+val debug_printer : Format.formatter -> t -> unit