Univs: correct handling of with in modules

For polymorphic and non-polymorphic parameters and definitions, fixes
bugs #4298, #4294

4 files changed, 93 insertions, 22 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7da0958ea..3be89afbd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,33 +72,64 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
-      let env' = Environ.add_constraints ccst env' in
-      let newus, cst = Univ.UContext.dest ctx in
-      let ctxs = Univ.ContextSet.of_context ctx in
-      let env' = Environ.add_constraints cst env' in
-      let c',ctx' = match cb.const_body with
-	| Undef _ | OpaqueDef _ ->
-	  let j = Typeops.infer env' c in
-	  let typ = Typeops.type_of_constant_type env' cb.const_type in
-	  let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-	    j.uj_type typ in
-	    j.uj_val, Univ.ContextSet.add_constraints cst' ctxs
-	| Def cs ->
-	  let cst' = Reduction.infer_conv env' (Environ.universes env') c
-	    (Mod_subst.force_constr cs) in
-	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
-	    (* if cb.const_polymorphic then  *)Univ.ContextSet.add_constraints cst' ctxs
-	    (* else cst' +++ cst *)
+      let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
+      let uctx = (* Context of the spec *)
+	if cb.const_polymorphic then
+	  Univ.instantiate_univ_context uctx
+	else uctx
+      in
+      let c', univs, ctx' = 
+	if not cb.const_polymorphic then
+	  let env' = Environ.push_context ~strict:true uctx env' in
+	  let env' = Environ.push_context ~strict:true ctx env' in
+	  let c',cst = match cb.const_body with
+	    | Undef _ | OpaqueDef _ ->
+	      let j = Typeops.infer env' c in
+	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+						j.uj_type typ in
+	      j.uj_val, cst'
+	    | Def cs ->
+	       let c' = Mod_subst.force_constr cs in
+	         c, Reduction.infer_conv env' (Environ.universes env') c c'
+	  in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+	else
+	  let cus, ccst = Univ.UContext.dest uctx in
+	  let newus, cst = Univ.UContext.dest ctx in
+	  let () =
+	    if not (Univ.Instance.length cus == Univ.Instance.length newus) then
+	      error_incorrect_with_constraint lab
+	  in
+	  let inst = Univ.Instance.append cus newus in
+	  let csti = Univ.enforce_eq_instances cus newus cst in
+	  let csta = Univ.Constraint.union csti ccst in
+	  let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
+	  let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+		     error_incorrect_with_constraint lab
+	  in
+	  let cst = match cb.const_body with
+	    | Undef _ | OpaqueDef _ ->
+	      let j = Typeops.infer env' c in
+	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+						j.uj_type typ in
+	      cst'
+	    | Def cs ->
+	       let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+	        cst'
 	  in
-            c, cst
+	    if not (Univ.Constraint.is_empty cst) then
+	      error_incorrect_with_constraint lab;
+	    let subst, ctx = Univ.abstract_universes true ctx in
+	      Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
-	  const_universes = Univ.ContextSet.to_context ctx' }
+	  const_universes = univs;
+	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 463e28a1c..58f3bcdf0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -322,7 +322,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
 		  error (IncompatibleUniverses incon)
-	else cst, env, Univ.Instance.empty
+	else
+	  cst, env, Univ.Instance.empty
       in
       (* Now check types *)
       let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -459,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   let env = add_module_type sup.mod_mp sup env in
+  let env = Environ.push_context_set ~strict:true super.mod_constraints env in
   check_modtypes Univ.Constraint.empty env
     (strengthen sup sup.mod_mp) super empty_subst
     (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/test-suite/bugs/closed/4294.v b/test-suite/bugs/closed/4294.v
new file mode 100644
index 000000000..1d5e3c71b
--- /dev/null
+++ b/test-suite/bugs/closed/4294.v
@@ -0,0 +1,31 @@
+Require Import Hurkens.
+
+Module NonPoly.
+Module Type Foo.
+  Definition U := Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type.
+  Definition U := Type.
+  Definition eq : Type = U := eq_refl.
+End M.
+
+Print Universes.
+Fail Definition bad : False := TypeNeqSmallType.paradox M.U M.eq.
+End NonPoly.
+
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type.
+  Monomorphic Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type.
+  Definition U := Type.
+  Monomorphic Definition eq : Type = U := eq_refl.
+End M.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox Type M.eq.
+(* Print Assumptions bad. *)
diff --git a/test-suite/bugs/closed/4298.v b/test-suite/bugs/closed/4298.v
new file mode 100644
index 000000000..875612ddf
--- /dev/null
+++ b/test-suite/bugs/closed/4298.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type.
+End Foo.
+
+Fail Module M : Foo with Definition U := Prop.