From bc510ed522f2f755e3952677feb8578899b8eb33 Mon Sep 17 00:00:00 2001
From: Stephen Dolan <sdolan@janestreet.com>
Date: Thu, 17 Nov 2022 14:33:05 +0000
Subject: [PATCH] Ensure that types from packed modules are always generalised
 (#11732)

(cherry picked from commit bf4a8efe68c95cfc1f85b96add7a46c0d6433fce)
---
 Changes                                       |  3 ++
 .../typing-modules/packed_module_levels.ml    | 42 +++++++++++++++++++
 typing/typemod.ml                             |  4 +-
 3 files changed, 48 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/tests/typing-modules/packed_module_levels.ml

diff --git a/Changes b/Changes
index 619e20fe343..0bf5a3ea290 100644
--- a/Changes
+++ b/Changes
@@ -68,6 +68,9 @@ OCaml 4.14 maintenance branch
   mismatch error involving recursive types.
   (Florian Angeletti, review by Gabriel Scherer)
 
+- #11732: Ensure that types from packed modules are always generalised
+  (Stephen Dolan and Leo White, review by Jacques Garrigue)
+
 - #11737: Fix segfault condition in Unix.stat under Windows in the presence of
   multiple threads.
   (Marc Lasson, Nicolás Ojeda Bär, review by Gabriel Scherer and David Allsopp)
diff --git a/testsuite/tests/typing-modules/packed_module_levels.ml b/testsuite/tests/typing-modules/packed_module_levels.ml
new file mode 100644
index 00000000000..a4883d00deb
--- /dev/null
+++ b/testsuite/tests/typing-modules/packed_module_levels.ml
@@ -0,0 +1,42 @@
+(* TEST
+   * expect
+*)
+type (_, _) equ = Refl : ('q, 'q) equ
+
+module type Ty = sig type t end
+type 'a modu = (module Ty with type t = 'a)
+
+type 'q1 packed =
+    P : 'q0 modu * ('q0, 'q1) equ -> 'q1 packed
+
+(* Adds a module M to the environment where M.t equals an existential *)
+let repack (type q) (x : q packed) : q modu =
+  match x with
+  | P (p, eq) ->
+    let module M = (val p) in
+    let Refl = eq in
+    (module M)
+
+[%%expect{|
+type (_, _) equ = Refl : ('q, 'q) equ
+module type Ty = sig type t end
+type 'a modu = (module Ty with type t = 'a)
+type 'q1 packed = P : 'q0 modu * ('q0, 'q1) equ -> 'q1 packed
+val repack : 'q packed -> 'q modu = <fun>
+|}]
+
+(* Same, using a polymorphic function rather than an existential *)
+
+let mkmod (type a) () : a modu =
+  (module struct type t = a end)
+
+let f (type foo) (intish : (foo, int) equ) =
+  let module M = (val (mkmod () : foo modu)) in
+  let Refl = intish in
+  let module C : sig type t = int end = M in
+  ()
+
+[%%expect{|
+val mkmod : unit -> 'a modu = <fun>
+val f : ('foo, int) equ -> unit = <fun>
+|}]
diff --git a/typing/typemod.ml b/typing/typemod.ml
index f19caace480..b575de29096 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -2048,9 +2048,11 @@ and package_constraints env loc mty constrs =
   end
 
 let modtype_of_package env loc p fl =
+  (* We call Ctype.correct_levels to ensure that the types being added to the
+     module type are at generic_level. *)
   let mty =
     package_constraints env loc (Mty_ident p)
-      (List.map (fun (n, t) -> (Longident.flatten n, t)) fl)
+      (List.map (fun (n, t) -> Longident.flatten n, Ctype.correct_levels t) fl)
   in
   Subst.modtype Keep Subst.identity mty