Fix #10176: shadowing vs automatic class based generalization

4 files changed, 17 insertions, 2 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f71ad14dd4..851109876b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -221,8 +221,10 @@ let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
-      let gr = Nametab.locate qid in
-      if Typeclasses.is_class gr then Some (clapp, gr) else None
+      if Libnames.idset_mem_qualid qid env then None
+      else
+        let gr = Nametab.locate qid in
+        if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
   match is_class with
diff --git a/library/libnames.ml b/library/libnames.ml
index 87c4de42e8..41b38e0378 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,6 +162,9 @@ let qualid_basename qid =
 let qualid_path qid =
   qid.CAst.v.dirpath
 
+let idset_mem_qualid qid s =
+  qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s
+
 (* Default paths *)
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index bbb4d2a058..7d77d95991 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool
 val qualid_path : qualid -> DirPath.t
 val qualid_basename : qualid -> Id.t
 
+val idset_mem_qualid : qualid -> Id.Set.t -> bool
+(** false when the qualid is not an ident *)
+
 (** {6 ... } *)
 
 (** some preset paths *)
diff --git a/test-suite/bugs/closed/bug_10176.v b/test-suite/bugs/closed/bug_10176.v
new file mode 100644
index 0000000000..fdb0eb87a4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10176.v
@@ -0,0 +1,7 @@
+Class Foo (xxx:nat) := foo : nat.
+
+Lemma aa `{Foo} : nat. Abort.
+
+Fail Lemma xy (Foo:bool->Type) `{Foo} : nat.
+
+Fail Lemma yx (Fooo:bool->Type) `{Fooo} : nat.