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

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

3 files changed, 33 insertions, 1 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 26573b9185..08519eb1fb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -130,6 +130,9 @@ Vernacular commands
   for all commands that support it. In particular, it does not have any effect
   on tactics anymore. May cause some incompatibilities.
 
+- The algorithm computing implicit arguments now behaves uniformly for primitive
+  projection and application nodes (bug #9508).
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 959455dfd2..7e8f2f4f3d 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -200,7 +200,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
           iter_with_full_binders sigma push_lift (frec false) ed c
-    | Proj (p,c) when rig ->
+    | Proj (p, _) when rig ->
       if strict then () else
         iter_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
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.