1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_067.v b/test-suite/bugs/closed/HoTT_coq_067.v
new file mode 100644
index 00000000..ad32a60c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_067.v
@@ -0,0 +1,28 @@
+Set Universe Polymorphism.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Goal forall (A : Type) (P : forall _ : A, Type) (x0 : A)
+     (p : P x0) (q : @paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p)),
+   @paths (@paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p))
+     (@idpath (@sigT A P) (@existT A P x0 p))
+     (@idpath (@sigT A P) (@existT A P x0 p)).
+  intros.
+  induction q.
+  admit.
+Qed.
+(** Error: Illegal application:
+The term "paths_rect" of type
+ "forall (A : Type) (a : A) (P : forall a0 : A, paths a a0 -> Type),
+  P a (idpath a) -> forall (y : A) (p : paths a y), P y p"
+cannot be applied to the terms
+ "{x : _ & P x}" : "Type"
+ "s" : "{x : _ & P x}"
+ "fun (a : {x : _ & P x}) (_ : paths s a) => paths (idpath a) (idpath a)"
+   : "forall a : {x : _ & P x}, paths s a -> Type"
+ "match proof_admitted return (paths (idpath s) (idpath s)) with
+  end" : "paths (idpath s) (idpath s)"
+ "s" : "{x : _ & P x}"
+ "q" : "paths (existT P x0 p) (existT P x0 p)"
+The 3rd term has type "forall a : {x : _ & P x}, paths s a -> Type"
+which should be coercible to "forall a : {x : _ & P x}, paths s a -> Type". *)