1 files changed, 36 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3331.v b/test-suite/bugs/opened/3331.v
new file mode 100644
index 0000000000..07504aed7c
--- /dev/null
+++ b/test-suite/bugs/opened/3331.v
@@ -0,0 +1,36 @@
+(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *)
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (x = y :>_) : type_scope.
+Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }.
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y) := H x y.
+Notation Contr := (IsTrunc minus_two).
+Section groupoid_category.
+  Variable X : Type.
+  Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}.
+  Goal X -> True.
+    intro d.
+    pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *)
+    clear H'.
+    compute in H.
+    change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H.
+    assert (H' := H).
+    pose proof (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as X0. (* success *)
+    clear H' X0.
+    Fail pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* Toplevel input, characters 21-22:
+Error:
+Cannot infer this placeholder.
+Could not find an instance for "Contr (idpath = idpath)" in environment:
+
+X : Type
+H : forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)
+d : X *)