GADT-based representation of module / module types.

checker/mod_checking.ml

@@ -196,11 +196,11 @@ let lookup_module mp env =
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
-    mod_expr = ();
+    mod_expr = ModTypeNul;
     mod_type = sign;
     mod_type_alg = None;
     mod_delta = delta;
-    mod_retroknowledge = ModTypeRK; }
+    mod_retroknowledge = ModTypeNul; }
 
 let rec collect_constants_without_body sign mp accu =
   let collect_field s lab = function
@@ -243,7 +243,7 @@ let rec check_module env opac mp mb opacify =
   let opac =
     check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta opacify
   in
-  let optsign, opac = match mb.mod_expr with
+  let optsign, opac = match Declareops.mod_expr mb with
     | Struct sign_struct ->
       let opacify = collect_constants_without_body mb.mod_type mb.mod_mp opacify in
       (* TODO: a bit wasteful, we recheck the types of parameters twice *)

checker/values.ml

@@ -481,7 +481,7 @@ let v_retro_action =
   |]
 
 let v_retroknowledge =
-  v_sum "module_retroknowledge" 1 [|[|v_list v_retro_action|]|]
+  v_sum "module_retroknowledge" 0 [|[|v_list v_retro_action|]|]
 
 let v_puniv = v_opt v_int
 
@@ -572,7 +572,7 @@ let [_v_sfb;_v_struc;_v_sign;_v_mexpr;_v_impl;v_module;_v_modtype] : _ Vector.t
            [|v_struc|]|])  (* Struct *)
   and v_module =
     v_tuple_c ("module_body",
-           [|v_mp;v_impl;v_sign;v_opt v_mexpr;v_resolver;v_retroknowledge|])
+           [|v_mp;v_sum_c ("when_mod_body", 0, [|[|v_impl|]|]);v_sign;v_opt v_mexpr;v_resolver;v_retroknowledge|])
   and v_modtype =
     v_tuple_c ("module_type_body",
            [|v_mp;v_noimpl;v_sign;v_opt v_mexpr;v_resolver;v_unit|])

dev/ci/user-overlays/19943-ppedrot-module-expr-type-gadt.sh

@@ -0,0 +1,3 @@
+overlay coq_lsp https://github.com/ppedrot/coq-lsp module-expr-type-gadt 19943
+
+overlay paramcoq https://github.com/ppedrot/paramcoq module-expr-type-gadt 19943

kernel/declarations.mli

