Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

6 files changed, 41 insertions, 30 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b621a3fe2f..6a721a1a8a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -702,7 +702,7 @@ let empty = {
 }
 
 let from_env e = 
-  { empty with universes = UState.make (Environ.universes e) }
+  { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
 
 let from_ctx ctx = { empty with universes = ctx }
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 5ed016e0d0..cb40e6eadd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,6 +34,7 @@ type t =
    (** The subset of unification variables that can be instantiated with
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
@@ -47,6 +48,7 @@ let empty =
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
     uctx_universes = initial_sprop_cumulative;
+    uctx_universes_lbound = Univ.Level.set;
     uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
@@ -54,10 +56,12 @@ let elaboration_sprop_cumul =
   Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
-let make u =
+let make ~lbound u =
   let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
-    { empty with 
-      uctx_universes = u; uctx_initial_universes = u}
+    { empty with
+      uctx_universes = u;
+      uctx_universes_lbound = lbound;
+      uctx_initial_universes = u}
 
 let is_empty ctx =
   ContextSet.is_empty ctx.uctx_local &&
@@ -83,7 +87,7 @@ let union ctx ctx' =
     let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in
     let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in
     let declarenew g =
-      LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g
     in
     let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
@@ -99,6 +103,7 @@ let union ctx ctx' =
            else
              let cstrsr = ContextSet.constraints ctx'.uctx_local in
              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
+        uctx_universes_lbound = ctx.uctx_universes_lbound;
         uctx_weak_constraints = weak}
 
 let context_set ctx = ctx.uctx_local
@@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl =
       (ContextSet.constraints uctx.uctx_local);
   ctx
 
-let restrict_universe_context (univs, csts) keep =
+let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
   if LSet.is_empty removed then univs, csts
   else
   let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
   let g = UGraph.initial_universes in
-  let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in
+  let g = LSet.fold (fun v g -> if Level.is_small v then g else
+                        UGraph.add_universe v ~lbound ~strict:false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
   let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
   let csts = Constraint.filter (fun (l,d,r) ->
-      not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+      not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
@@ -450,7 +456,7 @@ let restrict ctx vars =
   let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 let demote_seff_univs universes uctx =
@@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
     else ContextSet.append ctx' uctx.uctx_local in
   let declare g =
     LSet.fold (fun u g ->
-               try UGraph.add_universe u false g
+               try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
                with UGraph.AlreadyDeclared when sideff -> g)
               levels g
   in
@@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name
     | None -> add_uctx_loc u loc uctx.uctx_names
   in
   let initial =
-    UGraph.add_universe u false uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes
   in                                                 
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-                uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+                uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false
+                    u uctx.uctx_universes;
                 uctx_initial_universes = initial}
   in uctx', u
 
-let make_with_initial_binders e us =
-  let uctx = make e in
+let make_with_initial_binders ~lbound e us =
+  let uctx = make ~lbound e in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
@@ -561,10 +568,10 @@ let make_with_initial_binders e us =
 
 let add_global_univ uctx u =
   let initial =
-    UGraph.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
   in
   let univs = 
-    UGraph.add_universe u true uctx.uctx_universes
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
                                      uctx_initial_universes = initial;
@@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx =
       uctx.uctx_univ_variables LMap.empty
   in
   let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in
-  let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g)
-                                   (ContextSet.levels ctx') g in
+  let lbound = uctx.uctx_universes_lbound in
+  let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
+      (ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
@@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx =
                uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
+               uctx_universes_lbound = lbound;
                uctx_initial_universes = initial;
                uctx_weak_constraints = weak; } in
     uctx', subst
 
 let minimize uctx =
   let open UnivMinim in
+  let lbound = uctx.uctx_universes_lbound in
   let ((vars',algs'), us') =
-    normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
+    normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
   in
   if ContextSet.equal us' uctx.uctx_local then uctx
@@ -709,6 +719,7 @@ let minimize uctx =
         uctx_univ_variables = vars'; 
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
+        uctx_universes_lbound = lbound;
         uctx_initial_universes = uctx.uctx_initial_universes;
         uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 9689f2e961..52e48c4eeb 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : UGraph.t -> t
+val make : lbound:Univ.Level.t -> UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1b7c33b9c1..30fdd28997 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
 (* TODO check is_small/sprop *)
-let normalize_context_set g ctx us algs weak =
+let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
@@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak =
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+    let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g)
                            ctx UGraph.initial_universes
     in
     let add_soft u g =
       if not (Level.is_small u || LSet.mem u ctx)
-      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g
       else g
     in
     let g = Constraint.fold
@@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak =
   (* We ignore the trivial Prop/Set <= i constraints. *)
   let noneqs =
     Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+      (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
                            (Level.is_prop l && d == Lt && Level.is_set r)))
       csts
   in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 21f6efe86a..72b432e62f 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 6cc7868a38..1f1edbed16 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 [@@ocaml.deprecated "Use [UState.restrict_universe_context]"]