Module type substitutions

Changes

@@ -26,6 +26,11 @@ Working version
   (Takafumi Saikawa and Jacques Garrigue, review by Gabriel Scherer and
    Florian Angeletti)
 
+- #10133: module type substitutions
+  Allow 'SIG with module type T = F(X).S', 'SIG with module type T := sig end'
+  and their local equivalent `module type T := sig type u end`
+  (Florian Angeletti, review by Gabriel Radanne and Leo White)
+
 ### Runtime system:
 
 - #9284: Add -config option to display the configuration of ocamlrun on stdout,

manual/src/refman/extensions/signaturesubstitution.etex

@@ -63,6 +63,8 @@ specification:
           ...
         | 'type' type-subst { 'and' type-subst }
         | 'module' module-name ':=' extended-module-path
+        | 'module' 'type' module-name ':=' module-type
+
 ;
 
 type-subst:
@@ -97,3 +99,67 @@ module type S = sig
   type 'a poly_list := [ `Cons of 'a * 'a poly_list | `Nil ]
 end [@@expect error];;
 \end{caml_example}
+
+\subsection{ss:module-type-substitution}{Module type substitutions}
+
+(Introduced in OCaml 4.13)
+
+\begin{syntax}
+mod-constraint:
+          ...
+        | 'module ' 'type' modtype-path  '=' module-type
+        | 'module ' 'type' modtype-path  ':=' module-type
+\end{syntax}
+
+Module type substitution essentially behaves like type substitutions.
+They are useful to refine an abstract module type in a signature into
+a concrete module type,
+
+\begin{caml_example}{toplevel}
+module type ENDO = sig
+  module type T
+  module F: T -> T
+end
+module Endo(X: sig module type T end): ENDO with module type T = X.T =
+struct
+    module type T = X.T
+    module F(X:T) = X
+ end;;
+\end{caml_example}
+
+It is also possible to substitute a concrete module type with an
+equivalent module types.
+
+\begin{caml_example*}{verbatim}
+module type A = sig
+  type x
+  module type R = sig
+    type a = A of x
+    type b
+  end
+end
+module type S = sig
+  type a = A of int
+  type b
+end
+module type B = A with type x = int and module type R = S
+\end{caml_example*}
+However, such substitutions are never necessary.
+
+Destructive module type substitution removes the module type substitution
+from the signature
+\begin{caml_example}{toplevel}
+module type ENDO' = ENDO with module type T := ENDO;;
+\end{caml_example}
+If the right hand side of the substitution is not a path, then the destructive
+substitution is only valid if the left-hand side of the substitution is never
+used as the type of a first-class module in the original module type.
+
+\begin{caml_example}{verbatim}[error]
+module type T = sig module type S val x: (module S) end
+module type Error = T with module type S := sig end
+\end{caml_example}
+
+\section{s:module-alias}{Type-level module aliases}
+\ikwd{module\@\texttt{module}}
+%HEVEA\cutname{modulealias.html}

manual/src/refman/modtypes.etex

@@ -55,8 +55,9 @@ See also the following language extensions:
 \hyperref[s:signature-substitution]{substitution inside a signature},
 \hyperref[s:module-alias]{type-level module aliases},
 \hyperref[s:attributes]{attributes},
-\hyperref[s:extension-nodes]{extension nodes} and
-\hyperref[s:generative-functors]{generative functors}.
+\hyperref[s:extension-nodes]{extension nodes},
+\hyperref[s:generative-functors]{generative functors},
+and \hyperref[ss:module-type-substitution]{module type substitutions}.
 
 \subsection{ss:mty-simple}{Simple module types}
 

ocamldoc/odoc_sig.ml

