[Typeclasses] Warn when RHS of `:>` is not a class

This introduces the warning “not-a-class” in the “typeclasses” category.

4 files changed, 51 insertions, 11 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 15a55d9e72..882798205b 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -260,6 +260,12 @@ preorder can be used instead. This is very similar to the coercion
 mechanism of ``Structure`` declarations. The implementation simply
 declares each projection as an instance.
 
+.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class
+
+   Using this ``:>`` syntax with a right-hand-side that is not itself a Class
+   has no effect (apart from emitting this warning). In particular, is does not
+   declare a coercion.
+
 One can also declare existing objects or structure projections using
 the Existing Instance command to achieve the same effect.
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4aea2c3db9..65677a0da6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -434,28 +434,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.
diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v
new file mode 100644
index 0000000000..c1fdd04a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9014.v
@@ -0,0 +1,19 @@
+(* A type, not a class *)
+Variant T := mkT.
+
+(* In records, :> declares a coercion *)
+Record R := { t_of_r :> T }.
+Check forall r : R, r = r :> T.
+
+(* A class *)
+Class A := { p : Prop }.
+(* A sub-class *)
+Class B := { a_of_b :> A ; t_of_b :> T }.
+(* The sub-instance is automatically inferred due to :> for a_of_b *)
+Check forall b : B, p.
+(* No coercion is introduced by :> in t_of_b *)
+Fail Check forall b : B, b = b :> T.
+
+(* Using :> when the RHS is not a class produces a “not-a-class” warning. *)
+Set Warnings "+not-a-class".
+Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }.