Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class

2 files changed, 26 insertions, 11 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 18c9650bd1..d732544c5c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -427,28 +427,40 @@ let remove_instance i =
   Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
   remove_instance_hint i.is_impl
 
-let declare_instance info local glob =
+let warning_not_a_class =
+  let name = "not-a-class" in
+  let category = "typeclasses" in
+  CWarnings.create ~name ~category (fun (n, ty) ->
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      Pp.(str "Ignored instance declaration for “"
+          ++ Nametab.pr_global_env Id.Set.empty n
+          ++ str "”: “"
+          ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
+          ++ str "” is not a class")
+    )
+
+let declare_instance ?(warn = false) info local glob =
   let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
       assert (not (isVarRef glob) || local);
       add_instance (new_instance tc info (not local) glob)
-    | None -> ()
+    | None -> if warn then warning_not_a_class (glob, ty)
 
 let add_class cl =
   add_class cl;
   List.iter (fun (n, inst, body) ->
-	     match inst with
-	     | Some (Backward, info) ->
-	       (match body with
-	       | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
-	       | Some b -> declare_instance (Some info) false (ConstRef b))
-	     | _ -> ())
-  cl.cl_projs
+      match inst with
+      | Some (Backward, info) ->
+        (match body with
+         | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
+         | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b))
+      | _ -> ())
+    cl.cl_projs
 
 
-      
 (*
  * interface functions
  *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8bdac0a575..d00195678b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
+(** Declares the given global reference as an instance of its type.
+    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
+    when said type is not a registered type class. *)
+val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.