@@ -451,11 +451,14 @@ module Analyser =
     let erased_names_of_constraints constraints acc =
       List.fold_right (fun constraint_ acc ->
         match constraint_ with
-        | Parsetree.Pwith_type _ | Parsetree.Pwith_module _ -> acc
+        | Parsetree.Pwith_type _ | Parsetree.Pwith_module _ | Parsetree.Pwith_modtype _ -> acc
         | Parsetree.Pwith_typesubst (s, typedecl) ->
            constraint_for_subitem acc s (fun s -> Parsetree.Pwith_typesubst (s, typedecl))
         | Parsetree.Pwith_modsubst (s, modpath) ->
-           constraint_for_subitem acc s (fun s -> Parsetree.Pwith_modsubst (s, modpath)))
+           constraint_for_subitem acc s (fun s -> Parsetree.Pwith_modsubst (s, modpath))
+        | Parsetree.Pwith_modtypesubst (s, modpath) ->
+            constraint_for_subitem acc s
+              (fun s -> Parsetree.Pwith_modtypesubst (s, modpath)))
         constraints acc
 
     let is_erased ident map =
@@ -510,6 +513,7 @@ module Analyser =
            end
         | Parsetree.Psig_modtype {Parsetree.pmtd_name=name} as m ->
           if is_erased name.txt erased then acc else take_item m
