Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.

2 files changed, 15 insertions, 1 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 651c76ae1..b3858146d 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -642,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs =
   let env = Global.env () in
   let mty_entry_o, subs, inl_res = match res with
     | Enforce (mty,ann) ->
-        Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
+        let inl = inl2intopt ann in
+        let mte, _ = interp_modast env ModType mty in
+        (* We check immediately that mte is well-formed *)
+        let _ = Mod_typing.translate_mse env None inl mte in
+        Some mte, [], inl
     | Check mtys ->
 	None, build_subtypes interp_modast env mp arg_entries_r mtys,
         default_inline ()
diff --git a/test-suite/bugs/closed/4713.v b/test-suite/bugs/closed/4713.v
new file mode 100644
index 000000000..5d4d73be3
--- /dev/null
+++ b/test-suite/bugs/closed/4713.v
@@ -0,0 +1,10 @@
+Module Type T.
+  Parameter t : Type.
+End T.
+Module M : T.
+  Definition t := unit.
+End M.
+
+Fail Module Z : T with Module t := M := M.
+Fail Module Z <: T with Module t := M := M.
+Fail Declare Module Z : T with Module t := M.