Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.

6 files changed, 56 insertions, 12 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ea098902a..d303038c5 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
-let universes_of_constr sigma c =
+let universes_of_constr env sigma c =
   let open Univ in
+  let open Declarations in
   let rec aux s c =
     match kind sigma c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
     | Sort u ->
        let sort = ESorts.kind sigma u in
        if Sorts.is_small sort then s
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3e6a13f70..651ccbb10 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -203,7 +203,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
    type of evars appearing in it. *)
-val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
 
 (** {6 Substitutions} *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index c28e78f7d..6566ad989 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -22,6 +22,7 @@ type uinfo = {
 type t =
  { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
+   uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.LSet.t; 
@@ -34,6 +35,7 @@ type t =
 let empty =
   { uctx_names = UNameMap.empty, Univ.LMap.empty;
     uctx_local = Univ.ContextSet.empty;
+    uctx_seff_univs = Univ.LSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_universes = UGraph.initial_universes;
@@ -60,6 +62,7 @@ let union ctx ctx' =
   else if is_empty ctx' then ctx
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
+    let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in
     let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
                                (Univ.ContextSet.levels ctx.uctx_local) in
@@ -70,6 +73,7 @@ let union ctx ctx' =
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
         uctx_local = local;
+        uctx_seff_univs = seff;
         uctx_univ_variables = 
           Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
         uctx_univ_algebraic = 
@@ -365,12 +369,21 @@ let check_univ_decl ~poly uctx decl =
   ctx
 
 let restrict ctx vars =
+  let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
+let demote_seff_univs entry uctx =
+  let open Entries in
+  match entry.const_entry_universes with
+  | Polymorphic_const_entry _ -> uctx
+  | Monomorphic_const_entry (univs, _) ->
+    let seff = Univ.LSet.union uctx.uctx_seff_univs univs in
+    { uctx with uctx_seff_univs = seff }
+
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
@@ -552,7 +565,8 @@ let refresh_undefined_univ_variables uctx =
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
-               uctx_local = ctx'; 
+               uctx_local = ctx';
+               uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
                uctx_initial_universes = initial } in
@@ -569,7 +583,8 @@ let normalize uctx =
       Universes.refresh_constraints uctx.uctx_initial_universes us'
     in
       { uctx_names = uctx.uctx_names;
-        uctx_local = us'; 
+        uctx_local = us';
+        uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *)
         uctx_univ_variables = vars'; 
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
diff --git a/engine/uState.mli b/engine/uState.mli
index 2c39e85f7..5dfe9a22d 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 val restrict : t -> Univ.LSet.t -> t
 
+val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
+
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
diff --git a/engine/univops.ml b/engine/univops.ml
index 9a9ae12ca..df25d8725 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -9,12 +9,25 @@
 open Univ
 open Constr
 
-let universes_of_constr c =
+let universes_of_constr env c =
+  let open Declarations in
   let rec aux s c = 
     match kind c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) -> 
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
+    | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
diff --git a/engine/univops.mli b/engine/univops.mli
index 9af568bcb..30fcc4368 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -9,7 +9,8 @@
 open Constr
 open Univ
 
-(** Shrink a universe context to a restricted set of variables *)
+(** The universes of monomorphic constants appear. *)
+val universes_of_constr : Environ.env -> constr -> LSet.t
 
-val universes_of_constr : constr -> LSet.t
+(** Shrink a universe context to a restricted set of variables *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t