Merge PR #931: Parametrize module body

15 files changed, 123 insertions, 70 deletions

diff --git a/API/API.mli b/API/API.mli
index fce319fe37..8b0bef48c9 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1280,23 +1280,28 @@ sig
                                | Algebraic of module_expression
                              | Struct of module_signature
                              | FullStruct
-   and module_body =
+   and 'a generic_module_body =
                        { mod_mp : Names.ModPath.t;
-                         mod_expr : module_implementation;
+                         mod_expr : 'a;
                          mod_type : module_signature;
                          mod_type_alg : module_expression option;
                          mod_constraints : Univ.ContextSet.t;
                          mod_delta : Mod_subst.delta_resolver;
-                         mod_retroknowledge : Retroknowledge.action list
+                         mod_retroknowledge : 'a module_retroknowledge;
                        }
    and module_signature = (module_type_body,structure_body) functorize
-   and module_type_body = module_body
+   and module_body = module_implementation generic_module_body
+   and module_type_body = unit generic_module_body
    and structure_body = (Names.Label.t * structure_field_body) list
    and structure_field_body =
                             | SFBconst of constant_body
                             | SFBmind of mutual_inductive_body
                             | SFBmodule of module_body
                             | SFBmodtype of module_type_body
+  and _ module_retroknowledge =
+  | ModBodyRK :
+    Retroknowledge.action list -> module_implementation module_retroknowledge
+  | ModTypeRK : unit module_retroknowledge
 end
 
 module Declareops :
diff --git a/checker/cic.mli b/checker/cic.mli
index 59dd5bc4d3..753fd0fc00 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -385,9 +385,9 @@ and module_implementation =
   | Struct of module_signature (** interactive body *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and module_body =
+and 'a generic_module_body =
   { mod_mp : module_path; (** absolute path of the module *)
-    mod_expr : module_implementation; (** implementation *)
+    mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
@@ -395,13 +395,19 @@ and module_body =
     mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
-    mod_retroknowledge : action list }
+    mod_retroknowledge : 'a module_retroknowledge; }
+
+and module_body = module_implementation generic_module_body
 
 (** A [module_type_body] is just a [module_body] with no
-    implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge] *)
+    implementation and also an empty [mod_retroknowledge] *)
+
+and module_type_body = unit generic_module_body
 
-and module_type_body = module_body
+and _ module_retroknowledge =
+| ModBodyRK :
+  action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
 
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 093d999a34..884a1ef18c 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -583,24 +583,30 @@ let rec subst_expr sub = function
   | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
 
 let rec subst_expression sub me =
-  functor_map (subst_module sub) (subst_expr sub) me
+  functor_map (subst_module_type sub) (subst_expr sub) me
 
 and subst_signature sub sign =
-  functor_map (subst_module sub) (subst_structure sub) sign
+  functor_map (subst_module_type sub) (subst_structure sub) sign
 
 and subst_structure sub struc =
   let subst_body = function
     | SFBconst cb -> SFBconst (subst_const_body sub cb)
     | SFBmind mib -> SFBmind (subst_mind sub mib)
     | SFBmodule mb -> SFBmodule (subst_module sub mb)
-    | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb)
+    | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb)
   in
   List.map (fun (l,b) -> (l,subst_body b)) struc
 
-and subst_module sub mb =
+and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun subst_impl sub mb ->
   { mb with
     mod_mp = subst_mp sub mb.mod_mp;
-    mod_expr =
-      implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
+    mod_expr = subst_impl sub mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
     mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+
+and subst_module sub mb =
+  subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
+
+and subst_module_type sub mb =
+  subst_body (fun _ () -> ()) sub mb
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b6816dd484..3c9e1cac54 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -70,12 +70,12 @@ let lookup_module mp env =
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
-    mod_retroknowledge = []; }
+    mod_retroknowledge = ModTypeRK; }
 
 let rec check_module env mp mb =
   let (_:module_signature) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 79cd5c29fd..f0abc39eac 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,7 +49,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -93,17 +93,19 @@ let strengthen_const mp_from l cb resolver =
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
-  else strengthen_body true mp_from mp_to mb
+  else
+    let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in
+    strengthen_body mk_expr mp_from mp_to mb
 
