Imported Upstream version 8.5~beta1+dfsg

1 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
new file mode 100644
index 00000000..ba69f6b1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -0,0 +1,33 @@
+Set Implicit Arguments.
+
+Generalizable All Variables.
+
+Parameter SpecializedCategory : Type -> Type.
+Parameter Object : forall obj, SpecializedCategory obj -> Type.
+
+Section SpecializedFunctor.
+  (* Variable objC : Type. *)
+  Context `(C : SpecializedCategory objC).
+
+  Polymorphic Record SpecializedFunctor := {
+    ObjectOf' : objC -> Type;
+    ObjectC : Object C
+  }.
+End SpecializedFunctor.
+
+Section FunctorInterface.
+  Variable objC : Type.
+  Variable C : SpecializedCategory objC.
+  Variable F : SpecializedFunctor C.
+
+  Set Printing All.
+  Set Printing Universes.
+  Check @ObjectOf' objC C F. (* Toplevel input, characters 24-25:
+Error:
+In environment
+objC : Type (* Top.515 *)
+C : SpecializedCategory objC
+F : @SpecializedFunctor (* Top.516 *) objC C
+The term "F" has type "@SpecializedFunctor (* Top.516 *) objC C"
+ while it is expected to have type
+ "@SpecializedFunctor (* Top.519 Top.520 *) objC C". *)