Univs: fix bug #4161.

Retypecheck abstracted infered predicate to register the right
universe constraints.

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v
new file mode 100644
index 000000000..aa2b189b6
--- /dev/null
+++ b/test-suite/bugs/closed/4161.v
@@ -0,0 +1,27 @@
+
+    (* Inductive t : Type -> Type := *)
+    (* | Just : forall (A : Type), t A -> t A. *)
+
+    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
+    (*   match x in t A return t (A + unit) with *)
+    (*   | Just T x => @test T x *)
+    (*   end. *)
+
+
+    Definition Type1 := Type.
+Definition Type2 := Type.
+Definition cast (x:Type2) := x:Type1.
+Axiom f: Type2 -> Prop.
+Definition A :=
+ let T := fun A:Type1 => _ in
+ fun A':Type2 =>
+ eq_refl : T A' = f A' :> Prop.
+(* Type2 <= Type1... f A -> Type1 <= Type2 *)
+
+Inductive t : Type -> Type :=
+    | Just : forall (A : Type), t A -> t A.
+
+Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
+  match x in t A with
+  | Just B x => @test B x
+  end.
\ No newline at end of file