Imported Upstream version 8.5~beta1+dfsg

1 files changed, 61 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_068.v b/test-suite/bugs/closed/HoTT_coq_068.v
new file mode 100644
index 00000000..f1cdcbf2
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_068.v
@@ -0,0 +1,61 @@
+Generalizable All Variables.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Module success.
+  Axiom bar : nat -> Type -> Type.
+
+  Definition foo (n : nat) (A : Type) : Type :=
+    match n with
+      | O => A
+      | S n' => forall x y : A, bar n' (x = y)
+    end.
+
+  Definition foo_succ n A : foo (S n) A.
+  Admitted.
+
+  Goal forall n (X Y : Type) (y : X) (x : X), bar n (x = y).
+  intros.
+  apply (foo_succ _ _).
+  Defined.
+End success.
+
+Module failure.
+  Fixpoint bar (n : nat) (A : Type) : Type :=
+    match n with
+      | O => A
+      | S n' => forall x y : A, bar n' (x = y)
+    end.
+
+  Definition foo_succ n A : bar (S n) A.
+  Admitted.
+
+  Goal forall n (X Y : Type) (y : X) (x : X), bar n (x = y).
+  intros.
+  apply foo_succ.
+  (* Toplevel input, characters 22-34:
+Error: In environment
+n : nat
+X : Type
+Y : Type
+y : X
+x : X
+Unable to unify
+ "forall x0 y0 : ?16,
+  (fix bar (n : nat) (A : Type) {struct n} : Type :=
+     match n with
+     | 0 => A
+     | S n' => forall x y : A, bar n' (x = y)
+     end) ?15 (x0 = y0)" with
+ "(fix bar (n : nat) (A : Type) {struct n} : Type :=
+     match n with
+     | 0 => A
+     | S n' => forall x y : A, bar n' (x = y)
+     end) n (x = y)".
+*)
+  Defined.
+End failure.