Reject nested foralls/contexts in instance types more consistently

GHC is very wishy-washy about rejecting instance declarations with
nested `forall`s or contexts that are surrounded by outermost
parentheses. This can even lead to some strange interactions with
`ScopedTypeVariables`, as demonstrated in #18240. This patch makes
GHC more consistently reject instance types with nested
`forall`s/contexts so as to prevent these strange interactions.

On the implementation side, this patch tweaks `splitLHsInstDeclTy`
and `getLHsInstDeclHead` to not look through parentheses, which can
be semantically significant. I've added a
`Note [No nested foralls or contexts in instance types]` in
`GHC.Hs.Type` to explain why. This also introduces a
`no_nested_foralls_contexts_err` function in `GHC.Rename.HsType` to
catch nested `forall`s/contexts in instance types. This function is
now used in `rnClsInstDecl` (for ordinary instance declarations) and
`rnSrcDerivDecl` (for standalone `deriving` declarations), the latter
of which fixes #18271.

On the documentation side, this adds a new
"Formal syntax for instance declaration types" section to the GHC
User's Guide that presents a BNF-style grammar for what is and isn't
allowed in instance types.

Fixes #18240. Fixes #18271.

4 files changed, 132 insertions, 7 deletions

diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index deb29310ff..aa602b4f7c 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -150,6 +150,22 @@ Language
     data U a where
       MkU :: (Show a => U a)
 
+* GHC more strictly enforces the rule that the type in the top of an instance
+  declaration is not permitted to contain nested ``forall``\ s or contexts, as
+  documented in :ref:`formal-instance-syntax`. For example, the following
+  examples, which previous versions of GHC would accept, are now rejected:
+
+    instance (forall a. C a) where ...
+    instance (Show a => C a) where ...
+
+  In addition, GHC now enforces the rule that the types in ``deriving`` clauses
+  and ``via`` types (for instances derived with :extension:`DerivingVia`)
+  cannot contain nested ``forall``\ s or contexts. For example, the following
+  examples, which previous versions of GHC would accept, are now rejected: ::
+
+    data T = MkT deriving (C1, (forall x. C2 x))
+    deriving via (forall x. V x) instance C (S x)
+
 * A new language extension :extension:`QualifiedDo` is implemented, allowing
   to qualify a do block to control which operations to use for desugaring do
   syntax. ::
diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 372861d2a7..50938e98d0 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/docs/users_guide/exts/explicit_forall.rst
@@ -37,6 +37,11 @@ Notes:
 
       instance forall a. Eq a => Eq [a] where ...
 
+  Note that the use of ``forall``s in instance declarations is somewhat
+  restricted in comparison to other types. For example, instance declarations
+  are not allowed to contain nested ``forall``s. See
+  :ref:`formal-instance-syntax` for more information.
+
 - If the :ghc-flag:`-Wunused-foralls` flag is enabled, a warning will be emitted
   when you write a type variable in an explicit ``forall`` statement that is
   otherwise unused. For instance: ::
diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst
index 3dd7969d97..14b2e39a27 100644
--- a/docs/users_guide/exts/instances.rst
+++ b/docs/users_guide/exts/instances.rst
@@ -99,6 +99,77 @@ GHC relaxes this rule in two ways:
 However, the instance declaration must still conform to the rules for
 instance termination: see :ref:`instance-termination`.
 
