Lazy strengthening

lambda/translmod.ml

@@ -274,7 +274,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 ->

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

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

parsing/ast_helper.ml

@@ -242,6 +242,32 @@ module Mty = struct
   let with_ ?loc ?attrs a b = mk ?loc ?attrs (Pmty_with (a, b))
   let typeof_ ?loc ?attrs a = mk ?loc ?attrs (Pmty_typeof a)
   let extension ?loc ?attrs a = mk ?loc ?attrs (Pmty_extension a)
+
+  let strengthen mty lid =
+    let loc = mty.pmty_loc in
+    let mt =
+      { pmty_desc = Pmty_with (mty, [Pwith_module (lid,lid)]);
+        pmty_attributes = [];
+        pmty_loc = loc
+      }
+    in
+    let md =
+      { pmd_name = Location.mknoloc None;
+        pmd_type = mt;
+        pmd_attributes = [];
+        pmd_loc = loc
+      }
+    in
+    let payload = PSig [{psig_desc = Psig_module md; psig_loc = loc}] in
+    Pmty_extension (Location.mknoloc "strengthen", payload)
+
+  let unstrengthen = function
+    | {pmty_desc =
+        Pmty_extension (str, PSig [{psig_desc =
+          Psig_module {pmd_type = {pmty_desc =
+            Pmty_with (mty, [Pwith_module (_,lid)])}}}])}
+      when str.txt = "strengthen" -> Some (mty, lid)
+    | _ -> None
 end
 
 module Mod = struct

parsing/ast_helper.mli

@@ -260,6 +260,10 @@ module Mty:
       with_constraint list -> module_type
     val typeof_: ?loc:loc -> ?attrs:attrs -> module_expr -> module_type
     val extension: ?loc:loc -> ?attrs:attrs -> extension -> module_type
+
+    (* Hack to deal with the strengthening syntax (`S with M`) *)
+    val strengthen: module_type -> lid -> module_type_desc
+    val unstrengthen: module_type -> (module_type * lid) option
   end
 
 (** Module expressions *)

parsing/parser.mly

@@ -1754,6 +1754,8 @@ module_type:
         { Pmty_functor(Named (mknoloc None, $1), $3) }
     | module_type WITH separated_nonempty_llist(AND, with_constraint)
         { Pmty_with($1, $3) }
