More explicit foralls (GHC Proposal 0007)

Allow the user to explicitly bind type/kind variables in type and data
family instances (including associated instances), closed type family
equations, and RULES pragmas. Follows the specification of GHC
Proposal 0007, also fixes #2600. Advised by Richard Eisenberg.

This modifies the Template Haskell AST -- old code may break!

Other Changes:
- convert HsRule to a record
- make rnHsSigWcType more general
- add repMaybe to DsMeta

Includes submodule update for Haddock.

Test Plan: validate

Reviewers: goldfire, bgamari, alanz

Subscribers: simonpj, RyanGlScott, goldfire, rwbarton,
             thomie, mpickering, carter

GHC Trac Issues: #2600, #14268

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

42 files changed, 469 insertions, 49 deletions

diff --git a/testsuite/tests/ghc-api/annotations/stringSource.hs b/testsuite/tests/ghc-api/annotations/stringSource.hs
index 96702f5235..1b5803b817 100644
--- a/testsuite/tests/ghc-api/annotations/stringSource.hs
+++ b/testsuite/tests/ghc-api/annotations/stringSource.hs
@@ -73,7 +73,7 @@ testOneFile libdir fileName = do
 
      doRuleDecl :: RuleDecl GhcPs
                 -> [(String,[Located (SourceText,FastString)])]
-     doRuleDecl (HsRule _ ss _ _ _ _) = [("r",[ss])]
+     doRuleDecl (HsRule _ ss _ _ _ _ _) = [("r",[ss])]
 
      doCCallTarget :: CCallTarget
                    -> [(String,[Located (SourceText,FastString)])]
diff --git a/testsuite/tests/ghc-api/annotations/t11430.hs b/testsuite/tests/ghc-api/annotations/t11430.hs
index 5a50af85f1..232d47ff98 100644
--- a/testsuite/tests/ghc-api/annotations/t11430.hs
+++ b/testsuite/tests/ghc-api/annotations/t11430.hs
@@ -60,11 +60,11 @@ testOneFile libdir fileName = do
 
      doRuleDecl :: RuleDecl GhcPs
                 -> [(String,[String])]
-     doRuleDecl (HsRule _ _ (ActiveBefore (SourceText ss) _) _ _ _)
+     doRuleDecl (HsRule _ _ (ActiveBefore (SourceText ss) _) _ _ _ _)
        = [("rb",[ss])]
-     doRuleDecl (HsRule _ _ (ActiveAfter (SourceText ss) _) _ _ _)
+     doRuleDecl (HsRule _ _ (ActiveAfter (SourceText ss) _) _ _ _ _)
        = [("ra",[ss])]
-     doRuleDecl (HsRule _ _ _ _ _ _) = []
+     doRuleDecl (HsRule _ _ _ _ _ _ _) = []
 
      doHsExpr :: HsExpr GhcPs -> [(String,[String])]
      doHsExpr (HsTickPragma _ src (_,_,_) ss _) = [("tp",[show ss])]
diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
new file mode 100644
index 0000000000..067127cf8a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeInType #-}
+
+module ExplicitForAllFams where
+
+import Data.Proxy
+import Data.Kind
+
+-- From Proposal 0007
+
+data family F a
+data instance forall (x :: Bool). F (Proxy x) = MkF
+
+class C a where
+  type G a b
+instance forall a. C [a] where
+  type forall b. G [a] b = Int
+
+type family H a b where
+  forall x y. H [x] (Proxy y) = Double
+  forall z.   H z   z         = Bool
+
+-- More tests
+
+type family D a b where
+  forall (a :: Type -> Type) (b :: a Int) (c :: k). D (Proxy b) (Proxy c) = ()
+  forall (a :: Bool) (b :: Proxy a). D (Proxy b) () = Int
+  forall (a :: Type). D a a = Maybe a
diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.hs b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.hs
new file mode 100644
index 0000000000..2b8e2cbed8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ExplicitForAllFams2 where
+
+import Data.Kind (Type)
+
+-- Even more tests
+
+type family CF a b where
+  forall x y.         CF [x] (Maybe y) = (x,y)
+  forall (z :: Type). CF z   z         = Bool
+  forall.             CF _   _         = ()
+
+type family OF a
+type instance forall a b. OF (Maybe a, Either a b) = Either [a] b
+
+data family DF a
+data instance forall a b. DF (Maybe a, Either a b) = DF a a b
+
+data family NF a
+newtype instance forall a b. NF (Maybe a, Either a b) = NF { unNF :: Either [a] b }
+
+class Cl a where
+  type AT a b
+  data AD a b
+instance forall a. Cl (Maybe a) where
+  type forall b. AT (Maybe a) b = b
+  data forall b. AD (Maybe a) b = AD b
+
+-- Should produce warnings
+
+type family N a where
+  forall t a. N (t a) = [a]
+  forall a.   N a     = ()
+
+type family N' a where
+  N' (t a) = [a]
+  N' a     = ()
diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.stderr b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.stderr
new file mode 100644
index 0000000000..0d2eaae027
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.stderr
@@ -0,0 +1,12 @@
+
+ExplicitForAllFams2.hs:34:10: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘t’
+
+ExplicitForAllFams2.hs:35:10: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘a’
+
+ExplicitForAllFams2.hs:38:7: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘t’
+
+ExplicitForAllFams2.hs:39:6: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘a’
diff --git a/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarnings.stderr b/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarnings.stderr
index 5881145e23..833315e6be 100644
--- a/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarnings.stderr
+++ b/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarnings.stderr
@@ -1,12 +1,12 @@
 
