Merge PR #9314: Enrich implicits for instances

Reviewed-by: SkySkimmer

3 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v
index d2eb61e3e2..b0b573f5d5 100644
--- a/test-suite/bugs/closed/bug_3393.v
+++ b/test-suite/bugs/closed/bug_3393.v
@@ -109,6 +109,7 @@ Global Instance isisomorphism_compose' `{Funext}
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {H C D F' F''} T' {F} T {H0 H1}.
 Section lemmas.
   Context `{Funext}.
   Variable C : PreCategory.
diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v
index 460ae8f110..1305104cdb 100644
--- a/test-suite/bugs/closed/bug_3422.v
+++ b/test-suite/bugs/closed/bug_3422.v
@@ -175,6 +175,7 @@ Global Instance isisomorphism_compose'
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}.
 
 Section lemmas.
   Local Open Scope natural_transformation_scope.
diff --git a/test-suite/bugs/closed/bug_9313.v b/test-suite/bugs/closed/bug_9313.v
new file mode 100644
index 0000000000..0845e7732c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9313.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+Existing Class True.
+
+Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo1 (a := 3) (b := 4).
+
+Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo2 (a := 3) (b := 4).
+
+Instance foo3 (a : nat) {b : nat} (e : a = b) : True.
+exact I.
+Qed.
+Check foo3 (a := 3) (b := 4).