+    | module_type WITH mkrhs(mod_longident)
+        { Mty.strengthen $1 $3 }
 /*  | LPAREN MODULE mkrhs(mod_longident) RPAREN
         { Pmty_alias $3 } */
     | extension

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/388, {<.39>
-                      "t"[type] -> X/388<.39> . "t"[type];
+     Abs<.40>(X/386, {<.39>
+                      "t"[type] -> X/386<.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/391, {
-                      "t"[type] -> X/391<.41> . "t"[type];
+     Abs<.42>(X/389, {
+                      "t"[type] -> X/389<.41> . "t"[type];
                       });
  }
 module Big_to_small2 : B2S

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

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,29 @@ 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
+|}]

testsuite/tests/typing-modules/strengthening.ml

@@ -0,0 +1,55 @@
+(* TEST
+   * expect
+*)
+
+module type S1 = sig
+  module type T
+  module M : T
+  module N : T with M
+end
+[%%expect{|
+module type S1 = sig module type T module M : T module N : (T with M) end
+|}]
+
+module type S2 = sig
+  module type T
+  module M : sig end
+  module N : T with M
+end
+[%%expect{|
+Line 1:
+Error: Modules do not match: T is not included in sig end
+|}]
+
+module type S3 = sig
+  module type T = sig type t end
+  module M : T
+  module N : T with M
+end
+[%%expect{|
+module type S3 =
+  sig
+    module type T = sig type t end
+    module M : T
+    module N : sig type t = M.t end
+  end
+|}]
+
+module type S4 = sig
+  module type T = sig type t end
+  module M : T
+  module N : T with M with type t = int
+end
+[%%expect{|
+Line 4, characters 13-39:
+4 |   module N : T with M with type t = int
+                 ^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this `with' constraint, the new definition of t
+       does not match its original definition in the constrained signature:
+       Type declarations do not match:
+         type t = int
+       is not included in
+         type t = M.t
+       The type int is not equal to the type M.t
+|}]
+

testsuite/tests/warnings/w32.compilers.reference

@@ -81,3 +81,7 @@ File "w32.ml", line 65, characters 18-29:
 65 | module G (X : sig val x : int end) = X
                        ^^^^^^^^^^^
 Warning 32 [unused-value-declaration]: unused value x.
+File "w32.ml", line 76, characters 29-40:
+76 |   module type S = sig type t val x : int end
+                                  ^^^^^^^^^^^
+Warning 32 [unused-value-declaration]: unused value x.

testsuite/tests/warnings/w32.ml

@@ -69,3 +69,15 @@ module H (X : sig val x : int end) = X
 module type S = sig
   module F:  sig val x : int end -> sig end
 end
+
+(* Nominal type comparison *)
+
+module Nominal = struct
+  module type S = sig type t val x : int end
+
+  module F(X:S) = struct type t = X.t end
+  module M : S = struct type t = int let x = 1 end
+
+  module N = F(M)
+end
+

testsuite/tests/warnings/w32.mli

@@ -18,3 +18,6 @@ module H (X : sig val x : int end) : sig val x : int end
 module type S = sig
   module F:  sig val x : int end -> sig end
 end
+
+module Nominal : sig module N : sig type t end end
+

testsuite/tests/warnings/w60.compilers.reference

@@ -2,3 +2,7 @@ File "w60.ml", line 40, characters 13-14:
 40 |   let module M = struct end in
                   ^
 Warning 60 [unused-module]: unused module M.
+File "w60.ml", line 48, characters 4-22:
+48 |     module M : sig end
+         ^^^^^^^^^^^^^^^^^^
+Warning 60 [unused-module]: unused module M.

testsuite/tests/warnings/w60.ml

@@ -39,3 +39,22 @@ let () =
   (* M is unused, but no warning was emitted before 4.10. *)
   let module M = struct end in
   ()
+
+
+(* Nominal type comparisons *)
+
+module Nominal = struct
+  module type S = sig
+    module M : sig end
+    type t
+  end
+
+  module M : S = struct
+    module M = struct end
+    type t = int
+  end
+
+  module F(X:S) = struct type t = X.t end
+
+  module N = F(M)
+end

testsuite/tests/warnings/w60.mli

@@ -10,3 +10,6 @@ end
 
 module M : sig end
 module O : sig end
+
+module Nominal : sig module N : sig type t end end
+

toplevel/topdirs.ml

@@ -569,7 +569,7 @@ let () =
                (if secretly_the_same_path env path new_path
                 then acc
                 else def Trec_not :: acc)
-         | Mty_ident _ | Mty_signature _ | Mty_functor _ ->
+         | Mty_ident _ | Mty_signature _ | Mty_functor _ | Mty_strengthen _ ->
              List.rev (def (is_rec_module id md) :: acc)
        in
        accum_aliases path md []
@@ -593,7 +593,7 @@ let () =
                (if secretly_the_same_path env path new_path
                 then acc
                 else def :: acc)
-         | None | Some (Mty_alias _ | Mty_signature _ | Mty_functor _) ->
+         | None | Some (Mty_alias _ | Mty_signature _ | Mty_functor _ | Mty_strengthen _) ->
              List.rev (def :: acc)
        in
        accum_defs path mtd []

typing/btype.ml

@@ -382,6 +382,9 @@ let type_iterators =
     | Mty_functor (p, mt) ->
         it.it_functor_param it p;
         it.it_module_type it mt
+    | Mty_strengthen (mty,p,_) ->
+        it.it_module_type it mty;
+        it.it_path p
   and it_class_type it = function
       Cty_constr (p, tyl, cty) ->
         it.it_path p;

typing/ctype.ml

@@ -739,7 +739,7 @@ let rec normalize_package_path env p =
   in
   match t with
   | Some (Mty_ident p) -> normalize_package_path env p
-  | Some (Mty_signature _ | Mty_functor _ | Mty_alias _) | None ->
+  | Some (Mty_signature _ | Mty_functor _ | Mty_alias _ | Mty_strengthen _ ) | None ->
       match p with
         Path.Pdot (p1, s) ->
           (* For module aliases *)

typing/env.ml

@@ -1921,8 +1921,8 @@ let rec components_of_module_maker
           fcomp_shape = cm_shape;
           fcomp_cache = Hashtbl.create 17;
           fcomp_subst_cache = Hashtbl.create 17 })
-  | MtyL_ident _ -> Error No_components_abstract
   | MtyL_alias p -> Error (No_components_alias p)
+  | MtyL_ident _ | MtyL_strengthen _ -> Error No_components_abstract
 
 (* Insertion of bindings by identifier + path *)
 
@@ -2574,7 +2574,7 @@ let read_signature modname filename =
   let md = Subst.Lazy.force_module_decl mda.mda_declaration in
   match md.md_type with
   | Mty_signature sg -> sg
-  | Mty_ident _ | Mty_functor _ | Mty_alias _ -> assert false
+  | Mty_ident _ | Mty_functor _ | Mty_alias _ | Mty_strengthen _ -> assert false
 
 let is_identchar_latin1 = function
   | 'A'..'Z' | 'a'..'z' | '_' | '\192'..'\214' | '\216'..'\246'