Fix #16116 by removing badAssocRhs

7 files changed, 57 insertions, 22 deletions

diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index e5fe3a3a31..0699f80858 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -784,14 +784,6 @@ rnFamInstEqn doc mb_cls rhs_kvars
                                       ++ map hsLTyVarName bndrs'
                     ; warnUnusedTypePatterns all_nms nms_used
 
-                         -- See Note [Renaming associated types]
-                    ; let bad_tvs = maybe [] (filter is_bad . snd) mb_cls
-                          var_name_set = mkNameSet (map hsLTyVarName bndrs'
-                                                    ++ all_imp_var_names)
-                          is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs
-                                           && not (cls_tkv `elemNameSet` var_name_set)
-                    ; unless (null bad_tvs) (badAssocRhs bad_tvs)
-
                     ; return ((bndrs', pats', payload'), rhs_fvs `plusFV` pat_fvs) }
 
        ; let all_fvs  = fvs `addOneFV` unLoc tycon'
@@ -999,6 +991,21 @@ can all be in scope (Trac #5862):
       id :: Ob x a => x a a
       (.) :: (Ob x a, Ob x b, Ob x c) => x b c -> x a b -> x a c
 Here 'k' is in scope in the kind signature, just like 'x'.
+
+Although type family equations can bind type variables with explicit foralls,
+it need not be the case that all variables that appear on the RHS must be bound
+by a forall. For instance, the following is acceptable:
+
+   class C a where
+     type T a b
+   instance C (Maybe a) where
+     type forall b. T (Maybe a) b = Either a b
+
+Even though `a` is not bound by the forall, this is still accepted because `a`
+was previously bound by the `instance C (Maybe a)` part. (see Trac #16116).
+
+In each case, the function which detects improperly bound variables on the RHS
+is TcValidity.checkValidFamPats.
 -}
 
 
@@ -2078,13 +2085,6 @@ are no data constructors we allow h98_style = True
 ***************************************************** -}
 
 ---------------
-badAssocRhs :: [Name] -> RnM ()
-badAssocRhs ns
-  = addErr (hang (text "The RHS of an associated type declaration mentions"
-                  <+> text "out-of-scope variable" <> plural ns
-                  <+> pprWithCommas (quotes . ppr) ns)
-               2 (text "All such variables must be bound on the LHS"))
-
 wrongTyFamName :: Name -> Name -> SDoc
 wrongTyFamName fam_tc_name eqn_tc_name
   = hang (text "Mismatched type name in type family instance.")
diff --git a/testsuite/tests/indexed-types/should_fail/T5515.stderr b/testsuite/tests/indexed-types/should_fail/T5515.stderr
index 688eef697e..ebeb52b5cd 100644
--- a/testsuite/tests/indexed-types/should_fail/T5515.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5515.stderr
@@ -1,8 +1,24 @@
 
-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: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: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
+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’
diff --git a/testsuite/tests/rename/should_compile/T16116a.hs b/testsuite/tests/rename/should_compile/T16116a.hs
new file mode 100644
index 0000000000..b5be6cc968
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T16116a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16616a where
+
+class C a where
+  type T a b
+
+instance C (Maybe a) where
+  type forall b. T (Maybe a) b = Either a b
diff --git a/testsuite/tests/rename/should_compile/all.T b/testsuite/tests/rename/should_compile/all.T
index 0bcd25ccf1..a7c8da4671 100644
--- a/testsuite/tests/rename/should_compile/all.T
+++ b/testsuite/tests/rename/should_compile/all.T
@@ -166,4 +166,4 @@ test('T15994', [], run_command, ['$MAKE -s --no-print-directory T15994'])
 test('T15798a', normal, compile, [''])
 test('T15798b', normal, compile, [''])
 test('T15798c', normal, compile, [''])
-
+test('T16116a', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/T16116b.hs b/testsuite/tests/rename/should_fail/T16116b.hs
new file mode 100644
index 0000000000..c1de71d5e0
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16116b.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+module T16116b where
+
+class C a where
+  type F a
+instance C [a] where
+  type F [a] = b
diff --git a/testsuite/tests/rename/should_fail/T16116b.stderr b/testsuite/tests/rename/should_fail/T16116b.stderr
new file mode 100644
index 0000000000..ff6b5e13a4
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16116b.stderr
@@ -0,0 +1,2 @@
+
+T16116b.hs:7:16: error: Not in scope: type variable ‘b’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index d5a5ec58e9..03ee63b449 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -144,4 +144,5 @@ test('T15611b', normal, ghci_script, ['T15611b.script'])
 test('T15828', normal, compile_fail, [''])
 test('T16002', normal, compile_fail, [''])
 test('T16114', normal, compile_fail, [''])
+test('T16116b', normal, compile_fail, [''])
 test('ExplicitForAllRules2', normal, compile_fail, [''])