flambda-backend: Lazy strengthening (#1337)

This PR adds strengthening as a first-class concept to the module type language. The main motivation is faster module type checking but this also makes the language more expressive, allowing more programs to type.
# New syntax
Suppose we have
```ocaml
module type S = sig type t end
module M : S
```
The actual type of `M` is stronger than `S` - it is `sig type t = M.t end`. The new extension allows this type to be written as `S with M` (in the literature, `S/M` is often used). This effectively strengthens all types in `S` with the information that they are equal to those in `M`.
# Expressivity
Previously, strengthening happened by actually adding information to all types in a module type. This meant that abstract module types couldn’t be strengthened. Consider
```ocaml
module F (Y : sig module type A module X : A end) = Y.X
```
We now infer the `functor (Y : …) -> (Y.A with Y.X)` for `F` where previously, we only could infer `functor (Y : …) -> Y.A`, thus losing information. See ocaml/ocaml#12204 for more details.
# Efficiency
The main benefit of the extension, though, is that it allows us to type check some programs much quicker. Consider the following example.
```ocaml
module type S = sig
  type t
  val x : t 
  <lots of value declarations>
end
module M : S = …
module F (X : S) = …
module N = F(M)
```
To type `N`, we have to check that the type of `M` is a subtype of `S`. With the new extension, this is simple: `M` gets the type `S with M` and `S with M < S` always holds so the check finishes very quickly. Previously, we would infer the (large) type
```ocaml
sig
  type t = M.t
  val x : t
   …
end
```
for `M` by unfolding `S` and strengthening it. When checking `F(M)`, we would then match this type against `S` which requires unfolding `S` again and then comparing the individual signature items.
# Unused warnings
Suppose that `x` in the above example isn’t actually used anywhere. With this PR, we will indeed issue an unused declaration warning. This wasn’t the case previously as `x` was (implicitly) used while typing `F(M)` since were unfolding `S`.

---------

Co-authored-by: Roman Leshchinskiy <rleshchinskiy@janestreet.com>

.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 \

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 ->

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/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

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. *)

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

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