Fix #8908: incorrect refresh of algebraic universes.

6 files changed, 27 insertions, 4 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b3848e1b5b..6345046431 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -891,6 +891,9 @@ let make_flexible_variable evd ~algebraic u =
   { evd with universes =
       UState.make_flexible_variable evd.universes ~algebraic u }
 
+let make_nonalgebraic_variable evd u =
+  { evd with universes = UState.make_nonalgebraic_variable evd.universes u }
+
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index be54bebcd7..0a8d1f3287 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -561,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid
 val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map
 (** See [UState.make_flexible_variable] *)
 
+val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
+(** See [UState.make_nonalgebraic_variable]. *)
+
 val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t 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 41905feab7..dc760e7f97 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -577,6 +577,9 @@ let make_flexible_variable ctx ~algebraic u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
+let make_nonalgebraic_variable ctx u =
+  { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic }
+
 let make_flexible_nonalgebraic ctx =
   {ctx with uctx_univ_algebraic = Univ.LSet.empty}
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 8053a7bf83..ad0cd5c1bb 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t
   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. *)
+  universe. Otherwise the variable is just made flexible.
+
+    If [l] is already algebraic it will remain so even with [algebraic:false]. *)
 val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
 
+val make_nonalgebraic_variable : t -> Univ.Level.t -> t
+(** Make the level non algebraic. Undefined behaviour on
+   already-defined algebraics. *)
+
 (** Turn all undefined flexible algebraic variables into simply flexible
    ones. Can be used in case the variables might appear in universe instances
    (typically for polymorphic program obligations). *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96213af9c6..4692fe0057 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       if not onlyalg then refresh_sort status ~direction s
 	       else t
 	    | UnivFlexible alg ->
-	       if onlyalg && alg then
-	         (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
-	       else t))
+               (if alg then
+                  evdref := Evd.make_nonalgebraic_variable !evdref l);
+               t))
       | Set when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
           only refreshing when we want higher universes. *)
diff --git a/test-suite/bugs/closed/bug_8908.v b/test-suite/bugs/closed/bug_8908.v
new file mode 100644
index 0000000000..9c85839b75
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8908.v
@@ -0,0 +1,8 @@
+Record foo : Type :=
+  { fooA : Type; fooB : Type }.
+Definition id {A : Type} (a : A) := a.
+Definition untypable : Type.
+  unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y).
+  exact foo.
+  constructor. exact unit. exact unit.
+Defined.