+        | Parsetree.Psig_modtypesubst _  -> acc
         | Parsetree.Psig_recmodule mods ->
           (match List.filter
                    (fun pmd ->
@@ -1288,7 +1292,8 @@ module Analyser =
             let (maybe_more, mods) = f ~first: true 0 pos_start_ele decls in
             (maybe_more, new_env, mods)
 
-        | Parsetree.Psig_modtype {Parsetree.pmtd_name=name; pmtd_type=pmodtype_decl} ->
+        | Parsetree.Psig_modtype {Parsetree.pmtd_name=name; pmtd_type=pmodtype_decl}
+        | Parsetree.Psig_modtypesubst {Parsetree.pmtd_name=name; pmtd_type=pmodtype_decl} ->
             let complete_name = Name.concat current_module_name name.txt in
             let sig_mtype =
               try Signature_search.search_module_type table name.txt

parsing/ast_helper.ml

@@ -271,6 +271,7 @@ module Sig = struct
   let mod_subst ?loc a = mk ?loc (Psig_modsubst a)
   let rec_module ?loc a = mk ?loc (Psig_recmodule a)
   let modtype ?loc a = mk ?loc (Psig_modtype a)
+  let modtype_subst ?loc a = mk ?loc (Psig_modtypesubst a)
   let open_ ?loc a = mk ?loc (Psig_open a)
   let include_ ?loc a = mk ?loc (Psig_include a)
   let class_ ?loc a = mk ?loc (Psig_class a)

parsing/ast_helper.mli

@@ -288,6 +288,7 @@ module Sig:
     val mod_subst: ?loc:loc -> module_substitution -> signature_item
     val rec_module: ?loc:loc -> module_declaration list -> signature_item
     val modtype: ?loc:loc -> module_type_declaration -> signature_item
+    val modtype_subst: ?loc:loc -> module_type_declaration -> signature_item
     val open_: ?loc:loc -> open_description -> signature_item
     val include_: ?loc:loc -> include_description -> signature_item
     val class_: ?loc:loc -> class_description list -> signature_item

parsing/ast_invariants.ml

@@ -24,6 +24,8 @@ let no_args loc = err loc "Function application with no argument."
 let empty_let loc = err loc "Let with no bindings."
 let empty_type loc = err loc "Type declarations cannot be empty."
 let complex_id loc = err loc "Functor application not allowed here."
+let module_type_substitution_missing_rhs loc =
+  err loc "Module type substitution with no right hand side"
 
 let simple_longident id =
   let rec is_simple = function
@@ -140,6 +142,8 @@ let iterator =
     let loc = sg.psig_loc in
     match sg.psig_desc with
     | Psig_type (_, []) -> empty_type loc
+    | Psig_modtypesubst {pmtd_type=None; _ } ->
+        module_type_substitution_missing_rhs loc
     | _ -> ()
   in
   let row_field self field =

parsing/ast_iterator.ml

@@ -263,10 +263,14 @@ module MT = struct
         iter_loc sub lid; sub.type_declaration sub d
     | Pwith_module (lid, lid2) ->
         iter_loc sub lid; iter_loc sub lid2
+    | Pwith_modtype (lid, mty) ->
+        iter_loc sub lid; sub.module_type sub mty
     | Pwith_typesubst (lid, d) ->
         iter_loc sub lid; sub.type_declaration sub d
     | Pwith_modsubst (s, lid) ->
         iter_loc sub s; iter_loc sub lid
+    | Pwith_modtypesubst (lid, mty) ->
+        iter_loc sub lid; sub.module_type sub mty
 
   let iter_signature_item sub {psig_desc = desc; psig_loc = loc} =
     sub.location sub loc;
@@ -281,7 +285,7 @@ module MT = struct
     | Psig_modsubst x -> sub.module_substitution sub x
     | Psig_recmodule l ->
         List.iter (sub.module_declaration sub) l
-    | Psig_modtype x -> sub.module_type_declaration sub x
+    | Psig_modtype x | Psig_modtypesubst x -> sub.module_type_declaration sub x
     | Psig_open x -> sub.open_description sub x
     | Psig_include x -> sub.include_description sub x
     | Psig_class l -> List.iter (sub.class_description sub) l

parsing/ast_mapper.ml

@@ -293,10 +293,14 @@ module MT = struct
         Pwith_type (map_loc sub lid, sub.type_declaration sub d)
     | Pwith_module (lid, lid2) ->
         Pwith_module (map_loc sub lid, map_loc sub lid2)
+    | Pwith_modtype (lid, mty) ->
+        Pwith_modtype (map_loc sub lid, sub.module_type sub mty)
     | Pwith_typesubst (lid, d) ->
         Pwith_typesubst (map_loc sub lid, sub.type_declaration sub d)
     | Pwith_modsubst (s, lid) ->
         Pwith_modsubst (map_loc sub s, map_loc sub lid)
+    | Pwith_modtypesubst (lid, mty) ->
+        Pwith_modtypesubst (map_loc sub lid, sub.module_type sub mty)
 
   let map_signature_item sub {psig_desc = desc; psig_loc = loc} =
     let open Sig in
@@ -314,6 +318,8 @@ module MT = struct
     | Psig_recmodule l ->
         rec_module ~loc (List.map (sub.module_declaration sub) l)
     | Psig_modtype x -> modtype ~loc (sub.module_type_declaration sub x)
+    | Psig_modtypesubst x ->
+        modtype_subst ~loc (sub.module_type_declaration sub x)
     | Psig_open x -> open_ ~loc (sub.open_description sub x)
     | Psig_include x -> include_ ~loc (sub.include_description sub x)
     | Psig_class l -> class_ ~loc (List.map (sub.class_description sub) l)

parsing/depend.ml

@@ -311,8 +311,10 @@ and add_modtype bv mty =
         (function
           | Pwith_type (_, td) -> add_type_declaration bv td
           | Pwith_module (_, lid) -> add_module_path bv lid
+          | Pwith_modtype (_, mty) -> add_modtype bv mty
           | Pwith_typesubst (_, td) -> add_type_declaration bv td
           | Pwith_modsubst (_, lid) -> add_module_path bv lid
+          | Pwith_modtypesubst (_, mty) -> add_modtype bv mty
         )
         cstrl
   | Pmty_typeof m -> add_module_expr bv m
@@ -380,7 +382,7 @@ and add_sig_item (bv, m) item =
       let bv' = add bv and m' = add m in
       List.iter (fun pmd -> add_modtype bv' pmd.pmd_type) decls;
       (bv', m')
-  | Psig_modtype x ->
+  | Psig_modtype x | Psig_modtypesubst x->
       begin match x.pmtd_type with
         None -> ()
       | Some mty -> add_modtype bv mty

parsing/parser.mly

@@ -1662,6 +1662,8 @@ signature_item:
         { let (ext, l) = $1 in (Psig_recmodule l, ext) }
     | module_type_declaration
         { let (body, ext) = $1 in (Psig_modtype body, ext) }
+    | module_type_subst
+        { let (body, ext) = $1 in (Psig_modtypesubst body, ext) }
     | open_description
         { let (body, ext) = $1 in (Psig_open body, ext) }
     | include_statement(module_type)
@@ -1774,6 +1776,23 @@ module_subst:
   }
 ;
 
+(* A module type substitution *)
+module_type_subst:
+  MODULE TYPE
+  ext = ext
+  attrs1 = attributes
+  id = mkrhs(ident)
+  COLONEQUAL
+  typ=module_type
+  attrs2 = post_item_attributes
+  {
+    let attrs = attrs1 @ attrs2 in
+    let loc = make_loc $sloc in
+    let docs = symbol_docs $sloc in
+    Mtd.mk id ~typ ~attrs ~loc ~docs, ext
+  }
+
+
 (* -------------------------------------------------------------------------- *)
 
 (* Class declarations. *)
@@ -3212,6 +3231,10 @@ with_constraint:
       { Pwith_module ($2, $4) }
   | MODULE mkrhs(mod_longident) COLONEQUAL mkrhs(mod_ext_longident)
       { Pwith_modsubst ($2, $4) }
+  | MODULE TYPE l=mkrhs(mty_longident) EQUAL rhs=module_type
+      { Pwith_modtype (l, rhs) }
+  | MODULE TYPE l=mkrhs(mty_longident) COLONEQUAL rhs=module_type
+      { Pwith_modtypesubst (l, rhs) }
 ;
 with_type_binder:
     EQUAL          { Public }

parsing/parsetree.mli

@@ -769,6 +769,8 @@ and signature_item_desc =
   | Psig_modtype of module_type_declaration
         (* module type S = MT
            module type S *)
+  | Psig_modtypesubst of module_type_declaration
+        (* module type S :=  ...  *)
   | Psig_open of open_description
         (* open X *)
   | Psig_include of include_description
@@ -852,6 +854,10 @@ and with_constraint =
            the name of the type_declaration. *)
   | Pwith_module of Longident.t loc * Longident.t loc
         (* with module X.Y = Z *)
+  | Pwith_modtype of Longident.t loc * module_type
+        (* with module type X.Y = Z *)
+  | Pwith_modtypesubst of Longident.t loc * module_type
+        (* with module type X.Y := sig end *)
   | Pwith_typesubst of Longident.t loc * type_declaration
         (* with type X.t := ..., same format as [Pwith_type] *)
   | Pwith_modsubst of Longident.t loc * Longident.t loc

parsing/pprintast.ml

@@ -1059,26 +1059,33 @@ and module_type ctxt f x =
         end
     | Pmty_with (mt, []) -> module_type ctxt f mt
     | Pmty_with (mt, l) ->
-        let with_constraint f = function
-          | Pwith_type (li, ({ptype_params= ls ;_} as td)) ->
-              let ls = List.map fst ls in
-              pp f "type@ %a %a =@ %a"
-                (list (core_type ctxt) ~sep:"," ~first:"(" ~last:")")
-                ls longident_loc li (type_declaration ctxt) td
-          | Pwith_module (li, li2) ->
-              pp f "module %a =@ %a" longident_loc li longident_loc li2;
-          | Pwith_typesubst (li, ({ptype_params=ls;_} as td)) ->
-              let ls = List.map fst ls in
-              pp f "type@ %a %a :=@ %a"
-                (list (core_type ctxt) ~sep:"," ~first:"(" ~last:")")
-                ls longident_loc li
-                (type_declaration ctxt) td
-          | Pwith_modsubst (li, li2) ->
-             pp f "module %a :=@ %a" longident_loc li longident_loc li2 in
         pp f "@[<hov2>%a@ with@ %a@]"
-          (module_type1 ctxt) mt (list with_constraint ~sep:"@ and@ ") l
+          (module_type1 ctxt) mt
+          (list (with_constraint ctxt) ~sep:"@ and@ ") l
     | _ -> module_type1 ctxt f x
 
+and with_constraint ctxt f = function
+  | Pwith_type (li, ({ptype_params= ls ;_} as td)) ->
+      let ls = List.map fst ls in
+      pp f "type@ %a %a =@ %a"
+        (list (core_type ctxt) ~sep:"," ~first:"(" ~last:")")
+        ls longident_loc li (type_declaration ctxt) td
+  | Pwith_module (li, li2) ->
+      pp f "module %a =@ %a" longident_loc li longident_loc li2;
+  | Pwith_modtype (li, mty) ->
+      pp f "module type %a =@ %a" longident_loc li (module_type ctxt) mty;
+  | Pwith_typesubst (li, ({ptype_params=ls;_} as td)) ->
+      let ls = List.map fst ls in
+      pp f "type@ %a %a :=@ %a"
+        (list (core_type ctxt) ~sep:"," ~first:"(" ~last:")")
+        ls longident_loc li
+        (type_declaration ctxt) td
+  | Pwith_modsubst (li, li2) ->
+      pp f "module %a :=@ %a" longident_loc li longident_loc li2
+  | Pwith_modtypesubst (li, mty) ->
+      pp f "module type %a :=@ %a" longident_loc li (module_type ctxt) mty;
+
+
 and module_type1 ctxt f x =
   if x.pmty_attributes <> [] then module_type ctxt f x
   else match x.pmty_desc with
@@ -1162,6 +1169,13 @@ and signature_item ctxt f x : unit =
                pp f "@ =@ %a" (module_type ctxt) mt
         ) md
         (item_attributes ctxt) attrs
