Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)

 When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1]
 in the environment. But since the stricter checks of commit r14150, this
 is an error if the environment already knows [mtb1] (for instance
 when doing (F M) and checking that M is compatible with the type of the
 arg of F.

 [check_subtypes] now expect [mtb1] to be already in env, and we move the
 add_module to the unique call site of this function that requires it.

 Moreover, we solve a second issue : when subtyping a functor, we
 update the environment once inside the functor, and this is also
 refused by the checks of commits r14150. So we first remove the module
 name from the env before doing the update. Since the module added
 earlier was a functor, there is no inner defs to chase in env.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 31 insertions, 16 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index fbe9d9ee2..99b364579 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -191,6 +191,15 @@ let shallow_add_module mp mb env =
 	env_modules = new_mods } in
   { env with env_globals = new_globals }
 
+let shallow_remove_module mp env =
+  if not (MPmap.mem mp env.env_globals.env_modules) then
+    Printf.ksprintf anomaly "Module %s is unknown"
+      (string_of_mp mp);
+  let new_mods = MPmap.remove mp env.env_globals.env_modules in
+  let new_globals =
+    { env.env_globals with
+	env_modules = new_mods } in
+  { env with env_globals = new_globals }
 
 let lookup_module mp env =
   MPmap.find mp env.env_globals.env_modules
diff --git a/checker/environ.mli b/checker/environ.mli
index add7c7060..628febbb0 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -69,5 +69,6 @@ val add_modtype :
   module_path -> Declarations.module_type_body -> env -> env
 val shallow_add_module :
   module_path -> Declarations.module_body -> env -> env
+val shallow_remove_module : module_path -> env -> env
 val lookup_module : module_path -> env -> Declarations.module_body
 val lookup_modtype : module_path -> env -> Declarations.module_type_body
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 315571705..9942816d1 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -253,18 +253,22 @@ and check_module env mp mb =
 	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
 	let (_:struct_expr_body) =
 	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
-          check_subtypes env 
-	    {typ_mp=mp;
-	     typ_expr=sign;
-	     typ_expr_alg=None;
-	     typ_constraints=Univ.empty_constraint;
-	     typ_delta = mb.mod_delta;}
-	    {typ_mp=mp;
-	     typ_expr=mb.mod_type;
-	     typ_expr_alg=None;
-	     typ_constraints=Univ.empty_constraint;
-	     typ_delta = mb.mod_delta;};
-	  
+	let mtb1 =
+	  {typ_mp=mp;
+	   typ_expr=sign;
+	   typ_expr_alg=None;
+	   typ_constraints=Univ.empty_constraint;
+	   typ_delta = mb.mod_delta;}
+	and mtb2 =
+	  {typ_mp=mp;
+	   typ_expr=mb.mod_type;
+	   typ_expr_alg=None;
+	   typ_constraints=Univ.empty_constraint;
+	   typ_delta = mb.mod_delta;}
+	in
+	let env = add_module (module_body_of_type mp mtb1) env in
+	check_subtypes env mtb1 mtb2
+
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0603300ba..0c97254b5 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -348,7 +348,8 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
 		(module_body_of_type (MPbound arg_id2) arg_t2) env 
 	      in
 	      let env = match body_t1 with
-		  SEBstruct str -> 
+		  SEBstruct str ->
+		    let env = shallow_remove_module mtb1.typ_mp env in
 		    add_module {mod_mp = mtb1.typ_mp;
 				mod_expr = None;
 				mod_type = body_t1;
@@ -367,8 +368,5 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
      else check_structure  env mtb1' mtb2' equiv subst1 subst2
 
 let check_subtypes env sup super =
-  (*if sup<>super then*)
-  let env = add_module (module_body_of_type sup.typ_mp sup) env
-  in
   check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
       (map_mp super.typ_mp sup.typ_mp) false
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 07f48789d..ecdf55775 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -13,6 +13,9 @@ open Declarations
 open Environ
 (*i*)
 
+(** Invariant: the first [module_type_body] is now supposed to be
+    known by [env] *)
+
 val check_subtypes : env -> module_type_body -> module_type_body -> unit