From 1974816aca996fe3ee9420b83f11d15923e70fda Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jul 2017 11:41:25 +0200
Subject: Separating the module_type and module_body types by using a type
 parameter.

As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
---
 kernel/declarations.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9697b0b8b2..1b32d343ee 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -250,9 +250,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 *)
     mod_type_alg : module_expression option; (** algebraic type *)
     mod_constraints : Univ.ContextSet.t; (**
@@ -269,13 +269,14 @@ 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
 
 (** Extra invariants :
 
-- 
cgit v1.2.3


From 37b81fe10d2da12180d96d931ba2b76370e1eea5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jul 2017 14:23:37 +0200
Subject: Statically enforcing that module types have no retroknowledge.

---
 kernel/declarations.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1b32d343ee..e17fb1c38f 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
-- 
cgit v1.2.3