aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMatthieu Sozeau2018-11-28 17:10:02 +0100
committerMatthieu Sozeau2018-11-28 17:10:02 +0100
commit320f8c4503293b37c852548e4d19ff4dd1c191cb (patch)
tree9d306d01b8ef00d8b87615259ea09fa82b568ad8 /doc
parent2e68697327f6f8a7f365ba3474a3f1a04ca4a621 (diff)
parent23fcb09d934bf77fe58f232d2c246a81fc76591f (diff)
Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/addendum/type-classes.rst6
1 files changed, 6 insertions, 0 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.