-UnusedTyVarWarnings.hs:8:5: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarnings.hs:8:7: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
 
-UnusedTyVarWarnings.hs:11:18: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarnings.hs:11:20: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
 
 UnusedTyVarWarnings.hs:27:5: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘a’
+    Defined but not used on the right hand side: type variable ‘a’
 
-UnusedTyVarWarnings.hs:33:17: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarnings.hs:33:19: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
diff --git a/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarningsNamedWCs.stderr b/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarningsNamedWCs.stderr
index 6cbc861b28..9049ddf696 100644
--- a/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarningsNamedWCs.stderr
+++ b/testsuite/tests/indexed-types/should_compile/UnusedTyVarWarningsNamedWCs.stderr
@@ -1,12 +1,12 @@
 
-UnusedTyVarWarningsNamedWCs.hs:8:5: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarningsNamedWCs.hs:8:7: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
 
-UnusedTyVarWarningsNamedWCs.hs:11:18: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarningsNamedWCs.hs:11:20: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
 
 UnusedTyVarWarningsNamedWCs.hs:27:5: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘a’
+    Defined but not used on the right hand side: type variable ‘a’
 
-UnusedTyVarWarningsNamedWCs.hs:33:17: warning: [-Wunused-type-patterns]
-    Defined but not used: type variable ‘b’
+UnusedTyVarWarningsNamedWCs.hs:33:19: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘b’
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5bfbca4db9..d95826c362 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -94,6 +94,9 @@ test('GivenCheckSwap', normal, compile, [''])
 test('GivenCheckDecomp', normal, compile, [''])
 test('GivenCheckTop', normal, compile, [''])
 
