Statically enforcing that module types have no retroknowledge.

5 files changed, 20 insertions, 10 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1b32d343e..e17fb1c38 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -259,7 +259,7 @@ and 'a generic_module_body =
       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]
@@ -278,6 +278,11 @@ and module_body = module_implementation generic_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 :
 
     - No [MEwith] inside a [mod_expr] implementation : the 'with' syntax
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index eead5b70d..d2b41aae9 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -283,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 () 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
   |[] ->
@@ -321,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 925d042b1..76915e917 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -143,10 +143,12 @@ let rec functor_iter fty f0 = function
 (** {6 Misc operations } *)
 
 let module_type_of_module mb =
-  { mb with mod_expr = (); mod_type_alg = None }
+  { mb with mod_expr = (); mod_type_alg = None;
+    mod_retroknowledge = ModTypeRK; }
 
 let module_body_of_type mp mtb =
-  { mtb with mod_expr = Abstract; 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 ()
@@ -270,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.
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index aa26405f7..ad622b07d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -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
@@ -737,7 +737,7 @@ let build_mtb mp sign cst delta =
     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 b311165f1..b564b2a8c 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