Test file for #7723

2 files changed, 59 insertions, 3 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 1b909a8d0..f17313230 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -258,14 +258,12 @@ let pos_universe_var i r sz =
   (* Compilation of a universe variable can happen either at toplevel (the
   current closure correspond to a constant and has local universes) or in a
   local closure (which has no local universes). *)
-  if r.nb_uni_stack != 0 then begin
+  if r.nb_uni_stack != 0 then
     (* Universe variables are represented by De Bruijn levels (not indices),
     starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq]
     with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access
     the last universe. *)
-    Printf.eprintf "pos_univ i=%i sz=%i arity=%i nb_univ=%i\n" i sz r.arity r.nb_uni_stack;
     Kacc (sz - r.arity - (r.nb_uni_stack - i))
-  end
   else
     let env = !(r.in_env) in
     let db = FVuniv_var i in
diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v
new file mode 100644
index 000000000..216290123
--- /dev/null
+++ b/test-suite/bugs/closed/7723.v
@@ -0,0 +1,58 @@
+Set Universe Polymorphism.
+
+Module Segfault.
+
+Inductive decision_tree : Type := .
+
+Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B
+  := match ls with
+     | nil => None
+     | cons x xs
+       => match f x with
+          | Some v => Some v
+          | None => first_satisfying_helper f xs
+          end
+     end.
+
+Axiom admit : forall {T}, T.
+Definition dtree4 : option decision_tree :=
+  match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil)
+  with
+  | Some _ => admit
+  | None => admit
+  end
+.
+Definition dtree'' := Eval vm_compute in dtree4. (* segfault *)
+
+End Segfault.
+
+Module OtherExample.
+
+Definition bar@{i} := Type@{i}.
+Definition foo@{i j} (x y z : nat) :=
+  @id Type@{j} bar@{i}.
+Eval vm_compute in foo.
+
+End OtherExample.
+
+Module LocalClosure.
+
+Definition bar@{i} := Type@{i}.
+
+Definition foo@{i j} (x y z : nat) :=
+  @id (nat -> Type@{j}) (fun _ => Type@{i}).
+Eval vm_compute in foo.
+
+End LocalClosure.
+
+Require Import Hurkens.
+Polymorphic Inductive unit := tt.
+
+Polymorphic Definition foo :=
+  let x := id tt in (x, x, Type).
+
+Lemma bad : False.
+  refine (TypeNeqSmallType.paradox (snd foo) _).
+  vm_compute.
+  Fail reflexivity.
+Abort.