From 592e41131613e198560de3c88158eadcd789b317 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anselm=20Sch=C3=BCler?= <mail@anselmschueler.com>
Date: Sat, 15 Jan 2022 14:22:44 +0100
Subject: [PATCH] =?UTF-8?q?Note=20that=20ImpredicativeTypes=20doesn?=
 =?UTF-8?q?=E2=80=99t=20allow=20polymorphic=20instances?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

See #20939
---
 docs/users_guide/exts/impredicative_types.rst | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs/users_guide/exts/impredicative_types.rst b/docs/users_guide/exts/impredicative_types.rst
index 63017b8a2e25..109ca28ea0e4 100644
--- a/docs/users_guide/exts/impredicative_types.rst
+++ b/docs/users_guide/exts/impredicative_types.rst
@@ -50,6 +50,15 @@ Switching on :extension:`ImpredicativeTypes`
   functions in many cases. For example, ``reverse xs`` will typecheck even if ``xs :: [forall a. a->a]``,
   by instantiating ``reverse`` at type ``forall a. a->a``.
 
+Note that the treatment of type-class constraints and implicit parameters remains entirely monomorphic,
+even with ImpredicativeTypes. Specifically:
+
+- You cannot apply a type class to a polymorphic type. This is illegal: ``f :: C (forall a. a->a) => [a] -> [a]``
+
+- You cannot give an instance declaration with a polymorphic argument. This is illegal: ``instance C (forall a. a->a)``
+
+- An implicit parameter cannot have a polymorphic type: ``g :: (?x :: forall a. a->a) => [a] -> [a]``
+
 For many years GHC has a special case for the function ``($)``, that allows it
 to typecheck an application like ``runST $ (do { ... })``, even though that
 instantiation may be impredicative.  This special case remains: even without
-- 
GitLab