+  | Psig_modtypesubst {pmtd_name=s; pmtd_type=md; pmtd_attributes=attrs} ->
+      let md = match md with
+        | None -> assert false (* ast invariant *)
+        | Some mt -> mt in
+      pp f "@[<hov2>module@ type@ %s@ :=@ %a@]%a"
+        s.txt (module_type ctxt) md
+        (item_attributes ctxt) attrs
   | Psig_class_type (l) -> class_type_declaration_list ctxt f l
   | Psig_recmodule decls ->
       let rec  string_x_module_type_list f ?(first=true) l =

parsing/printast.ml

@@ -730,6 +730,10 @@ and signature_item i ppf x =
       line i ppf "Psig_modtype %a\n" fmt_string_loc x.pmtd_name;
       attributes i ppf x.pmtd_attributes;
       modtype_declaration i ppf x.pmtd_type
+  | Psig_modtypesubst x ->
+      line i ppf "Psig_modtypesubst %a\n" fmt_string_loc x.pmtd_name;
+      attributes i ppf x.pmtd_attributes;
+      modtype_declaration i ppf x.pmtd_type
   | Psig_open od ->
       line i ppf "Psig_open %a %a\n" fmt_override_flag od.popen_override
         fmt_longident_loc od.popen_expr;
@@ -771,6 +775,14 @@ and with_constraint i ppf x =
       line i ppf "Pwith_modsubst %a = %a\n"
         fmt_longident_loc lid1
         fmt_longident_loc lid2;
+  | Pwith_modtype (lid1, mty) ->
+      line i ppf "Pwith_modtype %a\n"
+        fmt_longident_loc lid1;
+      module_type (i+1) ppf mty
+  | Pwith_modtypesubst (lid1, mty) ->
+     line i ppf "Pwith_modtypesubst %a\n"
+        fmt_longident_loc lid1;
+      module_type (i+1) ppf mty
 
 and module_expr i ppf x =
   line i ppf "module_expr %a\n" fmt_location x.pmod_loc;