@@ -342,6 +342,13 @@ type rewrite_rules_body = {
 
 (** {6 Module declarations } *)
 
+type mod_body = [ `ModBody ]
+type mod_type = [ `ModType ]
+
+type (_, 'v) when_mod_body =
+| ModBodyVal : 'v -> (mod_body, 'v) when_mod_body
+| ModTypeNul : (mod_type, 'v) when_mod_body
+
 (** Functor expressions are forced to be on top of other expressions *)
 
 type ('ty,'a) functorize =
@@ -400,12 +407,12 @@ and module_implementation =
 
 and 'a generic_module_body =
   { mod_mp : ModPath.t; (** absolute path of the module *)
-    mod_expr : 'a; (** implementation *)
+    mod_expr : ('a, module_implementation) when_mod_body; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
     mod_delta : Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *)
-    mod_retroknowledge : 'a module_retroknowledge }
+    mod_retroknowledge : ('a, Retroknowledge.action list) when_mod_body }
 
 (** For a module, there are five possible situations:
     - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
@@ -415,19 +422,16 @@ and 'a generic_module_body =
     - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
     And of course, all these situations may be functors or not. *)
 
-and module_body = module_implementation generic_module_body
+and module_body = mod_body generic_module_body
 
 (** A [module_type_body] is just a [module_body] with no implementation and
     also an empty [mod_retroknowledge]. Its [mod_type_alg] contains
     the algebraic definition of this module type, or [None]
     if it has been built interactively. *)
 
-and module_type_body = unit generic_module_body
+and module_type_body = mod_type generic_module_body
 
-and _ module_retroknowledge =
-| ModBodyRK :
-  Retroknowledge.action list -> module_implementation module_retroknowledge
-| ModTypeRK : unit module_retroknowledge
+type 'a module_retroknowledge = ('a, Retroknowledge.action list) when_mod_body
 
 (** Extra invariants :
 

kernel/declareops.ml

@@ -362,8 +362,16 @@ let subst_rewrite_rules subst ({ rewrules_rules } as rules) =
   if rewrules_rules == body' then rules else
     { rewrules_rules = body' }
 
+let mod_expr { mod_expr = ModBodyVal v; _ } = v
+
 (** Hashconsing of modules *)
 
+let hcons_when_mod_body (type a b) (f : b -> b) : (a, b) when_mod_body -> (a, b) when_mod_body = function
+| ModBodyVal v as arg ->
+  let v' = f v in
+  if v == v' then arg else ModBodyVal v'
+| ModTypeNul -> ModTypeNul
+
 let hcons_functorize hty he hself f = match f with
 | NoFunctor e ->
   let e' = he e in
@@ -394,10 +402,10 @@ let rec hcons_structure_field_body sb = match sb with
   let mib' = hcons_mind mib in
   if mib == mib' then sb else SFBmind mib'
 | SFBmodule mb ->
-  let mb' = hcons_module_body mb in
+  let mb' = hcons_generic_module_body mb in
   if mb == mb' then sb else SFBmodule mb'
 | SFBmodtype mb ->
-  let mb' = hcons_module_type mb in
+  let mb' = hcons_generic_module_body mb in
   if mb == mb' then sb else SFBmodtype mb'
 | SFBrules _ -> sb (* TODO? *)
 
@@ -411,7 +419,7 @@ and hcons_structure_body sb =
   List.Smart.map map sb
 
 and hcons_module_signature ms =
-  hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms
+  hcons_functorize hcons_generic_module_body hcons_structure_body hcons_module_signature ms
 
 and hcons_module_implementation mip = match mip with
 | Abstract -> Abstract
@@ -424,10 +432,10 @@ and hcons_module_implementation mip = match mip with
 | FullStruct -> FullStruct
 
 and hcons_generic_module_body :
-  'a. ('a -> 'a) -> 'a generic_module_body -> 'a generic_module_body =
-  fun hcons_impl mb ->
+  'a. 'a generic_module_body -> 'a generic_module_body =
+  fun mb ->
   let mp' = mb.mod_mp in
-  let expr' = hcons_impl mb.mod_expr in
+  let expr' = hcons_when_mod_body hcons_module_implementation mb.mod_expr in
   let type' = hcons_module_signature mb.mod_type in
   let type_alg' = mb.mod_type_alg in
   let delta' = mb.mod_delta in
@@ -450,8 +458,8 @@ and hcons_generic_module_body :
     mod_retroknowledge = retroknowledge';
   }
 
-and hcons_module_body mb =
-  hcons_generic_module_body hcons_module_implementation mb
+let hcons_module_body =
+  hcons_generic_module_body
 
-and hcons_module_type mb =
-  hcons_generic_module_body (fun () -> ()) mb
+let hcons_module_type =
+  hcons_generic_module_body

kernel/declareops.mli

@@ -77,6 +77,10 @@ val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj
 val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
   (Names.Projection.Repr.t * Sorts.relevance) array option
 
+(** {6 Modules} *)
+
+val mod_expr : module_body -> module_implementation
+
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
@@ -91,5 +95,6 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
 val hcons_const_body : ?hbody:(Constr.t -> Constr.t) ->
   ('a, 'b) pconstant_body -> ('a, 'b) pconstant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
+val hcons_generic_module_body : 'a generic_module_body -> 'a generic_module_body
 val hcons_module_body : module_body -> module_body
 val hcons_module_type : module_type_body -> module_type_body

kernel/mod_typing.ml

@@ -139,7 +139,7 @@ let rec check_with_def (cst, ustate) env struc (idl, wth) mp reso =
         | SFBmodule mb -> mb
         | _ -> error_not_a_module_label lab
       in
-      begin match mb.mod_expr with
+      begin match Declareops.mod_expr mb with
         | Abstract ->
           let struc = Modops.destr_nofunctor (MPdot (mp,lab)) mb.mod_type in
           let struc', cst =
@@ -171,7 +171,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
       (* Toplevel module definition *)
       let new_mb = lookup_module new_mp env in
       let new_mtb = module_type_of_module new_mb in
-      let cst = match old.mod_expr with
+      let cst = match Declareops.mod_expr old with
         | Abstract ->
           let mtb_old = module_type_of_module old in
           let cst = Subtyping.check_subtypes (cst, ustate) env' new_mtb mtb_old in
@@ -186,7 +186,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
       let new_mb' =
         { new_mb with
           mod_mp = mp';
-          mod_expr = Algebraic (MENoFunctor (MEident new_mp));
+          mod_expr = ModBodyVal (Algebraic (MENoFunctor (MEident new_mp)));
         }
       in
       let new_reso = add_delta_resolver reso new_mb.mod_delta in
@@ -202,7 +202,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
         | SFBmodule msb -> msb
         | _ -> error_not_a_module_label lab
       in
-      begin match old.mod_expr with
+      begin match Declareops.mod_expr old with
       | Abstract ->
         let struc = destr_nofunctor mp' old.mod_type in
         let struc',reso',cst =
@@ -286,15 +286,19 @@ let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl = function
 
 let mk_mod mp e ty reso =
   { mod_mp = mp;
-    mod_expr = e;
+    mod_expr = ModBodyVal e;
     mod_type = ty;
     mod_type_alg = None;
     mod_delta = reso;
-    mod_retroknowledge = ModBodyRK []; }
+    mod_retroknowledge = ModBodyVal []; }
 
 let mk_modtype mp ty reso =
-  let mb = mk_mod mp Abstract ty reso in
-  { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
+  { mod_mp = mp;
+    mod_expr = ModTypeNul;
+    mod_type = ty;
+    mod_type_alg = None;
+    mod_delta = reso;
+    mod_retroknowledge = ModTypeNul; }
 
 let rec translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod mp inl mse = function
   | [] ->
@@ -339,8 +343,8 @@ let finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sign,alg,reso) resty
     in
     { res_mtb with
       mod_mp = mp;
-      mod_expr = impl;
-      mod_retroknowledge = ModBodyRK [];
+      mod_expr = ModBodyVal impl;
+      mod_retroknowledge = ModBodyVal [];
     },
     (** constraints from module body typing + subtyping + module type. *)
     cst,
@@ -372,7 +376,7 @@ let rec forbid_incl_signed_functor env = function
   | MEwith _ -> assert false (* No 'with' syntax for modules *)
   | MEident mp1 ->
     let mb = lookup_module mp1 env in
-    match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
+    match mb.mod_type, mb.mod_type_alg, Declareops.mod_expr mb with
     | MoreFunctor _, Some _, _ ->
       (* functor + restricted signature = error *)
       error_include_restricted_functor mp1