From e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 23:33:42 +0200
Subject: Cleaning up the implementation of module subtyping in the kernel.

We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.

We also add a few tests for module subtyping in presence of polymorphic
constants.
---
 kernel/mod_typing.ml | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 71c0370083..69fbd0f325 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,37 +92,28 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	         c, Reduction.infer_conv env' (Environ.universes env') c c'
 	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
         | Polymorphic_const uctx ->
-          let uctx = Univ.instantiate_univ_context uctx in
-	  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 (UGraph.check_constraints cst (Environ.universes env')) then
-		     error_incorrect_with_constraint lab
-	  in
+          let subst, ctx = Univ.abstract_universes ctx in
+          let c = Vars.subst_univs_level_constr subst c in
+          let () =
+            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+              error_incorrect_with_constraint lab
+          in
+	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env 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 typ = Vars.subst_instance_constr cus typ 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 c' = Mod_subst.force_constr cs in
 	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
 	        cst'
 	  in
 	    if not (Univ.Constraint.is_empty cst) then
 	      error_incorrect_with_constraint lab;
-	    let subst, ctx = Univ.abstract_universes ctx in
-	      Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
+            c, Polymorphic_const ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
 (*      let ctx' = Univ.UContext.make (newus, cst) in *)
-- 
cgit v1.2.3


From 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 11:44:53 +0200
Subject: Adding a comment regarding De Bruijn universe indices in the kernel.

---
 kernel/mod_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 69fbd0f325..c7f3e5c51b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -98,6 +98,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
+          (** Terms are compared in a context with De Bruijn universe indices *)
 	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
-- 
cgit v1.2.3