Reject dodgy scoping in associated family instance RHSes

Commit e63518f5d6a93be111f9108c0990a1162f88d615 tried to push all of the logic
of detecting out-of-scope type variables on the RHSes of associated type family
instances to `GHC.Tc.Validity` by deleting a similar check in the renamer.
Unfortunately, this commit went a little too far, as there are some corner
cases that `GHC.Tc.Validity` doesn't detect. Consider this example:

```hs
class C a where
  data D a

instance forall a. C Int where
  data instance D Int = MkD a
```

If this program isn't rejected by the time it reaches the typechecker, then
GHC will believe the `a` in `MkD a` is existentially quantified and accept it.
This is almost surely not what the user wants! The simplest way to reject
programs like this is to restore the old validity check in the renamer
(search for `improperly_scoped` in `rnFamEqn`).

Note that this is technically a breaking change, since the program in the
`polykinds/T9574` test case (which previously compiled) will now be rejected:

```hs
instance Funct ('KProxy :: KProxy o) where
    type Codomain 'KProxy = NatTr (Proxy :: o -> *)
```

This is because the `o` on the RHS will now be rejected for being out of scope.
Luckily, this is simple to repair:

```hs
instance Funct ('KProxy :: KProxy o) where
    type Codomain ('KProxy @o) = NatTr (Proxy :: o -> *)
```

All of the discussion is now a part of the revamped
`Note [Renaming associated types]` in `GHC.Rename.Module`.

A different design would be to make associated type family instances have
completely separate scoping from the parent instance declaration, much like
how associated type family default declarations work today. See the discussion
beginning at https://gitlab.haskell.org/ghc/ghc/-/issues/18021#note_265729 for
more on this point. This, however, would break even more programs that are
accepted today and likely warrants a GHC proposal before going forward. In the
meantime, this patch fixes the issue described in #18021 in the least invasive
way possible. There are programs that are accepted today that will no longer
be accepted after this patch, but they are arguably pathological programs, and
they are simple to repair.

Fixes #18021.

6 files changed, 38 insertions, 23 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T5515.stderr b/testsuite/tests/indexed-types/should_fail/T5515.stderr
index ebeb52b5cd..688eef697e 100644
--- a/testsuite/tests/indexed-types/should_fail/T5515.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5515.stderr
@@ -1,24 +1,8 @@
 
-T5515.hs:6:16: error:
-    • Expecting one more argument to ‘ctx’
-      Expected a type, but ‘ctx’ has kind ‘* -> Constraint’
-    • In the first argument of ‘Arg’, namely ‘ctx’
-      In the first argument of ‘ctx’, namely ‘(Arg ctx)’
-      In the class declaration for ‘Bome’
+T5515.hs:9:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
+      All such variables must be bound on the LHS
 
-T5515.hs:14:1: error:
-    • Type variable ‘a’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘Arg’
-      In the instance declaration for ‘Some f’
-
-T5515.hs:14:10: error:
-    • Could not deduce (C f a0)
-      from the context: C f a
-        bound by an instance declaration:
-                   forall f a. C f a => Some f
-        at T5515.hs:14:10-24
-      The type variable ‘a0’ is ambiguous
-    • In the ambiguity check for an instance declaration
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the instance declaration for ‘Some f’
+T5515.hs:15:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
+      All such variables must be bound on the LHS
diff --git a/testsuite/tests/polykinds/T9574.stderr b/testsuite/tests/polykinds/T9574.stderr
new file mode 100644
index 0000000000..26f2925ed9
--- /dev/null
+++ b/testsuite/tests/polykinds/T9574.stderr
@@ -0,0 +1,4 @@
+
+T9574.hs:13:5: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘o’
+      All such variables must be bound on the LHS
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index a509dfd665..35d4df559d 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -107,7 +107,7 @@ test('T9725', normal, compile, [''])
 test('T9750', normal, compile, [''])
 test('T9569', normal, compile, [''])
 test('T9838', normal, multimod_compile, ['T9838.hs','-v0'])
-test('T9574', normal, compile, [''])
+test('T9574', normal, compile_fail, [''])
 test('T9833', normal, compile, [''])
 test('T7908', normal, compile, [''])
 test('PolyInstances', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/T18021.hs b/testsuite/tests/rename/should_fail/T18021.hs
new file mode 100644
index 0000000000..2bbc09661e
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T18021.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T18021 where
+
+class C a where
+  data D a
+
+instance forall a. C Int where
+  data instance D Int = MkD1 a
+
+class X a b
+
+instance forall a. C Bool where
+  data instance D Bool = MkD2
+    deriving (X a)
diff --git a/testsuite/tests/rename/should_fail/T18021.stderr b/testsuite/tests/rename/should_fail/T18021.stderr
new file mode 100644
index 0000000000..11fcea9964
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T18021.stderr
@@ -0,0 +1,8 @@
+
+T18021.hs:12:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
+      All such variables must be bound on the LHS
+
+T18021.hs:17:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
+      All such variables must be bound on the LHS
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 81285649ce..833e2d88f3 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -156,6 +156,7 @@ test('T16504', normal, compile_fail, [''])
 test('T14548', normal, compile_fail, [''])
 test('T16610', normal, compile_fail, [''])
 test('T17593', normal, compile_fail, [''])
+test('T18021', normal, compile_fail, [''])
 test('T18145', normal, compile_fail, [''])
 test('T18240a', normal, compile_fail, [''])
 test('T18240b', normal, compile_fail, [''])