1 files changed, 63 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
new file mode 100644
index 00000000..ca4d2380
--- /dev/null
+++ b/test-suite/bugs/closed/3454.v
@@ -0,0 +1,63 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+
+Record prod {A} {B}:= pair { fst : A ; snd : B }.
+Notation " A * B " := (@prod A B) : type_scope.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Notation pr1 := (@projT1 _ _).
+Arguments prod : clear implicits.
+
+Check (@projT1 _ (fun x : nat => x = x)).
+Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
+
+Record rimpl {b : bool} {n : nat} := { foo : forall {x : nat}, x = n }. 
+
+Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
+Check (fun r : @rimpl true 0 => @foo true 0 r 0).
+Check (fun r : @rimpl true 0 => foo r (x:=0)).
+Check (fun r : @rimpl true 0 => @foo _ _ r 0).
+Check (fun r : @rimpl true 0 => r.(@foo _ _)).
+Check (fun r : @rimpl true 0 => r.(foo)).
+
+Notation "{ x : T  & P }" := (@sigT T P).
+Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+(* Notation "{ x : T * U  & P }" := (@sigT (T * U) P). *)
+
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+
+Local Instance isequiv_tgt_compose A B
+: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
+           (A -> B)
+           (@compose A {xy : B * B & fst xy = snd xy} B
+                     (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
+(* Toplevel input, characters 220-223: *)
+(* Error: Cannot infer this placeholder. *)
+
+Local Instance isequiv_tgt_compose' A B
+: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
+           (A -> B)
+           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
+(* Toplevel input, characters 221-232: *)
+(* Error: *)
+(* In environment *)
+(* A : Type *)
+(* B : Type *)
+(* The term "pr1" has type "sigT ?30 -> ?29" while it is expected to have type *)
+(*  "{xy : B * B & fst xy = snd xy} -> ?27 * B". *)
+
+Local Instance isequiv_tgt_compose'' A B
+: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
+           (A -> B)
+           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) 
+                                                                  (fun s => s.(projT1)))).
+(* Toplevel input, characters 15-241:
+Error:
+Cannot infer an internal placeholder of type "Type" in environment:
+
+A : Type
+B : Type
+x : ?32
+. *)