Fix bug #8432 : program fixpoint and universes

One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v
new file mode 100644
index 0000000000..844ee12668
--- /dev/null
+++ b/test-suite/bugs/closed/8432.v
@@ -0,0 +1,39 @@
+Require Import Program.Tactics.
+
+Obligation Tactic := idtac.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Inductive Empty : Type :=.
+Inductive Unit : Type := tt.
+Definition not (A : Type) := A -> Empty.
+
+  Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty.
+  Proof. refine (
+    match H in paths _ i return
+      match i with
+      | O => Unit
+      | S _ => Empty
+      end
+    with
+    | idpath _ => tt
+    end
+  ). Defined.
+  Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x.
+  Proof.
+    destruct p. apply idpath.
+  Defined.
+  Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty.
+  Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined.
+Set Printing Universes.
+Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) :=
+match n as n return not (paths (S n) 0) with
+| 0 => nat_path_S_O _
+| S n' => let dummy := succ_not_zero n' in _
+end.
+Next Obligation.
+  intros f _ n dummy H. exact (nat_path_S_O _ H).
+  Show Universes.
+Defined.