From f2c08124b30eb87482dc0ed1d7199aa58950e309 Mon Sep 17 00:00:00 2001
From: Bodigrim <andrew.lelechenko@gmail.com>
Date: Fri, 22 Apr 2022 19:03:04 +0100
Subject: [PATCH] Document behaviour of RULES with KnownNat

---
 docs/users_guide/exts/rewrite_rules.rst | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs/users_guide/exts/rewrite_rules.rst b/docs/users_guide/exts/rewrite_rules.rst
index 7ac93bb21df9..75ee2474a984 100644
--- a/docs/users_guide/exts/rewrite_rules.rst
+++ b/docs/users_guide/exts/rewrite_rules.rst
@@ -228,6 +228,15 @@ From a semantic point of view:
 
    because ``y`` can match against ``0``.
 
+-  A rule that has a forall binder with a polymorphic type, is likely to fail to fire. E. g., ::
+
+        {-# RULES forall (x :: forall a. Num a => a -> a).  f x = blah #-}
+
+   Here ``x`` has a polymorphic type.  This applies to a forall'd binder with a type class constraint, such as::
+
+        {-# RULES forall @m (x :: KnownNat m => Proxy m).  g x = blah #-}
+
+   See `#21093 <https://gitlab.haskell.org/ghc/ghc/-/issues/21093>`_ for discussion.
 
 .. _rules-inline:
 
-- 
GitLab