Univs: fix bug #5365, generation of u+k <= v constraints

Use an explicit label ~algebraic for make_flexible_variable as well.

4 files changed, 23 insertions, 8 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index c2f848291b..ac31728f43 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -809,8 +809,9 @@ let new_sort_variable ?loc ?name rigid d =
 let add_global_univ d u =
   { d with universes = UState.add_global_univ d.universes u }
 
-let make_flexible_variable evd b u =
-  { evd with universes = UState.make_flexible_variable evd.universes b u }
+let make_flexible_variable evd ~algebraic u =
+  { evd with universes =
+      UState.make_flexible_variable evd.universes ~algebraic u }
 
 let make_evar_universe_context e l =
   let uctx = UState.make (Environ.universes e) in
diff --git a/engine/evd.mli b/engine/evd.mli
index 86887f3dcc..93d4a9d152 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -526,7 +526,9 @@ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 
 val universe_rigidity : evar_map -> Univ.Level.t -> rigid
-val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
+val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map
+(** See [UState.make_flexible_variable] *)
+
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
diff --git a/engine/uState.ml b/engine/uState.ml
index c35f97b2e9..146a386a29 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -381,16 +381,21 @@ let add_global_univ uctx u =
                                      uctx_initial_universes = initial;
                                      uctx_universes = univs }
 
-let make_flexible_variable ctx b u =
-  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
+let make_flexible_variable ctx ~algebraic u =
+  let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
   let uvars' = Univ.LMap.add u None uvars in
   let avars' = 
-    if b then
+    if algebraic then
       let uu = Univ.Universe.make u in
       let substu_not_alg u' v =
         Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
       in
-        if not (Univ.LMap.exists substu_not_alg uvars)
+      let has_upper_constraint () =
+        Univ.Constraint.exists
+          (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u)
+          (Univ.ContextSet.constraints cstrs)
+      in
+        if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ())
         then Univ.LSet.add u avars else avars 
     else avars 
   in
diff --git a/engine/uState.mli b/engine/uState.mli
index 0cdc6277a5..3776e4c9fd 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -92,7 +92,14 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
-val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+(** [make_flexible_variable g algebraic l]
+
+  Turn the variable [l] flexible, and algebraic if [algebraic] is true
+  and [l] can be. That is if there are no strict upper constraints on
+  [l] and and it does not appear in the instance of any non-algebraic
+  universe. Otherwise the variable is just made flexible. *)
+val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
 
 val is_sort_variable : t -> Sorts.t -> Univ.Level.t option