-and strengthen_body is_mod mp_from mp_to mb =
+and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun mk_expr mp_from mp_to mb ->
   match mb.mod_type with
   | MoreFunctor _ -> mb
   | NoFunctor sign ->
     let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
     in
     { mb with
-      mod_expr =
-        (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+      mod_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
@@ -130,7 +132,7 @@ and strengthen_sig mp_from sign mp_to resolver =
 	resolve_out,item::rest'
 
 let strengthen mtb mp =
-  strengthen_body false mtb.mod_mp mp mtb
+  strengthen_body ignore mtb.mod_mp mp mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
@@ -138,9 +140,9 @@ let subst_and_strengthen mb mp =
 let module_type_of_module mp mb =
   let mtb =
     { mb with
-      mod_expr = Abstract;
+      mod_expr = ();
       mod_type_alg = None;
-      mod_retroknowledge = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 68a467bea2..98a9c8250d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
 			  mod_type = body_t1;
 			  mod_type_alg = None;
 			  mod_constraints = mtb1.mod_constraints;
-			  mod_retroknowledge = [];
+			  mod_retroknowledge = ModBodyRK [];
 			  mod_delta = mtb1.mod_delta} env
 	  in
 	  check_structure env body_t1 body_t2 equiv
diff --git a/checker/values.ml b/checker/values.ml
index c95c3f1b2b..afde84854c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 c802f941f368bedd96e931cda0559d67  checker/cic.mli
+MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
 
 *)
 
@@ -54,6 +54,7 @@ let v_enum name n = Sum(name,n,[||])
 
 let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
 let v_bool = v_enum "bool" 2
+let v_unit = v_enum "unit" 1
 let v_ref v = v_tuple "ref" [|v|]
 
 let v_set v =
@@ -311,13 +312,13 @@ and v_impl =
   Sum ("module_impl",2, (* Abstract, FullStruct *)
   [|[|v_mexpr|];  (* Algebraic *)
     [|v_sign|]|])  (* Struct *)
-and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
+and v_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
          [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
 
 (** kernel/safe_typing *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9697b0b8b2..e17fb1c38f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -250,16 +250,16 @@ and module_implementation =
   | Struct of module_signature (** interactive body *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and module_body =
+and 'a generic_module_body =
   { mod_mp : module_path; (** absolute path of the module *)
-    mod_expr : module_implementation; (** implementation *)
+    mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
     mod_constraints : Univ.ContextSet.t; (**
       set of all universes constraints in the module  *)
     mod_delta : Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *)
-    mod_retroknowledge : Retroknowledge.action list }
+    mod_retroknowledge : 'a module_retroknowledge }
 
 (** For a module, there are five possible situations:
     - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
@@ -269,13 +269,19 @@ and 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. *)
 
-(** A [module_type_body] is just a [module_body] with no
-    implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+and module_body = module_implementation 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 = module_body
+and module_type_body = unit generic_module_body
+
+and _ module_retroknowledge =
+| ModBodyRK :
+  Retroknowledge.action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
 
 (** Extra invariants :
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 85dd1e66db..66d66c7d09 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -318,7 +318,7 @@ let rec hcons_structure_field_body sb = match sb with
   let mb' = hcons_module_body mb in
   if mb == mb' then sb else SFBmodule mb'
 | SFBmodtype mb ->
-  let mb' = hcons_module_body mb in
+  let mb' = hcons_module_type mb in
   if mb == mb' then sb else SFBmodtype mb'
 
 and hcons_structure_body sb =
@@ -331,10 +331,10 @@ and hcons_structure_body sb =
   List.smartmap map sb
 
 and hcons_module_signature ms =
-  hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms
+  hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms
 
 and hcons_module_expression me =
-  hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me
+  hcons_functorize hcons_module_type hcons_module_alg_expr hcons_module_expression me
 
 and hcons_module_implementation mip = match mip with
 | Abstract -> Abstract
@@ -346,9 +346,11 @@ and hcons_module_implementation mip = match mip with
   if ms == ms' then mip else Struct ms
 | FullStruct -> FullStruct
 
-and hcons_module_body mb =
+and hcons_generic_module_body :
+  'a. ('a -> 'a) -> 'a generic_module_body -> 'a generic_module_body =
+  fun hcons_impl mb ->
   let mp' = mb.mod_mp in
-  let expr' = hcons_module_implementation mb.mod_expr in
+  let expr' = hcons_impl mb.mod_expr in
   let type' = hcons_module_signature mb.mod_type in
   let type_alg' = mb.mod_type_alg in
   let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
@@ -373,3 +375,9 @@ and hcons_module_body mb =
     mod_delta = delta';
     mod_retroknowledge = retroknowledge';
   }
+
+and hcons_module_body mb =
+  hcons_generic_module_body hcons_module_implementation mb
+
+and hcons_module_type mb =
+  hcons_generic_module_body (fun () -> ()) mb
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index a8ba5fa392..b2d29759da 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -78,3 +78,4 @@ val safe_flags : typing_flags
 val hcons_const_body : constant_body -> constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
+val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0888ccc109..d2b41aae98 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -264,7 +264,9 @@ let rec translate_mse env mpo inl = function
   |MEident mp1 as me ->
     let mb = match mpo with
       |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
-      |None -> lookup_modtype mp1 env
+      |None ->
+        let mt = lookup_modtype mp1 env in
+        module_body_of_type mt.mod_mp mt
     in
     mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
@@ -281,9 +283,11 @@ let mk_mod mp e ty cst reso =
     mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = reso;
-    mod_retroknowledge = [] }
+    mod_retroknowledge = ModBodyRK []; }
 
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
+let mk_modtype mp ty cst reso =
+  let mb = mk_mod mp Abstract ty cst reso in
+  { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
 
 let rec translate_mse_funct env mpo inl mse = function
   |[] ->
@@ -319,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
+      mod_retroknowledge = ModBodyRK [];
       (** cst from module body typing,
           cst' from subtyping,
           constraints from module type. *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index a079bc8931..76915e917a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -143,11 +143,12 @@ let rec functor_iter fty f0 = function
 (** {6 Misc operations } *)
 
 let module_type_of_module mb =
-  { mb with mod_expr = Abstract; mod_type_alg = None }
+  { mb with mod_expr = (); mod_type_alg = None;
+    mod_retroknowledge = ModTypeRK; }
 
 let module_body_of_type mp mtb =
-  assert (mtb.mod_expr == Abstract);
-  { mtb with mod_mp = mp }
+  { mtb with mod_expr = Abstract; mod_mp = mp;
+      mod_retroknowledge = ModBodyRK []; }
 
 let check_modpath_equiv env mp1 mp2 =
   if ModPath.equal mp1 mp2 then ()
@@ -196,7 +197,8 @@ let rec subst_structure sub do_delta sign =
   in
   List.smartmap subst_body sign
 
-and subst_body is_mod sub do_delta mb =
+and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun is_mod sub subst_impl do_delta mb ->
   let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in
   let mp' = subst_mp sub mp in
   let sub =
@@ -205,10 +207,7 @@ and subst_body is_mod sub do_delta mb =
     else add_mp mp mp' empty_delta_resolver sub
   in
   let ty' = subst_signature sub do_delta ty in
-  let me' =
-    implem_smartmap
-      (subst_signature sub id_delta) (subst_expression sub id_delta) me
-  in
+  let me' = subst_impl sub me in
   let aty' = Option.smartmap (subst_expression sub id_delta) aty in
   let delta' = do_delta mb.mod_delta sub in
   if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
@@ -221,9 +220,14 @@ and subst_body is_mod sub do_delta mb =
       mod_type_alg = aty';
       mod_delta = delta' }
 
-and subst_module sub do_delta mb = subst_body true sub do_delta mb
+and subst_module sub do_delta mb =
+  subst_body true sub subst_impl do_delta mb
+
+and subst_impl sub me =
+  implem_smartmap
+    (subst_signature sub id_delta) (subst_expression sub id_delta) me
 
-and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb
+and subst_modtype sub do_delta mtb = subst_body false sub (fun _ () -> ()) do_delta mtb
 
 and subst_expr sub do_delta seb = match seb with
   |MEident mp ->
@@ -268,7 +272,7 @@ let add_retroknowledge mp =
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
         (Pp.str "had to import an unsupported kind of term.")
   in
-  fun lclrk env ->
+  fun (ModBodyRK lclrk) env ->
   (* The order of the declaration matters, for instance (and it's at the
      time this comment is being written, the only relevent instance) the
      int31 type registration absolutely needs int31 bits to be registered.
@@ -567,7 +571,7 @@ let rec is_bounded_expr l = function
       is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr
   | _ -> false
 
-let rec clean_module l mb =
+let rec clean_module_body l mb =
   let impl, typ = mb.mod_expr, mb.mod_type in
   let typ' = clean_signature l typ in
   let impl' = match impl with
@@ -577,19 +581,25 @@ let rec clean_module l mb =
   if typ==typ' && impl==impl' then mb
   else { mb with mod_type=typ'; mod_expr=impl' }
 
+and clean_module_type l mb =
+  let (), typ = mb.mod_expr, mb.mod_type in
+  let typ' = clean_signature l typ in
+  if typ==typ' then mb
+  else { mb with mod_type=typ' }
+
 and clean_field l field = match field with
   |(lab,SFBmodule mb) ->
-    let mb' = clean_module l mb in
+    let mb' = clean_module_body l mb in
     if mb==mb' then field else (lab,SFBmodule mb')
   |_ -> field
 
 and clean_structure l = List.smartmap (clean_field l)
 
 and clean_signature l =
-  functor_smartmap (clean_module l) (clean_structure l)
+  functor_smartmap (clean_module_type l) (clean_structure l)
 
 and clean_expression l =
-  functor_smartmap (clean_module l) (fun me -> me)
+  functor_smartmap (clean_module_type l) (fun me -> me)
 
 let rec collect_mbid l sign =  match sign with
   |MoreFunctor (mbid,ty,m) ->
@@ -613,14 +623,16 @@ let join_constant_body except otab cb =
   | _ -> ()
 
 let join_structure except otab s =
-  let rec join_module mb =
-    implem_iter join_signature join_expression mb.mod_expr;
+  let rec join_module : 'a. 'a generic_module_body -> unit = fun mb ->
     Option.iter join_expression mb.mod_type_alg;
     join_signature mb.mod_type
   and join_field (l,body) = match body with
     |SFBconst sb -> join_constant_body except otab sb
     |SFBmind _ -> ()
-    |SFBmodule m |SFBmodtype m -> join_module m
+    |SFBmodule m ->
+      implem_iter join_signature join_expression m.mod_expr;
+      join_module m
+    |SFBmodtype m -> join_module m
   and join_structure struc = List.iter join_field struc
   and join_signature sign =
     functor_iter join_module join_structure sign
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 04051f2e23..ad622b07d8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -574,7 +574,7 @@ let add_mind dir l mie senv =
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
-  let mtb = Declareops.hcons_module_body mtb in
+  let mtb = Declareops.hcons_module_type mtb in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -677,7 +677,7 @@ let build_module_body params restype senv =
       (struc,None,senv.modresolver,senv.univ) restype'
   in
   let mb' = functorize_module params mb in
-  { mb' with mod_retroknowledge = senv.local_retroknowledge }
+  { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -732,12 +732,12 @@ let end_module l restype senv =
 
 let build_mtb mp sign cst delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = delta;
-    mod_retroknowledge = [] }
+    mod_retroknowledge = ModTypeRK }
 
 let end_modtype l senv =
   let mp = senv.modpath in
@@ -853,7 +853,7 @@ let export ?except senv dir =
       mod_type_alg = None;
       mod_constraints = senv.univ;
       mod_delta = senv.modresolver;
-      mod_retroknowledge = senv.local_retroknowledge
+      mod_retroknowledge = ModBodyRK senv.local_retroknowledge
     }
   in
   let ast, symbols =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index b311165f10..b564b2a8c1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -416,7 +416,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 	     mod_type = subst_signature subst1 body_t1;
 	     mod_type_alg = None;
 	     mod_constraints = mtb1.mod_constraints;
-	     mod_retroknowledge = [];
+	     mod_retroknowledge = ModBodyRK [];
 	     mod_delta = mtb1.mod_delta} env
 	in
 	check_structure cst env body_t1 body_t2 equiv subst1 subst2
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 89c2a0ae30..f503c572d0 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -281,7 +281,8 @@ and extract_msignature_spec env mp1 reso = function
       MTfunsig (mbid, extract_mbody_spec env mp mtb,
 		extract_msignature_spec env' mp1 reso me)
 
-and extract_mbody_spec env mp mb = match mb.mod_type_alg with
+and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
+  fun env mp mb -> match mb.mod_type_alg with
   | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
   | None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type