+.. _formal-instance-syntax:
+
+Formal syntax for instance declaration types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The top of an instance declaration only permits very specific forms of types.
+To make more precise what forms of types are or are not permitted, we provide a
+BNF-style grammar for the tops of instance declarations below: ::
+
+  inst_top ::= 'instance' opt_forall opt_ctxt inst_head opt_where
+
+  opt_forall ::= <empty>
+              |  'forall' tv_bndrs '.'
+
+  tv_bndrs ::= <empty>
+            |  tv_bndr tv_bndrs
+
+  tv_bndr ::= tyvar
+           |  '(' tyvar '::' ctype ')'
+
+  opt_ctxt ::= <empty>
+            |  btype '=>'
+            |  '(' ctxt ')' '=>'
+
+  ctxt ::= ctype
+        |  ctype ',' ctxt
+
+  inst_head ::= '(' inst_head ')'
+             |  prefix_cls_tycon arg_types
+             |  arg_type infix_cls_tycon arg_type
+             |  '(' arg_type infix_cls_tycon arg_type ')' arg_types
+
+  arg_type ::= <empty>
+            |  arg_type arg_types
+
+  opt_where ::= <empty>
+             |  'where'
+
+Where:
+
+- ``btype`` is a type that is not allowed to have an outermost
+  ``forall``/``=>`` unless it is surrounded by parentheses. For example,
+  ``forall a. a`` and ``Eq a => a`` are not legal ``btype``s, but
+  ``(forall a. a)`` and ``(Eq a => a)`` are legal.
+- ``ctype`` is a ``btype`` that has no restrictions on an outermost
+  ``forall``/``=>``, so ``forall a. a`` and ``Eq a => a`` are legal ``ctype``s.
+- ``arg_type`` is a type that is not allowed to have ``forall``s or ``=>``s
+- ``prefix_cls_tycon`` is a class type constructor written prefix (e.g.,
+  ``Show`` or ``(&&&)``), while ``infix_cls_tycon`` is a class type constructor
+  written infix (e.g., ```Show``` or ``&&&``).
+
+This is a simplified grammar that does not fully delve into all of the
+implementation details of GHC's parser (such as the placement of Haddock
+comments), but it is sufficient to attain an understanding of what is
+syntactically allowed. Some further various observations about this grammar:
+
+- Instance declarations are not allowed to be declared with nested ``forall``s
+  or ``=>``s. For example, this would be rejected: ::
+
+    instance forall a. forall b. C (Either a b) where ...
+
+  As a result, ``inst_top`` puts all of its quantification and constraints up
+  front with ``opt_forall`` and ``opt_context``.
+- Furthermore, instance declarations types do not permit outermost parentheses
+  that surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
+  used. For example, ``instance (forall a. C a)`` would be rejected, since GHC
+  would treat the ``forall`` as being nested.
+
+  Note that it is acceptable to use parentheses in a ``inst_head``. For
+  instance, ``instance (C a)`` is accepted, as is ``instance forall a. (C a)``.
+
 .. _instance-rules:
 
 Relaxed rules for instance contexts
diff --git a/docs/users_guide/exts/scoped_type_variables.rst b/docs/users_guide/exts/scoped_type_variables.rst
index 002686ffd6..d80eb40d0d 100644
--- a/docs/users_guide/exts/scoped_type_variables.rst
+++ b/docs/users_guide/exts/scoped_type_variables.rst
@@ -16,11 +16,11 @@ Lexically scoped type variables
 
 .. tip::
 
-    ``ScopedTypeVariables`` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
+    :extension:`ScopedTypeVariables` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
     For the :ref:`decl-type-sigs` (or :ref:`exp-type-sigs`) examples in this section,
     the explicit ``forall`` is required.
     (If omitted, usually the program will not compile; in a few cases it will compile but the functions get a different signature.)
-    To trigger those forms of ``ScopedTypeVariables``, the ``forall`` must appear against the top-level signature (or outer expression)
+    To trigger those forms of :extension:`ScopedTypeVariables`, the ``forall`` must appear against the top-level signature (or outer expression)
     but *not* against nested signatures referring to the same type variables.
 
     Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :ref:`pattern-type-sigs`.
@@ -261,11 +261,12 @@ the pattern, rather than the pattern binding the variable.
 Class and instance declarations
 -------------------------------
 
-The type variables in the head of a ``class`` or ``instance``
-declaration scope over the methods defined in the ``where`` part. You do
-not even need an explicit ``forall`` (although you are allowed an explicit
-``forall`` in an ``instance`` declaration; see :ref:`explicit-foralls`).
-For example: ::
+:extension:`ScopedTypeVariables` allow the type variables bound by the top of a
+``class`` or ``instance`` declaration to scope over the methods defined in the
+``where`` part. Unlike :ref`decl-type-sigs`, type variables from class and
+instance declarations can be lexically scoped without an explicit ``forall``
+(although you are allowed an explicit ``forall`` in an ``instance``
+declaration; see :ref:`explicit-foralls`). For example: ::
 
       class C a where
         op :: [a] -> a
@@ -278,4 +279,36 @@ For example: ::
       instance C b => C [b] where
         op xs = reverse (head (xs :: [[b]]))
 
+      -- Alternatively, one could write the instance above as:
+      instance forall b. C b => C [b] where
+        op xs = reverse (head (xs :: [[b]]))
+
+While :extension:`ScopedTypeVariables` is required for type variables from the
+top of a class or instance declaration to scope over the /bodies/ of the
+methods, it is not required for the type variables to scope over the /type
+signatures/ of the methods. For example, the following will be accepted without
+explicitly enabling :extension:`ScopedTypeVariables`: ::
+
+      class D a where
+        m :: [a] -> a
+
+      instance D [a] where
+        m :: [a] -> [a]
+        m = reverse
+
+Note that writing ``m :: [a] -> [a]`` requires the use of the
+:extension:`InstanceSigs` extension.
+
+Similarly, :extension:`ScopedTypeVariables` is not required for type variables
+from the top of the class or instance declaration to scope over associated type
+families, which only requires the :extension:`TypeFamilies` extension. For
+instance, the following will be accepted without explicitly enabling
+:extension:`ScopedTypeVariables`: ::
+
+      class E a where
+        type T a
+
+      instance E [a] where
+        type T [a] = a
 
+See :ref:`scoping-class-params` for further information.