Properly expand projection parameters in Btermdn.

The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.

We fix this by adding dummy parameter arguments on sight.

Fixes #14009: TC search failure with primitive projections.

4 files changed, 50 insertions, 4 deletions

diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst
new file mode 100644
index 0000000000..3b58e193cb
--- /dev/null
+++ b/doc/changelog/04-tactics/14033-fix-14009.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Properly expand projection parameters in hint discrimination
+  nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_,
+  fixes `#9000 <https://github.com/coq/coq/issues/9000>`_,
+  `#14009 <https://github.com/coq/coq/issues/14009>`_,
+  by Pierre-Marie Pédrot).
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index af0ca22868..794d2bb94f 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -32,18 +32,25 @@ let compare_term_label t1 t2 = match t1, t2 with
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 
-let decomp_pat =
+let decomp_pat p =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc)
+    | PProj (p, c) ->
+      let hole = PMeta None in
+      let params = List.make (Projection.npars p) hole in
+      (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc)
     | c -> (c,acc)
   in
-  decrec []
+  decrec [] p
 
 let decomp sigma t =
   let rec decrec acc c = match EConstr.kind sigma c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
+    | Proj (p, c) ->
+      (* Hack: fake evar to generate [Everything] in the functions below *)
+      let hole = mkEvar (Evar.unsafe_of_int (-1), []) in
+      let params = List.make (Projection.npars p) hole in
+      (mkConst (Projection.constant p), params @ c :: acc)
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in
diff --git a/test-suite/bugs/closed/bug_14009.v b/test-suite/bugs/closed/bug_14009.v
new file mode 100644
index 0000000000..bf86f5117e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14009.v
@@ -0,0 +1,16 @@
+Class Bin {P:Type} (A B : P) := {}.
+
+Set Primitive Projections.
+
+Record test (n : nat) := { proj : Prop }.
+Axiom Bin_test : forall {t1 t2 : test O}, Bin (proj _ t1) (proj _ t2).
+
+Create HintDb db discriminated.
+#[local] Hint Resolve Bin_test : db.
+#[local] Hint Opaque proj : db.
+
+Goal forall t1 t2 : test O, Bin (proj O t1) (proj O t2).
+Proof.
+intros.
+solve [typeclasses eauto with db].
+Qed.
diff --git a/test-suite/bugs/closed/bug_9000.v b/test-suite/bugs/closed/bug_9000.v
new file mode 100644
index 0000000000..e239c8b1fe
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9000.v
@@ -0,0 +1,17 @@
+Set Primitive Projections.
+Class type (t : Type) : Type :=
+  { bar : t -> Prop  }.
+
+Instance type_nat : type nat :=
+  { bar := fun _ => True }.
+
+Definition foo_bar {n : nat} : bar n := I.
+
+#[local] Hint Resolve (@foo_bar) : typeclass_instances.
+#[local] Hint Resolve I : typeclass_instances.
+Check ltac:(typeclasses eauto with nocore typeclass_instances) : True.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
+Existing Class bar.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
+#[local] Hint Resolve (@foo_bar) : foo.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.