Adding universe names to polymorphic entry instances.

6 files changed, 22 insertions, 12 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..87fa385a60 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 
 type inductive_universes =
   | Monomorphic_ind_entry of Univ.ContextSet.t
-  | Polymorphic_ind_entry of Univ.UContext.t
-  | Cumulative_ind_entry of Univ.CumulativityInfo.t
+  | Polymorphic_ind_entry of Name.t list * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t list * Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
   | Monomorphic_const_entry of Univ.ContextSet.t
-  | Polymorphic_const_entry of Univ.UContext.t
+  | Polymorphic_const_entry of Name.t list * Univ.UContext.t
 
 type 'a in_constant_universes_entry = 'a * constant_universes_entry
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..2d74f99c15 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
   let env' =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry ctx -> push_context_set ctx env
-    | Polymorphic_ind_entry ctx -> push_context ctx env
-    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
   let env_params = check_context env' mie.mind_entry_params in
   let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry _ -> ()
     | Polymorphic_ind_entry _ -> ()
-    | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+    | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
@@ -851,12 +851,14 @@ let compute_projections (kn, i as ind) mib =
 let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
-  | Polymorphic_ind_entry ctx -> 
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in
     let (inst, auctx) = Univ.abstract_universes ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry cumi -> 
+  | Cumulative_ind_entry (nas, cumi) ->
     let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+    let () = assert (Int.equal (List.length nas) (Instance.length inst)) in
     let inst = Univ.make_instance_subst inst in
     (inst, Cumulative_ind acumi)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b11851bbb..df10398b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u =
     | Monomorphic_const uctx ->
       Monomorphic_const_entry uctx
     | Polymorphic_const auctx ->
-      Polymorphic_const_entry (Univ.AUContext.repr auctx)
+      Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..4759625e8a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,7 +68,8 @@ let feedback_completion_typecheck =
 let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
-  | Polymorphic_const_entry uctx ->
+  | Polymorphic_const_entry (nas, uctx) ->
+    let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
     let sbst, auctx = Univ.abstract_universes uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
@@ -78,7 +79,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
         | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
-        | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+        | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
       in
       let j = infer env t in
       let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
         env, Univ.empty_level_subst, Monomorphic_const ctx
-      | Polymorphic_const_entry uctx ->
+      | Polymorphic_const_entry (nas, uctx) ->
         (** Ensure not to generate internal constraints in polymorphic mode.
             The only way for this to happen would be that either the body
             contained deferred universes, or that it contains monomorphic
@@ -159,6 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             unconditionally export side-effects from polymorphic definitions,
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
+        let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes uctx in
         let sbst = Univ.make_instance_subst sbst in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..35566019a8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -948,6 +948,9 @@ struct
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
+  (** FIXME: Actually store this information in the type *)
+  let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u
+
 end
 
 let hcons_abstract_universe_context = AUContext.hcons
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..bc902d8f4b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -347,6 +347,9 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
+  val names : t -> Names.Name.t list
+  (** Return the names of the bound universe variables *)
+
 end
 
 (** Universe info for cumulative inductive types: A context of