1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_045.v b/test-suite/bugs/closed/HoTT_coq_045.v
new file mode 100644
index 00000000..00588ffb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_045.v
@@ -0,0 +1,53 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj
+  }.
+
+Record > Category :=
+  {
+    CObject : Type;
+    UnderlyingCategory :> @SpecializedCategory CObject
+  }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  {
+    ObjectOf :> objC -> objD
+  }.
+
+Definition Functor (C D : Category) := SpecializedFunctor C D.
+
+Parameter TerminalCategory : SpecializedCategory unit.
+
+Definition focus A (_ : A) := True.
+
+Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
+  assert (Hf : focus ((S tt) = (S tt))) by constructor.
+  let C1 := constr:(CObject) in
+  let C2 := constr:(fun C => @Object (CObject C) C) in
+  unify C1 C2.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  simpl in *.
+  let V := match type of Hf with
+             | focus ?V => constr:(V)
+           end
+  in exact V.
+(* Toplevel input, characters 89-96:
+Error: Illegal application:
+The term "ObjectOf" of type
+ "forall (objC : Set) (C : SpecializedCategory objC)
+    (objD : Type) (D : SpecializedCategory objD),
+  SpecializedFunctor C D -> objC -> objD"
+cannot be applied to the terms
+ "Object TerminalCategory" : "Type"
+ "TerminalCategory" : "SpecializedCategory unit"
+ "Object A" : "Type"
+ "UnderlyingCategory A" : "SpecializedCategory (CObject A)"
+ "S" : "Functor TerminalCategory A"
+ "tt" : "unit"
+The 1st term has type "Type" which should be coercible to
+"Set". *)
+Defined.