Fix #9508: Unexpected interaction between implicit arguments and primitive projections.

This was due to an involuntary capture of a variable name.

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9508.v b/test-suite/bugs/closed/bug_9508.v
new file mode 100644
index 0000000000..2c38e24add
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9508.v
@@ -0,0 +1,29 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Module OK.
+Record A := mkA {
+  T : Type;
+  P : T -> bool;
+}.
+
+About P. (* Argument a is implicit *)
+Check P (true: T (mkA negb)).
+End OK.
+
+Module KO.
+Set Primitive Projections.
+Record A := mkA {
+  T : Type;
+  P : T -> bool;
+}.
+
+About P. (* No implicit arguments *)
+Check P (true: T (mkA negb)).
+(*
+The command has indeed failed with message:
+The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}"
+while it is expected to have type "A".
+*)
+
+End KO.