Lazy strengthening

ocaml/.depend

@@ -1070,6 +1070,7 @@ typing/mode.cmi :
 typing/mtype.cmo : \
     typing/types.cmi \
     typing/subst.cmi \
+    typing/printtyp.cmi \
     typing/path.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
@@ -1082,6 +1083,7 @@ typing/mtype.cmo : \
 typing/mtype.cmx : \
     typing/types.cmx \
     typing/subst.cmx \
+    typing/printtyp.cmx \
     typing/path.cmx \
     parsing/location.cmx \
     typing/ident.cmx \

ocaml/lambda/translmod.ml

@@ -307,7 +307,8 @@ let init_shape id modl =
   let rec init_shape_mod subid loc env mty =
     match Mtype.scrape env mty with
       Mty_ident _
-    | Mty_alias _ ->
+    | Mty_alias _
+    | Mty_strengthen _ ->
         raise (Initialization_failure
                 (Unsafe {reason=Unsafe_module_binding;loc;subid}))
     | Mty_signature sg ->

ocaml/ocamldoc/odoc_env.ml

@@ -211,6 +211,8 @@ let subst_module_type env t =
           Odoc_name.to_path (full_module_type_name env (Odoc_name.from_path p))
         in
         Mty_ident new_p
+    | Mty_strengthen (mt,p,a) ->
+        Mty_strengthen (iter mt,p,a)
     | Mty_alias _
     | Mty_signature _ ->
         t

ocaml/ocamldoc/odoc_print.ml

@@ -55,7 +55,8 @@ let simpl_module_type ?code t =
   let rec iter t =
     match t with
       Mty_ident _
-    | Mty_alias _ -> t
+    | Mty_alias _
+    | Mty_strengthen _ -> t
     | Mty_signature _ ->
         (
          match code with

ocaml/parsing/builtin_attributes.ml

@@ -106,6 +106,7 @@ let builtin_attrs =
   ; "poll"; "ocaml.poll"
   ; "loop"; "ocaml.loop"
   ; "tail_mod_cons"; "ocaml.tail_mod_cons"
+  ; "unaliasable"; "ocaml.unaliasable"
   ]
 
 (* nroberts: When we upstream the builtin-attribute whitelisting, we shouldn't

ocaml/parsing/parser.mly

@@ -2048,6 +2048,9 @@ module_type:
         { Pmty_extension $1 }
     )
     { $1 }
+  | module_type WITH mkrhs(mod_ext_longident)
+      { Jane_syntax.Strengthen.mty_of ~loc:(make_loc $sloc)
+          { mty = $1; mod_id = $3 } }
 ;
 (* A signature, which appears between SIG and END (among other places),
    is a list of signature elements. *)

ocaml/testsuite/tests/shapes/functors.ml

@@ -223,8 +223,8 @@ module Big_to_small1 : B2S = functor (X : Big) -> X
 [%%expect{|
 {
  "Big_to_small1"[module] ->
-     Abs<.40>(X/385, {<.39>
-                      "t"[type] -> X/385<.39> . "t"[type];
+     Abs<.40>(X/383, {<.39>
+                      "t"[type] -> X/383<.39> . "t"[type];
                       });
  }
 module Big_to_small1 : B2S
@@ -234,8 +234,8 @@ module Big_to_small2 : B2S = functor (X : Big) -> struct include X end
 [%%expect{|
 {
  "Big_to_small2"[module] ->
-     Abs<.42>(X/388, {
-                      "t"[type] -> X/388<.41> . "t"[type];
+     Abs<.42>(X/386, {
+                      "t"[type] -> X/386<.41> . "t"[type];
                       });
  }
 module Big_to_small2 : B2S

ocaml/testsuite/tests/typing-modules-bugs/pr7112_bad.compilers.reference

@@ -2,4 +2,4 @@ File "pr7112_bad.ml", line 13, characters 30-31:
 13 | module G (X : F(N).S) : A.S = X
                                    ^
 Error: Signature mismatch:
-       Modules do not match: F(N).S is not included in A.S
+       Modules do not match: (F(N).S with X) is not included in A.S

ocaml/testsuite/tests/typing-modules/functors.ml

@@ -543,7 +543,7 @@ module F : functor (X : a) -> sig type t end
 Line 6, characters 13-19:
 6 |     type t = F(X).t
                  ^^^^^^
-Error: Modules do not match: a/1 is not included in a/2
+Error: Modules do not match: (a/1 with P.X) is not included in a/2
      Line 3, characters 2-15:
        Definition of module type a/1
      Line 1, characters 0-13:
@@ -1237,15 +1237,19 @@ end
 module U = F(PF)(PF)(PF)
 [%%expect {|
 module F :
-  functor (X : sig type witness module type t module M : t end) -> X.t
+  functor (X : sig type witness module type t module M : t end) ->
+    (X.t with X.M)
 module PF :
   sig
     type witness
     module type t =
-      functor (X : sig type witness module type t module M : t end) -> X.t
+      functor (X : sig type witness module type t module M : t end) ->
+        (X.t with X.M)
     module M = F
   end
-module U : PF.t
+module U :
+  functor (X : sig type witness module type t module M : t end) ->
+    (X.t with X.M)
 |}]
 
 module W = F(PF)(PF)(PF)(PF)(PF)(F)
@@ -1267,7 +1271,7 @@ Error: The functor application is ill-typed.
        6. Modules do not match:
             F :
             functor (X : sig type witness module type t module M : t end) ->
-              X.t
+              (X.t with X.M)
           is not included in
             $T6 = sig type witness module type t module M : t end
           Modules do not match:
@@ -1527,7 +1531,7 @@ Error: Signature mismatch:
              sig type wrong end ->
                functor (X : sig module type T end) (Res : X.T) (Res :
                  X.T) (Res : X.T)
-               -> X.T
+               -> (X.T with Res)
          end
        is not included in
          sig
@@ -1657,7 +1661,7 @@ module type Ext = sig module type T module X : T end
 module AExt : sig module type T = A module X = A end
 module FiveArgsExt :
   sig module type T = ty -> ty -> ty -> ty -> ty -> sig end module X : T end
-module Bar : functor (W : A) (X : Ext) (Y : B) (Z : Ext) -> Z.T
+module Bar : functor (W : A) (X : Ext) (Y : B) (Z : Ext) -> (Z.T with Z.X)
 type fine = Bar(A)(FiveArgsExt)(B)(AExt).a
 |}]
 
@@ -1745,3 +1749,28 @@ module Shape_arg :
     module M4 : functor (Arg5 : sig end) -> M3(Arg5).S3
   end
 |}]
+
+module F (X : sig module type S module M : S end) = struct
+  module N = X.M
+end
+
+module G (X : sig module type S module M : S end) = struct
+  module O = F(X)
+end
+
+module A = struct
+  module type S = sig type t end
+  module M = struct type t end
+end
+
+module B = G(A)
+[%%expect{|
+module F :
+  functor (X : sig module type S module M : S end) ->
+    sig module N : (X.S with X.M) end
+module G :
+  functor (X : sig module type S module M : S end) ->
+    sig module O : sig module N : (X.S with X.M) end end
+module A : sig module type S = sig type t end module M : sig type t end end
+module B : sig module O : sig module N : sig type t = A.M.t end end end
+|}]