Local universes for opaque polymorphic constants.

11 files changed, 61 insertions, 16 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b39aed01e8..f4b4834d98 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -158,6 +158,7 @@ type result = {
   cook_body : constant_def;
   cook_type : types;
   cook_universes : constant_universes;
+  cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
@@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 =
     else
       let ainst = Univ.make_abstract_instance auctx in
       let subst = Instance.append subst ainst in
-      let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
+      let substf = Univ.make_instance_subst subst in
+      let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
       subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons { from = cb; info } =
@@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } =
 		  hyps)
       hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
+  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
+                                            (Univ.make_instance_subst usubst)))
+      cb.const_private_poly_univs
+  in
   {
     cook_body = body;
     cook_type = typ;
     cook_universes = univs;
+    cook_private_univs = private_univs;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
   }
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 6ebe691b83..7ff4b657d3 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,6 +21,7 @@ type result = {
   cook_body : constant_def;
   cook_type : types;
   cook_universes : constant_universes;
+  cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156..68ccd933e7 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -78,6 +78,7 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
+    const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..90638be3ec 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -101,6 +101,7 @@ let subst_const_body sub cb =
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
+        const_private_poly_univs = cb.const_private_poly_univs;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
 
@@ -126,14 +127,20 @@ let hcons_const_universes cbu =
   match cbu with
   | Monomorphic_const ctx -> 
     Monomorphic_const (Univ.hcons_universe_context_set ctx)
-  | Polymorphic_const ctx -> 
+  | Polymorphic_const ctx ->
     Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
 
+let hcons_const_private_univs = function
+  | None -> None
+  | Some univs -> Some (Univ.hcons_universe_context_set univs)
+
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
-    const_universes = hcons_const_universes cb.const_universes }
+    const_universes = hcons_const_universes cb.const_universes;
+    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
+  }
 
 (** {6 Inductive types } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..a6bc579cf7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -380,6 +380,18 @@ let add_universes_set strict ctx g =
 let push_context_set ?(strict=false) ctx env =
   map_universes (add_universes_set strict ctx) env
 
+let push_subgraph (levels,csts) env =
+  let add_subgraph g =
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = UGraph.merge_constraints csts newg in
+    (if not (Univ.Constraint.is_empty csts) then
+       let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
+       (if not (UGraph.check_constraints restricted g) then
+          CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints.")));
+    newg
+  in
+  map_universes add_subgraph env
+
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fc..dd0df7d3d6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -268,6 +268,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
 val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
+val push_subgraph : Univ.ContextSet.t -> env -> env
+(** [push_subgraph univs env] adds the universes and constraints in
+   [univs] to [env] as [push_context_set ~strict:false univs env], and
+   also checks that they do not imply new transitive constraints
+   between pre-existing universes in [env]. *)
+
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0dde1c7e75..f43dbd88f9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver =
       | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
     in
       { cb with
-	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+        const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+        const_private_poly_univs = None;
 	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2464df799e..98a7014bee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -599,7 +599,7 @@ let inline_side_effects env body side_eff =
         let subst = Cmap_env.add c (Inr var) subst in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
-      | Polymorphic_const _auctx ->
+      | Polymorphic_const _ ->
         (** Inline the term to emulate universe polymorphism *)
         let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 35fa871b4e..f9fdbdd68e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = Undef nl;
         cook_type = t;
         cook_universes = univs;
+        cook_private_univs = None;
         cook_inline = false;
         cook_context = ctx;
       }
@@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = Monomorphic_const univs;
+        cook_private_univs = None;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
@@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let body, ctx', _ = handle env body side_eff in
         body, Univ.ContextSet.union ctx ctx'
       in
-      let env, usubst, univs = match c.const_entry_universes with
+      let env, usubst, univs, private_univs = match c.const_entry_universes with
       | Monomorphic_const_entry univs ->
         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
+        env, Univ.empty_level_subst, Monomorphic_const ctx, None
       | 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
-            side-effects. The first property is ruled out by upper layers,
-            and the second one is ensured by the fact we currently
-            unconditionally export side-effects from polymorphic definitions,
-            i.e. [trust] is always [Pure]. *)
-        let () = assert (Univ.ContextSet.is_empty ctx) in
+        (** [ctx] must contain local universes, such that it has no impact
+            on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        env, sbst, Polymorphic_const auctx
+        let env, local =
+          if opaque then
+            push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
+          else
+          if Univ.ContextSet.is_empty ctx then env, None
+          else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+        in
+        env, sbst, Polymorphic_const auctx, local
       in
       let j = infer env body in
       let typ = match typ with
@@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
+        cook_private_univs = private_univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
@@ -277,6 +281,7 @@ let build_constant_declaration _kn env result =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
+    const_private_poly_univs = result.cook_private_univs;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9083156745..fe07a1c90e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -866,6 +866,8 @@ let constraints_for ~kept g =
         arc.ltle csts)
     kept csts
 
+let domain g = LMap.domain g.entries
+
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
     will be strict most of the time), but is not necessarily minimal.
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index a2cc5b3116..a389b35993 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -79,6 +79,9 @@ val constraints_of_universes : t -> Constraint.t * LSet.t list
     eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *)
 val constraints_for : kept:LSet.t -> t -> Constraint.t
 
+val domain : t -> LSet.t
+(** Known universes *)
+
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)