Use HsTyPats in associated type family defaults

Associated type family default declarations behave strangely in a
couple of ways:

1. If one tries to bind the type variables with an explicit `forall`,
   the `forall`'d part will simply be ignored. (#16110)
2. One cannot use visible kind application syntax on the left-hand
   sides of associated default equations, unlike every other form
   of type family equation. (#16356)

Both of these issues have a common solution. Instead of using
`LHsQTyVars` to represent the left-hand side arguments of an
associated default equation, we instead use `HsTyPats`, which is what
other forms of type family equations use. In particular, here are
some highlights of this patch:

* `FamEqn` is no longer parameterized by a `pats` type variable, as
  the `feqn_pats` field is now always `HsTyPats`.
* The new design for `FamEqn` in chronicled in
  `Note [Type family instance declarations in HsSyn]`.
* `TyFamDefltEqn` now becomes the same thing as `TyFamInstEqn`. This
  means that many of `TyFamDefltEqn`'s code paths can now reuse the
  code paths for `TyFamInstEqn`, resulting in substantial
  simplifications to various parts of the code dealing with
  associated type family defaults.

Fixes #16110 and #16356.

2 files changed, 68 insertions, 13 deletions

diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index ca34106eb4..f14271294c 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -54,6 +54,35 @@ Language
   See the `section on explicit kind quantification
   <#explicit-kind-quantification>`__ for more details.
 
+- Type variables in associated type family default declarations can now be
+  explicitly bound with a ``forall`` when :extension:`ExplicitForAll` is
+  enabled, as in the following example: ::
+
+    class C a where
+      type T a b
+      type forall a b. T a b = Either a b
+
+  This has a couple of knock-on consequences:
+
+  - Wildcard patterns are now permitted on the left-hand sides of default
+    declarations, whereas they were rejected by previous versions of GHC.
+
+  - It used to be the case that default declarations supported occurrences of
+    left-hand side arguments with higher-rank kinds, such as in the following
+    example: ::
+
+      class C a where
+        type T a (f :: forall k. k -> Type)
+        type T a (f :: forall k. k -> Type) = f Int
+
+    This will no longer work unless ``f`` is explicitly quantified with a
+    ``forall``, like so: ::
+
+      class C a where
+        type T a (f :: forall k. k -> Type)
+        type forall a (f :: forall k. k -> Type).
+             T a f = f Int
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index bce2bf8370..b1baa308c5 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -8166,14 +8166,15 @@ Note the following points:
 -  A default declaration is not permitted for an associated *data* type.
 
 -  The default declaration must mention only type *variables* on the
-   left hand side, and the right hand side must mention only type
+   left hand side, and type variables may not be repeated on the left-hand
+   side. The right hand side must mention only type
    variables that are explicitly bound on the left hand side. This restriction
    is relaxed for *kind* variables, however, as the right hand side is allowed
    to mention kind variables that are implicitly bound on the left hand side.
 
-   Because of this, unlike :ref:`assoc-inst`, explicit binding of type/kind
-   variables in default declarations is not permitted by
-   :extension:`ExplicitForAll`.
+   Like with :ref:`assoc-inst`, it is possible to explicitly bind type and kind
+   variables in default declarations with a ``forall`` by using the
+   :extension:`ExplicitForAll` language extension.
 
 -  Unlike the associated type family declaration itself, the type variables of
    the default instance are independent of those of the parent class.
@@ -8192,26 +8193,51 @@ Here are some examples:
         type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the type instance
 
         type F3 a
-        type F3 [b] = b              -- BAD; only type variables allowed on the LHS
+        type F3 [b] = b              -- BAD; only type variables allowed on the
+                                             LHS, and the argument to F3 is
+                                             instantiated to [b], which is not
+                                             a bare type variable
 
-        type F4 a
-        type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
+        type F4 x y
+        type F4 x x = x              -- BAD; the type variable x is repeated on
+                                             the LHS
 
-        type F5 a :: [k]
-        type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
+        type F5 a
+        type F5 b = a                -- BAD; 'a' is not in scope  in the RHS
+
+        type F6 a :: [k]
+        type F6 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
                                             bound by an invisible kind pattern
                                             on the LHS
 
-        type F6 a
-        type F6 a =
+        type F7 a
+        type F7 a =
           Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
                                              even by an invisible kind pattern
 
-        type F7 (x :: a) :: [a]
-        type F7 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
+        type F8 (x :: a) :: [a]
+        type F8 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
                                             bound by the kind signature of the
                                             LHS type pattern
 
+        type F9 (a :: k)
+        type F9 a = Maybe a          -- BAD; the kind variable k is
+                                             instantiated to Type, which is not
+                                             a bare kind variable
+
+        type F10 (a :: j) (b :: k)
+        type F10 (a :: z) (b :: z)
+          = Proxy a                  -- BAD; the kind variable z is repeated,
+                                     -- as both j and k are instantiated to z
+
+        type F11 a b
+        type forall a b. F11 a b = a -- OK; LHS type variables can be
+                                        explicitly bound with 'forall'
+
+        type F12 (a :: k)
+        type F12 @k a = Proxy a      -- OK; visible kind application syntax is
+                                            permitted in default declarations
+
 .. _scoping-class-params:
 
 Scoping of class parameters