Merge PR #8786: Adding a regression test for bug #8785: universe constraints missing

1 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v
new file mode 100644
index 0000000000..b10569499e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8785.v
@@ -0,0 +1,44 @@
+Universe u v w.
+Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := .
+
+Inductive FiniteT : Type -> Prop :=
+  | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T)
+  | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X ->
+    invertible f -> FiniteT Y.
+
+Set Printing Universes.
+
+Axiom a : False.
+(*
+Constraint v <= u.
+Constraint v <= w.
+*)
+Lemma finite_subtype: forall (X:Type) (P:X->Prop),
+  FiniteT X -> (forall x:X, P x \/ ~ P x) ->
+  FiniteT {x:X | P x}.
+Proof.
+intros.
+induction H.
+
+destruct (H0 None).
+elim a.
+
+pose (g := fun (x:{x:T | P (Some x)}) =>
+  match x return {x:option T | P x} with
+    | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+pose (g := fun (x:{x:X | P (f x)}) =>
+  match x with
+  | exist _ x0 i => exist (fun x:Y => P x) (f x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+Qed.