Ensure that types from packed modules are always generalised (#11732)

Changes

@@ -221,6 +221,9 @@ Working version
   currying optimisation accidentally disabled by #10340.
   (Stephen Dolan, review by Gabriel Scherer)
 
+- #11732: Ensure that types from packed modules are always generalised
+  (Stephen Dolan and Leo White, review by Jacques Garrigue)
+
 OCaml 5.0
 ---------
 

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>
+|}]

typing/typemod.ml

@@ -2038,9 +2038,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