From 23fcb09d934bf77fe58f232d2c246a81fc76591f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 16 Nov 2018 13:24:54 +0000
Subject: [Typeclasses] Warn when RHS of `:>` is not a class

This introduces the warning “not-a-class” in the “typeclasses” category.
---
 test-suite/bugs/closed/bug_9014.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9014.v

(limited to 'test-suite')

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 }.
-- 
cgit v1.2.3