Implicitly bind kind variables in type family instance RHSes when it's sensible

Summary:
Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:

```lang=haskell
type T = (Nothing :: Maybe a)
```

However, it would not accept a very similar type family instance:

```lang=haskell
type family   T :: Maybe a
type instance T = (Nothing :: Maybe a)
```

The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing #14131.

In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be //implicitly// bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in #7938 and #9574 to typecheck, whereas before they would
have been rejected.

Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
undergone a minor facelift).

While doing this has the upside of fixing #14131, it also made it easier to
trigger #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #13985, #14131

Differential Revision: https://phabricator.haskell.org/D3872

2 files changed, 84 insertions, 6 deletions

diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst
index 96fbdd4886..db573202e2 100644
--- a/docs/users_guide/8.4.1-notes.rst
+++ b/docs/users_guide/8.4.1-notes.rst
@@ -27,6 +27,24 @@ Language
   wish to; this is quite like how regular datatypes with a kind signature can omit
   some type variables.
 
+- There are now fewer restrictions regarding whether kind variables can appear
+  on the right-hand sides of type and data family instances. Before, there was
+  a strict requirements that all kind variables on the RHS had to be explicitly
+  bound by type patterns on the LHS. Now, kind variables can be *implicitly*
+  bound, which allows constructions like these: ::
+
+    data family Nat :: k -> k -> *
+    -- k is implicitly bound by an invisible kind pattern
+    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+      Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      -- o is implicitly bound by the kind signature
+      -- of the LHS type pattern ('KProxy)
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+
 - Implicitly bidirectional pattern synonyms no longer allow bang patterns
   (``!``) or irrefutable patterns (``~``) on the right-hand side. Previously,
   this was allowed, although the bang patterns and irrefutable patterns would
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index bd11360acc..65f8629ccf 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7659,8 +7659,23 @@ Note the following points:
    instance declarations of the class in which the family was declared,
    just as with the equations of the methods of a class.
 
--  The variables on the right hand side of the type family equation
-   must, as usual, be bound on the left hand side.
+-  The type variables on the right hand side of the type family equation
+   must, as usual, be explicitly bound by 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. For example, these are
+   legitimate: ::
+
+    data family Nat :: k -> k -> *
+    -- k is implicitly bound by an invisible kind pattern
+    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+      Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      -- o is implicitly bound by the kind signature
+      -- of the LHS type pattern ('KProxy)
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
 
 -  The instance for an associated type can be omitted in class
    instances. In that case, unless there is a default instance (see
@@ -7715,15 +7730,18 @@ Note the following points:
 
 -  The default declaration must mention only type *variables* on the
    left hand side, and the right hand side must mention only type
-   variables bound on the left hand side. However, unlike the associated
-   type family declaration itself, the type variables of the default
-   instance are independent of those of the parent class.
+   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.
+
+-  Unlike the associated type family declaration itself, the type variables of
+   the default instance are independent of those of the parent class.
 
 Here are some examples:
 
 ::
 
-      class C a where
+      class C (a :: *) where
         type F1 a :: *
         type instance F1 a = [a]     -- OK
         type instance F1 a = a->a    -- BAD; only one default instance is allowed
@@ -7738,6 +7756,21 @@ Here are some examples:
         type F4 a
         type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
 
+        type F5 a :: [k]
+        type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
+                                            bound by an invisible kind pattern
+                                            on the LHS
+
+        type F6 a
+        type F6 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
+                                            bound by the kind signature of the
+                                            LHS type pattern
+
 .. _scoping-class-params:
 
 Scoping of class parameters
@@ -7760,6 +7793,33 @@ Here, the right-hand side of the data instance mentions the type
 variable ``d`` that does not occur in its left-hand side. We cannot
 admit such data instances as they would compromise type safety.
 
+Bear in mind that it is also possible for the *right*-hand side of an
+associated family instance to contain *kind* parameters (by using the
+:ghc-flag:`-XPolyKinds` extension). For instance, this class and instance are
+perfectly admissible: ::
+
+    class C k where
+      type T :: k
+
+    instance C (Maybe a) where
+      type T = (Nothing :: Maybe a)
+
+Here, although the right-hand side ``(Nothing :: Maybe a)`` mentions a kind
+variable ``a`` which does not occur on the left-hand side, this is acceptable,
+because ``a`` is *implicitly* bound by ``T``'s kind pattern.
+
+A kind variable can also be bound implicitly in a LHS type pattern, as in this
+example: ::
+
+    class C a where
+      type T (x :: a) :: [a]
+
+    instance C (Maybe a) where
+      type T x = ('[] :: [Maybe a])
+
+In ``('[] :: [Maybe a])``, the kind variable ``a`` is implicitly bound by the
+kind signature of the LHS type pattern ``x``.
+
 Instance contexts and associated type and data instances
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~