+test('ExplicitForAllFams1', normal, compile, [''])
+test('ExplicitForAllFams2', normal, compile, ['-Wunused-foralls -Wunused-type-patterns'])
+
 # A very delicate test
 test('Gentle', normal, compile, [''])
 
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.hs
new file mode 100644
index 0000000000..53a0e2ab32
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ExplicitForAllFams3 where
+
+type family H a b where
+  forall a.   H [a] (Maybe b) = Double
+
+type family J a
+type instance forall a.   J (a, b) = Bool
+
+data family K a
+data instance forall a.   K (a, b)    = K4 Bool
+
+data family L a
+newtype instance forall a.   L (a, b)    = L4 { unL4 :: Bool    }
+
+class C a where
+  type CT a b
+  data CD a b
+instance C Int where
+  type forall a.   CT [a] (Maybe b) = Bool
+  data forall a.   CD [a] (Maybe b) = CD4 Bool
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.stderr
new file mode 100644
index 0000000000..92e0b1df64
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams3.stderr
@@ -0,0 +1,17 @@
+
+ExplicitForAllFams3.hs:7:28: error: Not in scope: type variable ‘b’
+
+ExplicitForAllFams3.hs:10:33: error:
+    Not in scope: type variable ‘b’
+
+ExplicitForAllFams3.hs:13:33: error:
+    Not in scope: type variable ‘b’
+
+ExplicitForAllFams3.hs:16:36: error:
+    Not in scope: type variable ‘b’
+
+ExplicitForAllFams3.hs:22:34: error:
+    Not in scope: type variable ‘b’
+
+ExplicitForAllFams3.hs:23:34: error:
+    Not in scope: type variable ‘b’
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.hs
new file mode 100644
index 0000000000..f99e884161
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ExplicitForAllFams4a where
+
+type family H a b where
+  forall a b. H [a] (a,a)     = Float
+  forall b.   H _ _           = Maybe b
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
new file mode 100644
index 0000000000..ecbd7d9e79
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
@@ -0,0 +1,8 @@
+
+ExplicitForAllFams4a.hs:7:12: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type family declaration for ‘H’
+
+ExplicitForAllFams4a.hs:8:10: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type family declaration for ‘H’
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
new file mode 100644
index 0000000000..cb5665401b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ExplicitForAllFams4 where
+
+type family J a
+type instance forall a b. J [a]    = Float
+type instance forall b.   J _      = Maybe b
+
+data family K a
+data instance forall a b. K (a, Bool) = K5 Float
+data instance forall b.   K _         = K6 (Maybe b)
+
+data family L a
+newtype instance forall a b. L (a, Bool) = L5 { unL5 :: Float   }
+newtype instance forall b.   L _         = L6 { unL56:: Maybe b }
+
+class C a where
+  type CT a b
+  data CD a b
+
+instance C Int where
+  type forall a b. CT [a] (a,a)     = Float
+  type forall b.   CT _ _           = Maybe b
+  data forall a b. CD [a] (a,a)     = CD5 Float
+  data forall b.   CD _ _           = CD6 (Maybe b)
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
new file mode 100644
index 0000000000..0861a8a756
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
@@ -0,0 +1,44 @@
+
+ExplicitForAllFams4b.hs:7:24: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type instance declaration for ‘J’
+
+ExplicitForAllFams4b.hs:8:22: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type instance declaration for ‘J’
+
+ExplicitForAllFams4b.hs:11:24: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the data instance declaration for ‘K’
+
+ExplicitForAllFams4b.hs:12:22: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the data instance declaration for ‘K’
+
+ExplicitForAllFams4b.hs:15:27: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the newtype instance declaration for ‘L’
+
+ExplicitForAllFams4b.hs:16:25: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the newtype instance declaration for ‘L’
+
+ExplicitForAllFams4b.hs:23:17: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:24:15: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:25:17: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:26:15: error:
+    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 11e9d0a65d..12fa999a9f 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -35,6 +35,10 @@ test('OverIndirectThisMod', [], multimod_compile_fail, ['OverIndirectThisModD',
 
 test('SkolemOccursLoop', expect_fail, compile_fail, [''])
 
+test('ExplicitForAllFams3', normal, compile_fail, [''])
+test('ExplicitForAllFams4a', normal, compile_fail, [''])
+test('ExplicitForAllFams4b', normal, compile_fail, [''])
+
 test('T2334A', normal, compile_fail, [''])
 test('T1900', normal, compile_fail, [''])
 test('T2157', normal, compile_fail, [''])
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index edc66e0a2d..4648baa1f1 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -78,6 +78,7 @@
              ({ DumpParsedAst.hs:8:3-8 }
               (Unqual
                {OccName: Length}))
+             (Nothing)
              [({ DumpParsedAst.hs:8:10-17 }
                (HsParTy
                 (NoExt)
@@ -140,6 +141,7 @@
              ({ DumpParsedAst.hs:9:3-8 }
               (Unqual
                {OccName: Length}))
+             (Nothing)
              [({ DumpParsedAst.hs:9:10-12 }
                (HsExplicitListTy
                 (NoExt)
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index f20c450a9a..5c1a03e091 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -131,6 +131,7 @@
                (NoExt)
                ({ DumpRenamedAst.hs:11:3-8 }
                 {Name: DumpRenamedAst.Length})
+               (Nothing)
                [({ DumpRenamedAst.hs:11:10-17 }
                  (HsParTy
                   (NoExt)
@@ -186,6 +187,7 @@
                (NoExt)
                ({ DumpRenamedAst.hs:12:3-8 }
                 {Name: DumpRenamedAst.Length})
+               (Nothing)
                [({ DumpRenamedAst.hs:12:10-12 }
                  (HsExplicitListTy
                   (NoExt)
@@ -289,6 +291,7 @@
            (NoExt)
            ({ DumpRenamedAst.hs:17:18-20 }
             {Name: DumpRenamedAst.Nat})
+           (Nothing)
            [({ DumpRenamedAst.hs:17:22-37 }
              (HsParTy
               (NoExt)
diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr
index 4aee57db37..71a54b085a 100644
--- a/testsuite/tests/parser/should_compile/KindSigs.stderr
+++ b/testsuite/tests/parser/should_compile/KindSigs.stderr
@@ -37,6 +37,7 @@
              ({ KindSigs.hs:12:3-5 }
               (Unqual
                {OccName: Foo}))
+             (Nothing)
              [({ KindSigs.hs:12:7 }
                (HsTyVar
                 (NoExt)
diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.hs b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.hs
new file mode 100644
index 0000000000..7862468d17
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeApplications #-}
+
+module ExplicitForAllRules1 where
+
+import Data.Proxy
+import Data.Kind
+
+-- From Proposal 0007 (w/ fix to "example")
+
+{-# RULES
+"example"  forall a b. forall. map @a @b f = f
+"example2" forall a. forall (x :: a). id x = x
+  #-}
+
+{-# NOINLINE f #-}
+f :: a -> b
+f = undefined
+
+-- More tests
+
+{-# RULES
+"example3" forall (a :: Type -> Type) (b :: a Int) c. forall x y. g @(Proxy b) @(Proxy c) x y = ()
+"example4" forall (a :: Bool) (b :: Proxy a). forall x. g @(Proxy b) @() x = id @()
+"example5" forall (a :: Type). forall. h @a = id @a
+"example5" forall k (c :: k). forall (x :: Proxy c). id @(Proxy c) x = x
+  #-}
+
+{-# NOINLINE g #-}
+g :: a -> b -> ()
+g _ _ = ()
+
+{-# NOINLINE h #-}
+h :: a -> a
+h x = x
+
+-- Should NOT have a parse error :(
+{-# RULES "example6" forall a forall. g a forall = () #-}
+
+-- Should generate a warning
+{-# RULES "example7" forall a b. forall (x :: a). id x = x #-}
diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
new file mode 100644
index 0000000000..54a32adafd
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
@@ -0,0 +1,4 @@
+
+ExplicitForAllRules1.hs:45:31: warning: [-Wunused-foralls (in -Wextra)]
+    Unused quantified type variable ‘b’
+    in the rule "example7"
diff --git a/testsuite/tests/rename/should_compile/T2600.hs b/testsuite/tests/rename/should_compile/T2600.hs
new file mode 100644
index 0000000000..bdf483cace
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T2600.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T2600 where
+
+-- ** See trac #10595 for why we're okay with this generating warnings! **
+
+class T t where
+    to :: [a] -> t a
+    from :: t a -> [a]
+    tmap :: (a -> a) -> t a -> t a
+
+{-# RULES
+
+"myrule" forall t a. forall f x.
+     from (tmap f (to x :: t a)) = map f (from (to x :: t a))
+
+  #-}
diff --git a/testsuite/tests/rename/should_compile/T2600.stderr b/testsuite/tests/rename/should_compile/T2600.stderr
new file mode 100644
index 0000000000..91f594ff9e
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T2600.stderr
@@ -0,0 +1,10 @@
+
+T2600.hs:16:1: warning: [-Winline-rule-shadowing (in -Wdefault)]
+    Rule "myrule" may never fire
+      because rule "Class op tmap" for ‘tmap’ might fire first
+    Probable fix: add phase [n] or [~n] to the competing rule
+
+T2600.hs:16:1: warning: [-Winline-rule-shadowing (in -Wdefault)]
+    Rule "myrule" may never fire
+      because rule "Class op to" for ‘to’ might fire first
+    Probable fix: add phase [n] or [~n] to the competing rule
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_compile/all.T b/testsuite/tests/rename/should_compile/all.T
index 3a90cbd667..a3f862f8a4 100644
--- a/testsuite/tests/rename/should_compile/all.T
+++ b/testsuite/tests/rename/should_compile/all.T
@@ -81,6 +81,10 @@ test('T2205', normal, compile, [''])
 
 test('T2334', normal, compile, [''])
 test('T2506', normal, compile, [''])
+
+test('ExplicitForAllRules1', normal, compile, ['-Wunused-foralls'])
+test('T2600', normal, compile, [''])
+
 test('T2914', normal, compile, [''])
 test('T3221', normal, compile, [''])
 test('T3262', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/ExplicitForAllRules2.hs b/testsuite/tests/rename/should_fail/ExplicitForAllRules2.hs
new file mode 100644
index 0000000000..081b39bced
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/ExplicitForAllRules2.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeApplications #-}
+
+module ExplicitForAllRules2 where
+
+{-# RULES "new4" forall a. forall (x :: b). id @a (wk x) = (wk x) #-}
+{-# RULES "new5" forall a. forall (x :: a). id @a y = y #-}
+{-# RULES "new6" forall a. forall (x :: a). id @c x = x #-}
+
+{-# NOINLINE wk #-}
+wk :: forall b a. b -> a
+wk _ = error ""
diff --git a/testsuite/tests/rename/should_fail/ExplicitForAllRules2.stderr b/testsuite/tests/rename/should_fail/ExplicitForAllRules2.stderr
new file mode 100644
index 0000000000..909cc0ae20
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/ExplicitForAllRules2.stderr
@@ -0,0 +1,10 @@
+
+ExplicitForAllRules2.hs:6:41: error:
+    Not in scope: type variable ‘b’
+
+ExplicitForAllRules2.hs:7:11: error:
+    Rule "new5":
+    Forall'd variable ‘x’ does not appear on left hand side
+
+ExplicitForAllRules2.hs:8:49: error:
+    Not in scope: type variable ‘c’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index db0db47ca9..6debe7b917 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -138,3 +138,5 @@ test('T15539', normal, compile_fail, [''])
 test('T15487', normal, multimod_compile_fail, ['T15487','-v0'])
 test('T15659', normal, compile_fail, [''])
 test('T15607', normal, compile_fail, [''])
+
+test('ExplicitForAllRules2', normal, compile_fail, [''])
diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs
index 0b25da9248..2a8b3b4ab6 100644
--- a/testsuite/tests/th/ClosedFam2TH.hs
+++ b/testsuite/tests/th/ClosedFam2TH.hs
@@ -11,10 +11,12 @@ $( return [ ClosedTypeFamilyD
                 , KindedTV (mkName "b") (VarT (mkName "k")) ]
                 ( TyVarSig (KindedTV (mkName "r") (VarT (mkName "k"))))
                 Nothing)
-              [ TySynEqn [ (VarT (mkName "a"))
+              [ TySynEqn Nothing
+                         [ (VarT (mkName "a"))
                          , (VarT (mkName "a")) ]
                          (ConT (mkName "Int"))
-              , TySynEqn [ (VarT (mkName "a"))
+              , TySynEqn Nothing
+                         [ (VarT (mkName "a"))
                          , (VarT (mkName "b")) ]
                          (ConT (mkName "Bool")) ] ])
 
diff --git a/testsuite/tests/th/T12503.hs b/testsuite/tests/th/T12503.hs
index 517c4ba156..eef302c429 100644
--- a/testsuite/tests/th/T12503.hs
+++ b/testsuite/tests/th/T12503.hs
@@ -21,7 +21,7 @@ data family T2 (a :: b)
 data instance T2 b
 class C2 a
 
-$(do FamilyI (DataFamilyD tName _ _) [DataInstD [] _ [tyVar] _ _ _]
+$(do FamilyI (DataFamilyD tName _ _) [DataInstD [] _ _ [tyVar] _ _ _]
        <- reify ''T2
      d <- instanceD (cxt [])
                     (conT ''C2 `appT` (conT tName `appT` return tyVar))
diff --git a/testsuite/tests/th/T12646.stderr b/testsuite/tests/th/T12646.stderr
index 647ccd6396..5b25cff89f 100644
--- a/testsuite/tests/th/T12646.stderr
+++ b/testsuite/tests/th/T12646.stderr
@@ -1,3 +1,4 @@
 type family T12646.F (a_0 :: k_1) :: * where
-    T12646.F (a_2 :: * -> *) = GHC.Types.Int
-    T12646.F (a_3 :: k_4) = GHC.Types.Char
+    forall (a_2 :: * -> *). T12646.F (a_2 :: * -> *) = GHC.Types.Int
+    forall (k_3 :: *)
+           (a_4 :: k_3). T12646.F (a_4 :: k_3) = GHC.Types.Char
diff --git a/testsuite/tests/th/T13618.hs b/testsuite/tests/th/T13618.hs
index 487b5e4efc..1156aada39 100644
--- a/testsuite/tests/th/T13618.hs
+++ b/testsuite/tests/th/T13618.hs
@@ -15,11 +15,11 @@ $(return [])
 main :: IO ()
 main = print
   $(do FamilyI (DataFamilyD _ _ _) insts <- reify ''DF
-       lift $ all (\case DataInstD _ _ [AppT _ (VarT v1)] _
-                                       [NormalC _ [(_, VarT v2)]] _
+       lift $ all (\case DataInstD _ _ _ [AppT _ (VarT v1)] _
+                                         [NormalC _ [(_, VarT v2)]] _
                            -> v1 == v2
-                         NewtypeInstD _ _ [AppT _ (VarT v1)] _
-                                          (NormalC _ [(_, VarT v2)]) _
+                         NewtypeInstD _ _ _ [AppT _ (VarT v1)] _
+                                            (NormalC _ [(_, VarT v2)]) _
                            -> v1 == v2
                          _ -> error "Not a data or newtype instance")
               insts)
diff --git a/testsuite/tests/th/T5886a.hs b/testsuite/tests/th/T5886a.hs
index 33b4d0e1e2..5756fcc513 100644
--- a/testsuite/tests/th/T5886a.hs
+++ b/testsuite/tests/th/T5886a.hs
@@ -11,5 +11,5 @@ class C α where
   type AT α ∷ Type
 
 bang ∷ DecsQ
-bang = return [InstanceD Nothing [] (AppT (ConT ''C) (ConT ''Int))
-                [TySynInstD ''AT (TySynEqn [ConT ''Int] (ConT ''Int))]]
+bang = return [InstanceD Nothing  [] (AppT (ConT ''C) (ConT ''Int))
+                [TySynInstD ''AT (TySynEqn Nothing [ConT ''Int] (ConT ''Int))]]
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
index 442e4ab5dd..6b7b67d5a9 100644
--- a/testsuite/tests/th/T6018th.hs
+++ b/testsuite/tests/th/T6018th.hs
@@ -20,17 +20,20 @@ $( return
                              [(mkName "a"), (mkName "b"), (mkName "c") ]))
    , TySynInstD
        (mkName "F")
-       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Int"), ConT (mkName "Char")
                  , ConT (mkName "Bool")]
                  ( ConT (mkName "Bool")))
    , TySynInstD
        (mkName "F")
-       (TySynEqn [ ConT (mkName "Char"), ConT (mkName "Bool")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Char"), ConT (mkName "Bool")
                  , ConT (mkName "Int")]
                  ( ConT (mkName "Int")))
    , TySynInstD
        (mkName "F")
-       (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Bool"), ConT (mkName "Int")
                  , ConT (mkName "Char")]
                  ( ConT (mkName "Char")))
    ] )
@@ -48,7 +51,8 @@ $( return
        (Just $ InjectivityAnn (mkName "r") [mkName "a"]))
    , TySynInstD
        (mkName "J")
-       (TySynEqn [ ConT (mkName "Int"), VarT (mkName "b") ]
+       (TySynEqn Nothing
+                 [ ConT (mkName "Int"), VarT (mkName "b") ]
                  ( ConT (mkName "Int")))
    ] )
 
@@ -66,13 +70,16 @@ $( return
        , KindedTV (mkName "c") StarT ]
        (TyVarSig (PlainTV (mkName "r")))
        (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")]))
-       [ TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+       [ TySynEqn Nothing
+                  [ ConT (mkName "Int"), ConT (mkName "Char")
                   , ConT (mkName "Bool")]
                   ( ConT (mkName "Bool"))
-       , TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+       , TySynEqn Nothing
+                  [ ConT (mkName "Int"), ConT (mkName "Char")
                   , ConT (mkName "Int")]
                   ( ConT (mkName "Bool"))
-       , TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+       , TySynEqn Nothing
+                  [ ConT (mkName "Bool"), ConT (mkName "Int")
                   , ConT (mkName "Int")]
                   ( ConT (mkName "Int"))
        ]
@@ -103,17 +110,20 @@ $( return
                              [(mkName "a"), (mkName "b") ]))
    , TySynInstD
        (mkName "H")
-       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Int"), ConT (mkName "Char")
                  , ConT (mkName "Bool")]
                  ( ConT (mkName "Bool")))
    , TySynInstD
        (mkName "H")
-       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Int")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Int"), ConT (mkName "Int")
                  , ConT (mkName "Int")]
                  ( ConT (mkName "Bool")))
    , TySynInstD
        (mkName "H")
-       (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+       (TySynEqn Nothing
+                 [ ConT (mkName "Bool"), ConT (mkName "Int")
                  , ConT (mkName "Int")]
                  ( ConT (mkName "Int")))
    ] )
diff --git a/testsuite/tests/th/T6018th.stderr b/testsuite/tests/th/T6018th.stderr
index 7193fb5948..9566b1acd5 100644
--- a/testsuite/tests/th/T6018th.stderr
+++ b/testsuite/tests/th/T6018th.stderr
@@ -1,5 +1,5 @@
 
-T6018th.hs:97:4:
+T6018th.hs:104:4:
     Type family equations violate injectivity annotation:
-      H Int Int Int = Bool -- Defined at T6018th.hs:97:4
-      H Int Char Bool = Bool -- Defined at T6018th.hs:97:4
+      H Int Int Int = Bool -- Defined at T6018th.hs:104:4
+      H Int Char Bool = Bool -- Defined at T6018th.hs:104:4
diff --git a/testsuite/tests/th/T7532a.hs b/testsuite/tests/th/T7532a.hs
index 84fa23e69f..8f686fe206 100644
--- a/testsuite/tests/th/T7532a.hs
+++ b/testsuite/tests/th/T7532a.hs
@@ -11,5 +11,5 @@ class C a where
 bang' :: DecsQ
 bang' = return [
      InstanceD Nothing [] (AppT (ConT ''C) (ConT ''Int)) [
-         DataInstD [] ''D [ConT ''Int] Nothing [
+         DataInstD [] ''D Nothing [ConT ''Int] Nothing [
              NormalC (mkName "T") []] []]]
diff --git a/testsuite/tests/th/T8884.stderr b/testsuite/tests/th/T8884.stderr
index 022776ea7f..3226507172 100644
--- a/testsuite/tests/th/T8884.stderr
+++ b/testsuite/tests/th/T8884.stderr
@@ -1,4 +1,5 @@
 type family T8884.Foo (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0 where
-    T8884.Foo (x_3 :: k_4) = x_3
+    forall (k_3 :: *) (x_4 :: k_3). T8884.Foo (x_4 :: k_3) = x_4
 type family T8884.Baz (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0
-type instance T8884.Baz (x_0 :: k_1) = x_0
+type instance forall (k_0 :: *)
+                     (x_1 :: k_0). T8884.Baz (x_1 :: k_0) = x_1
diff --git a/testsuite/tests/th/T8953.stderr b/testsuite/tests/th/T8953.stderr
index 3dad41244b..d87acef442 100644
--- a/testsuite/tests/th/T8953.stderr
+++ b/testsuite/tests/th/T8953.stderr
@@ -1,6 +1,7 @@
 type family T8953.Poly (a_0 :: k_1) :: *
-type instance T8953.Poly (x_2 :: GHC.Types.Bool) = GHC.Types.Int
-type instance T8953.Poly (x_3 :: GHC.Maybe.Maybe k_4) = GHC.Types.Double
+type instance forall (x_2 :: GHC.Types.Bool). T8953.Poly (x_2 :: GHC.Types.Bool) = GHC.Types.Int
+type instance forall (k_3 :: *)
+                     (x_4 :: GHC.Maybe.Maybe k_3). T8953.Poly (x_4 :: GHC.Maybe.Maybe k_3) = GHC.Types.Double
 type family T8953.Silly :: k_0 -> *
 type instance T8953.Silly = (Data.Proxy.Proxy :: * -> *)
 type instance T8953.Silly = (Data.Proxy.Proxy :: (* -> *) -> *)
@@ -15,5 +16,6 @@ type instance T8953.F GHC.Types.Char = T8953.G (T8953.T1 :: * ->
                                                             (* -> *) -> *)
                                                GHC.Types.Bool
 type family T8953.G (a_0 :: k_1) :: k_1
-type instance T8953.G (T8953.T1 :: k1_2 ->
-                                   k2_3 -> *) = (T8953.T2 :: k1_2 -> k2_3 -> *)
+type instance forall (k1_2 :: *)
+                     (k2_3 :: *). T8953.G (T8953.T1 :: k1_2 ->
+                                                       k2_3 -> *) = (T8953.T2 :: k1_2 -> k2_3 -> *)
diff --git a/testsuite/tests/th/TH_ExplicitForAllRules.hs b/testsuite/tests/th/TH_ExplicitForAllRules.hs
new file mode 100644
index 0000000000..f5bd519db8
--- /dev/null
+++ b/testsuite/tests/th/TH_ExplicitForAllRules.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TemplateHaskell, ExplicitForAll #-}
+
+module Main where
+
+import TH_ExplicitForAllRules_a
+
+$(decls)
+
+main = hsToTh
diff --git a/testsuite/tests/th/TH_ExplicitForAllRules.stdout b/testsuite/tests/th/TH_ExplicitForAllRules.stdout
new file mode 100644
index 0000000000..635fce750e
--- /dev/null
+++ b/testsuite/tests/th/TH_ExplicitForAllRules.stdout
@@ -0,0 +1,3 @@
+{-# RULES "example"
+    forall a_0 . forall (x_1 :: a_0) . GHC.Base.id x_1
+    = x_1 #-}
\ No newline at end of file
diff --git a/testsuite/tests/th/TH_ExplicitForAllRules_a.hs b/testsuite/tests/th/TH_ExplicitForAllRules_a.hs
new file mode 100644
index 0000000000..e428035492
--- /dev/null
+++ b/testsuite/tests/th/TH_ExplicitForAllRules_a.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitForAll #-}
+module TH_ExplicitForAllRules_a (decls, hsToTh) where
+
+import Language.Haskell.TH
+
+decls = [d| {-# RULES "example" forall a. forall (x :: a). id x = x #-} |]
+
+hsToTh = do
+  decls' <- runQ decls
+  mapM (print . ppr) decls'
diff --git a/testsuite/tests/th/TH_reifyExplicitForAllFams.hs b/testsuite/tests/th/TH_reifyExplicitForAllFams.hs
new file mode 100644
index 0000000000..60a6d4563f
--- /dev/null
+++ b/testsuite/tests/th/TH_reifyExplicitForAllFams.hs
@@ -0,0 +1,35 @@
+-- test reification of explicit foralls in type families
+
+{-# LANGUAGE TypeFamilies, ExplicitForAll #-}
+module TH_reifyExplicitForAllFams where
+
+import System.IO
+import Language.Haskell.TH
+import Text.PrettyPrint.HughesPJ
+
+import Data.Proxy
+import Data.Kind
+
+$([d| data family F a
+      data instance forall a. F (Maybe a) = MkF a |])
+
+$([d| class C a where
+        type G a b
+      instance forall a. C [a] where
+        type forall b. G [a] b = Proxy b |])
+
+$([d| type family H a b where
+        forall x y. H [x] (Proxy y) = Either x y
+        forall z.   H z   z         = Maybe z |])
+
+$(return [])
+
+test :: ()
+test = $(let
+      display :: Name -> Q ()
+      display q = do { i <- reify q; runIO $ hPutStrLn stderr (pprint i) }
+    in do { display ''F
+          ; display ''C
+          ; display ''G
+          ; display ''H
+          ; [| () |] })
diff --git a/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr
new file mode 100644
index 0000000000..6205547873
--- /dev/null
+++ b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr
@@ -0,0 +1,16 @@
+data family TH_reifyExplicitForAllFams.F (a_0 :: *) :: *
+data instance forall (a_1 :: *). TH_reifyExplicitForAllFams.F (GHC.Maybe.Maybe a_1)
+    = TH_reifyExplicitForAllFams.MkF a_1
+class TH_reifyExplicitForAllFams.C (a_0 :: *)
+    where type TH_reifyExplicitForAllFams.G (a_0 :: *) (b_1 :: *) :: *
+instance TH_reifyExplicitForAllFams.C ([a_2])
+type family TH_reifyExplicitForAllFams.G (a_0 :: *) (b_1 :: *) :: *
+type instance forall (a_2 :: *)
+                     (b_3 :: *). TH_reifyExplicitForAllFams.G ([a_2])
+                                                              b_3 = Data.Proxy.Proxy b_3
+type family TH_reifyExplicitForAllFams.H (a_0 :: *) (b_1 :: *) :: * where
+    forall (x_2 :: *) (y_3 :: *). TH_reifyExplicitForAllFams.H ([x_2])
+                                                               (Data.Proxy.Proxy y_3) = Data.Either.Either x_2
+                                                                                                           y_3
+    forall (z_4 :: *). TH_reifyExplicitForAllFams.H z_4
+                                                    z_4 = GHC.Maybe.Maybe z_4
\ No newline at end of file
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 75ec5dbca6..50154a4fea 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -76,6 +76,10 @@ test('TH_reifyMkName', normal, compile, ['-v0'])
 
 test('TH_reifyInstances', normal, compile, ['-v0'])
 
+test('TH_reifyExplicitForAllFams', normal, compile, ['-v0'])
+test('TH_ExplicitForAllRules', normal, multimod_compile_and_run,
+     ['TH_ExplicitForAllRules.hs', '-v0 ' + config.ghc_th_way_flags])
+
 test('TH_spliceDecl1', normal, compile, ['-v0'])
 test('TH_spliceDecl2', normal, compile, ['-v0'])
 test('TH_spliceDecl3', [], multimod_compile,