Merge PR #9307: Handle local definitions in implicit arguments of Instance

3 files changed, 12 insertions, 3 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 6789bc038e..ae67eb5d1b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -93,6 +93,9 @@ Vernacular commands
 - The naming scheme for anonymous binders in a `Theorem` has changed to
   avoid conflicts with explicitly named binders.
 
+- Computation of implicit arguments now properly handles local definitions in the
+  binders for an `Instance`.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v
new file mode 100644
index 0000000000..a80f3233a3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9300.v
@@ -0,0 +1,6 @@
+Existing Class True.
+
+Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined.
+
+Fail Check foo (n := 3) true (s := (4 , 5)).
+Check foo (n := 3) (b := true) (4 , 5).
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 370df615fc..a342f5bf98 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -301,10 +301,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
     else tclass
   in
-  let sigma, k, u, cty, ctx', ctx, len, imps, subst =
+  let sigma, k, u, cty, ctx', ctx, imps, subst =
     let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
     let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
-    let len = List.length ctx in
+    let len = Context.Rel.nhyps ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum sigma c' in
     let ctx'' = ctx' @ ctx in
@@ -320,7 +320,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
         | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
         cl_context (args, [])
     in
-      sigma, cl, u, c', ctx', ctx, len, imps, args
+      sigma, cl, u, c', ctx', ctx, imps, args
   in
   let id =
     match instid with