Explicit Specificity

Implementation for Ticket #16393.
Explicit specificity allows users to manually create inferred type variables,
by marking them with braces.
This way, the user determines which variables can be instantiated through
visible type application.

The additional syntax is included in the parser, allowing users to write
braces in type variable binders (type signatures, data constructors etc).
This information is passed along through the renamer and verified in the
type checker.
The AST for type variable binders, data constructors, pattern synonyms,
partial signatures and Template Haskell has been updated to include the
specificity of type variables.

Minor notes:
- Bumps haddock submodule
- Disables pattern match checking in GHC.Iface.Type with GHC 8.8

57 files changed, 378 insertions, 67 deletions

diff --git a/testsuite/tests/ghci/scripts/T11098.stdout b/testsuite/tests/ghci/scripts/T11098.stdout
index 5a748053c3..7ff1306768 100644
--- a/testsuite/tests/ghci/scripts/T11098.stdout
+++ b/testsuite/tests/ghci/scripts/T11098.stdout
@@ -1,3 +1,3 @@
 [SigD foo_1 (AppT (AppT ArrowT (VarT a_0)) (VarT a_0)),FunD foo_1 [Clause [VarP x_2] (NormalB (VarE x_2)) []]]
 "[SigD foo_ (AppT (AppT ArrowT (VarT _a_)) (VarT _a_)),FunD foo_ [Clause [VarP x_] (NormalB (VarE x_)) []]]"
-[SigD foo_6 (ForallT [PlainTV _a_5] [] (AppT (AppT ArrowT (VarT _a_5)) (VarT _a_5))),FunD foo_6 [Clause [VarP x_7] (NormalB (VarE x_7)) []]]
+[SigD foo_6 (ForallT [PlainTV _a_5 SpecifiedSpec] [] (AppT (AppT ArrowT (VarT _a_5)) (VarT _a_5))),FunD foo_6 [Clause [VarP x_7] (NormalB (VarE x_7)) []]]
diff --git a/testsuite/tests/indexed-types/should_fail/T9160.hs b/testsuite/tests/indexed-types/should_fail/T9160.hs
index 9186686579..cefa18d6f3 100644
--- a/testsuite/tests/indexed-types/should_fail/T9160.hs
+++ b/testsuite/tests/indexed-types/should_fail/T9160.hs
@@ -7,7 +7,7 @@ $( do { cls_nm <- newName "C"
       ; a_nm   <- newName "a"
       ; k_nm   <- newName "k"
       ; f_nm   <- newName "F"
-      ; return [ClassD [] cls_nm [KindedTV a_nm (VarT k_nm)] []
+      ; return [ClassD [] cls_nm [KindedTV a_nm () (VarT k_nm)] []
                  [OpenTypeFamilyD
                    (TypeFamilyHead f_nm [] (KindSig (VarT k_nm)) Nothing)]]})
 
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index 8ae907ee25..7d86febb65 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -177,6 +177,7 @@
         [({ DumpParsedAst.hs:9:21-29 }
           (KindedTyVar
            (NoExtField)
+           (())
            ({ DumpParsedAst.hs:9:21-22 }
             (Unqual
              {OccName: as}))
@@ -215,12 +216,14 @@
        [({ DumpParsedAst.hs:14:8 }
          (UserTyVar
           (NoExtField)
+          (())
           ({ DumpParsedAst.hs:14:8 }
            (Unqual
             {OccName: f}))))
        ,({ DumpParsedAst.hs:14:11-16 }
          (KindedTyVar
           (NoExtField)
+          (())
           ({ DumpParsedAst.hs:14:11 }
            (Unqual
             {OccName: a}))
@@ -362,6 +365,7 @@
         [({ DumpParsedAst.hs:16:17-22 }
           (KindedTyVar
            (NoExtField)
+           (())
            ({ DumpParsedAst.hs:16:17 }
             (Unqual
              {OccName: a}))
@@ -375,6 +379,7 @@
         ,({ DumpParsedAst.hs:16:26-39 }
           (KindedTyVar
            (NoExtField)
+           (())
            ({ DumpParsedAst.hs:16:26 }
             (Unqual
              {OccName: f}))
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 57da7c2199..68dc470498 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -206,6 +206,7 @@
           [({ DumpRenamedAst.hs:11:21-29 }
             (KindedTyVar
              (NoExtField)
+             (())
              ({ DumpRenamedAst.hs:11:21-22 }
               {Name: as})
              ({ DumpRenamedAst.hs:11:27-29 }
@@ -352,15 +353,13 @@
                   {Name: GHC.Types.Type}))))))
             [({ DumpRenamedAst.hs:19:3-45 }
               (ConDeclGADT
-               (NoExtField)
+               [{Name: f}
+               ,{Name: g}]
                [({ DumpRenamedAst.hs:19:3-5 }
                  {Name: DumpRenamedAst.Nat})]
                ({ DumpRenamedAst.hs:19:10-45 }
                 (False))
-               (HsQTvs
-                [{Name: f}
-                ,{Name: g}]
-                [])
+               []
                (Nothing)
                (PrefixCon
                 [({ DumpRenamedAst.hs:19:10-34 }
@@ -373,6 +372,7 @@
                      [({ DumpRenamedAst.hs:19:18-19 }
                        (UserTyVar
                         (NoExtField)
+                        (SpecifiedSpec)
                         ({ DumpRenamedAst.hs:19:18-19 }
                          {Name: xx})))]
                      ({ DumpRenamedAst.hs:19:22-33 }
@@ -451,11 +451,13 @@
          [({ DumpRenamedAst.hs:21:8 }
            (UserTyVar
             (NoExtField)
+            (())
             ({ DumpRenamedAst.hs:21:8 }
              {Name: f})))
          ,({ DumpRenamedAst.hs:21:11-16 }
            (KindedTyVar
             (NoExtField)
+            (())
             ({ DumpRenamedAst.hs:21:11 }
              {Name: a})
             ({ DumpRenamedAst.hs:21:16 }
@@ -587,6 +589,7 @@
           [({ DumpRenamedAst.hs:23:17-22 }
             (KindedTyVar
              (NoExtField)
+             (())
              ({ DumpRenamedAst.hs:23:17 }
               {Name: a})
              ({ DumpRenamedAst.hs:23:22 }
@@ -598,6 +601,7 @@
           ,({ DumpRenamedAst.hs:23:26-39 }
             (KindedTyVar
              (NoExtField)
+             (())
              ({ DumpRenamedAst.hs:23:26 }
               {Name: f})
              ({ DumpRenamedAst.hs:23:31-39 }
diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr
index 06ed01539a..1d6c055436 100644
--- a/testsuite/tests/parser/should_compile/KindSigs.stderr
+++ b/testsuite/tests/parser/should_compile/KindSigs.stderr
@@ -72,6 +72,7 @@
         [({ KindSigs.hs:11:17 }
           (UserTyVar
            (NoExtField)
+           (())
            ({ KindSigs.hs:11:17 }
             (Unqual
              {OccName: a}))))])
@@ -93,6 +94,7 @@
        [({ KindSigs.hs:15:10 }
          (UserTyVar
           (NoExtField)
+          (())
           ({ KindSigs.hs:15:10 }
            (Unqual
             {OccName: a}))))])
@@ -165,6 +167,7 @@
        [({ KindSigs.hs:16:11 }
          (UserTyVar
           (NoExtField)
+          (())
           ({ KindSigs.hs:16:11 }
            (Unqual
             {OccName: a}))))])
@@ -458,6 +461,7 @@
        [({ KindSigs.hs:28:12 }
          (UserTyVar
           (NoExtField)
+          (())
           ({ KindSigs.hs:28:12 }
            (Unqual
             {OccName: b}))))])
diff --git a/testsuite/tests/parser/should_compile/T15323.stderr b/testsuite/tests/parser/should_compile/T15323.stderr
index 25b0ed002d..c69f94afba 100644
--- a/testsuite/tests/parser/should_compile/T15323.stderr
+++ b/testsuite/tests/parser/should_compile/T15323.stderr
@@ -21,6 +21,7 @@
        [({ T15323.hs:5:19 }
          (UserTyVar
           (NoExtField)
+          (())
           ({ T15323.hs:5:19 }
            (Unqual
             {OccName: v}))))])
@@ -40,14 +41,13 @@
              {OccName: TestParens}))]
           ({ T15323.hs:6:21-55 }
            (True))
-          (HsQTvs
-           (NoExtField)
-           [({ T15323.hs:6:28 }
-             (UserTyVar
-              (NoExtField)
-              ({ T15323.hs:6:28 }
-               (Unqual
-                {OccName: v}))))])
+          [({ T15323.hs:6:28 }
+            (UserTyVar
+             (NoExtField)
+             (SpecifiedSpec)
+             ({ T15323.hs:6:28 }
+              (Unqual
+               {OccName: v}))))]
           (Just
            ({ T15323.hs:6:32-37 }
             [({ T15323.hs:6:32-37 }
diff --git a/testsuite/tests/polykinds/T7022a.hs b/testsuite/tests/polykinds/T7022a.hs
index a286fd3c1d..ee71b806c1 100644
--- a/testsuite/tests/polykinds/T7022a.hs
+++ b/testsuite/tests/polykinds/T7022a.hs
@@ -9,5 +9,5 @@ makeSList :: Q [Dec]
 makeSList = do
    a <- newName "a"
    k <- newName "k"
-   return [TySynD (mkName "SList") [KindedTV a (AppT ListT (VarT k))]
+   return [TySynD (mkName "SList") [KindedTV a () (AppT ListT (VarT k))]
                   (AppT (ConT (mkName "Sing")) (VarT a))]
diff --git a/testsuite/tests/printer/T14289b.hs b/testsuite/tests/printer/T14289b.hs
index 3ff39805d6..d35292c5cd 100644
--- a/testsuite/tests/printer/T14289b.hs
+++ b/testsuite/tests/printer/T14289b.hs
@@ -33,7 +33,7 @@ main
 Bceomes
 
 
-[DataD [] Foo_0 [PlainTV a_2] Nothing
+[DataD [] Foo_0 [PlainTV a_2 ()] Nothing
   [NormalC Foo_1 [(Bang NoSourceUnpackedness NoSourceStrictness,VarT a_2)]]
   [DerivClause Nothing
       [AppT (AppT (ConT Main.C) (VarT y_6989586621679027885))
diff --git a/testsuite/tests/printer/T14289c.hs b/testsuite/tests/printer/T14289c.hs
index 6e58df1a54..adf378c41e 100644
--- a/testsuite/tests/printer/T14289c.hs
+++ b/testsuite/tests/printer/T14289c.hs
@@ -30,7 +30,7 @@ main
 ----------------------------------------
 Becomes
 
-[DataD [] Foo_0 [PlainTV a_2] Nothing
+[DataD [] Foo_0 [PlainTV a_2 ()] Nothing
   [NormalC Foo_1 [(Bang NoSourceUnpackedness NoSourceStrictness,VarT a_2)]]
   [DerivClause Nothing
     [AppT (AppT EqualityT (VarT a_2))
diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs
index abe2ddca3b..f1e5eee9c0 100644
--- a/testsuite/tests/th/ClosedFam2TH.hs
+++ b/testsuite/tests/th/ClosedFam2TH.hs
@@ -7,9 +7,9 @@ import Language.Haskell.TH
 $( return [ ClosedTypeFamilyD
               (TypeFamilyHead
                 (mkName "Equals")
-                [ KindedTV (mkName "a") (VarT (mkName "k"))
-                , KindedTV (mkName "b") (VarT (mkName "k")) ]
-                ( TyVarSig (KindedTV (mkName "r") (VarT (mkName "k"))))
+                [ KindedTV (mkName "a") () (VarT (mkName "k"))
+                , KindedTV (mkName "b") () (VarT (mkName "k")) ]
+                ( TyVarSig (KindedTV (mkName "r") () (VarT (mkName "k"))))
                 Nothing)
               [ TySynEqn Nothing
                          (AppT (AppT (ConT (mkName "Equals")) (VarT (mkName "a")))
@@ -29,7 +29,7 @@ b = False
 $( return [ ClosedTypeFamilyD
                (TypeFamilyHead
                 (mkName "Foo")
-                [ KindedTV (mkName "a") (VarT (mkName "k"))]
+                [ KindedTV (mkName "a") () (VarT (mkName "k"))]
                 (KindSig StarT ) Nothing )
                 [ TySynEqn Nothing
                            (AppT (AppKindT (ConT (mkName "Foo")) StarT)
diff --git a/testsuite/tests/th/T10267.hs b/testsuite/tests/th/T10267.hs
index 009d0f035c..45636bf295 100644
--- a/testsuite/tests/th/T10267.hs
+++ b/testsuite/tests/th/T10267.hs
@@ -13,7 +13,7 @@ import T10267a
 
 $(return [
    SigD (mkName "k")
-        (ForallT [PlainTV (mkName "a")]
+        (ForallT [PlainTV (mkName "a") SpecifiedSpec]
                  []
                  (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a"))))
  , FunD (mkName "k")
@@ -22,7 +22,7 @@ $(return [
 
 $(return [
    SigD (mkName "l")
-        (ForallT [PlainTV (mkName "a")]
+        (ForallT [PlainTV (mkName "a") SpecifiedSpec]
                  []
                  (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a"))))
  , FunD (mkName "l")
diff --git a/testsuite/tests/th/T10828.hs b/testsuite/tests/th/T10828.hs
index 94d9b3967b..ffb4525f6a 100644
--- a/testsuite/tests/th/T10828.hs
+++ b/testsuite/tests/th/T10828.hs
@@ -31,7 +31,7 @@ $( do { decl <- [d| data family D a :: Type -> Type
 
 $( return
    [ DataD [] (mkName "T")
-           [ PlainTV (mkName "a") ]
+           [ PlainTV (mkName "a") () ]
            (Just StarT)
            [ GadtC [(mkName "MkT")]
                    [ ( Bang NoSourceUnpackedness NoSourceStrictness
@@ -43,7 +43,7 @@ $( return
                    ]
                    (AppT (ConT (mkName "T"))
                          (VarT (mkName "a")))
-           , ForallC [PlainTV (mkName "a"), PlainTV (mkName "b")]
+           , ForallC [PlainTV (mkName "a") SpecifiedSpec, PlainTV (mkName "b") SpecifiedSpec]
                      [AppT (AppT EqualityT (VarT $ mkName "a"  ) )
                                            (ConT $ mkName "Int") ] $
              RecGadtC [(mkName "MkC")]
diff --git a/testsuite/tests/th/T10828a.hs b/testsuite/tests/th/T10828a.hs
index c3108c3e38..d66547bad7 100644
--- a/testsuite/tests/th/T10828a.hs
+++ b/testsuite/tests/th/T10828a.hs
@@ -8,7 +8,7 @@ import System.IO
 -- attempting to place a kind signature on a H98 data type
 $( return
    [ DataD [] (mkName "T")
-           [ PlainTV (mkName "a") ]
+           [ PlainTV (mkName "a") () ]
            (Just StarT)
            [ NormalC (mkName "MkT")
                    [ ( Bang NoSourceUnpackedness NoSourceStrictness
diff --git a/testsuite/tests/th/T10828b.hs b/testsuite/tests/th/T10828b.hs
index 1db3b0840c..03706d6b7c 100644
--- a/testsuite/tests/th/T10828b.hs
+++ b/testsuite/tests/th/T10828b.hs
@@ -8,7 +8,7 @@ import System.IO
 -- attempting to mix GADT and normal constructors
 $( return
    [ DataD [] (mkName "T")
-           [ PlainTV (mkName "a") ]
+           [ PlainTV (mkName "a") () ]
            (Just StarT)
            [ NormalC
                (mkName "MkT")
@@ -19,7 +19,7 @@ $( return
                  , VarT (mkName "a")
                  )
                ]
-           , ForallC [PlainTV (mkName "a")]
+           , ForallC [PlainTV (mkName "a") SpecifiedSpec]
                      [AppT (AppT EqualityT (VarT $ mkName "a"  ) )
                                            (ConT $ mkName "Int") ] $
              RecGadtC
diff --git a/testsuite/tests/th/T10945.hs b/testsuite/tests/th/T10945.hs
index be7a792d61..d9a24663ab 100644
--- a/testsuite/tests/th/T10945.hs
+++ b/testsuite/tests/th/T10945.hs
@@ -6,7 +6,7 @@ import Language.Haskell.TH
 
 $$(return [
    SigD (mkName "m")
-        (ForallT [PlainTV (mkName "a")]
+        (ForallT [PlainTV (mkName "a") SpecifiedSpec]
                  []
                  (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a"))))
  , FunD (mkName "m")
diff --git a/testsuite/tests/th/T10945.stderr b/testsuite/tests/th/T10945.stderr
index 786a0befa5..765be1fa80 100644
--- a/testsuite/tests/th/T10945.stderr
+++ b/testsuite/tests/th/T10945.stderr
@@ -8,7 +8,7 @@ T10945.hs:7:4: error:
           [SigD
              (mkName "m")
              (ForallT
-                [PlainTV (mkName "a")] []
+                [PlainTV (mkName "a") SpecifiedSpec] []
                 (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
            FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]
       In the Template Haskell splice
@@ -16,7 +16,7 @@ T10945.hs:7:4: error:
              [SigD
                 (mkName "m")
                 (ForallT
-                   [PlainTV (mkName "a")] []
+                   [PlainTV (mkName "a") SpecifiedSpec] []
                    (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
               FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
       In the expression:
@@ -24,6 +24,6 @@ T10945.hs:7:4: error:
              [SigD
                 (mkName "m")
                 (ForallT
-                   [PlainTV (mkName "a")] []
+                   [PlainTV (mkName "a") SpecifiedSpec] []
                    (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
               FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) []]])
diff --git a/testsuite/tests/th/T11345.hs b/testsuite/tests/th/T11345.hs
index 39dd8adc08..2288cdad15 100644
--- a/testsuite/tests/th/T11345.hs
+++ b/testsuite/tests/th/T11345.hs
@@ -15,7 +15,7 @@ $(do gadtName   <- newName "GADT2"
      prefixName <- newName "Prefix2"
      infixName  <- newName ":****:"
      a          <- newName "a"
-     return [ DataD [] gadtName [KindedTV a StarT] Nothing
+     return [ DataD [] gadtName [KindedTV a () StarT] Nothing
               [ GadtC [prefixName]
                 [ (Bang NoSourceUnpackedness NoSourceStrictness,ConT ''Int)
                 , (Bang NoSourceUnpackedness NoSourceStrictness,ConT ''Int)
diff --git a/testsuite/tests/th/T11721_TH.hs b/testsuite/tests/th/T11721_TH.hs
index 979ff15b0d..b8e895c155 100644
--- a/testsuite/tests/th/T11721_TH.hs
+++ b/testsuite/tests/th/T11721_TH.hs
@@ -12,8 +12,8 @@ $(return [])
 
 main :: IO ()
 main = print
-  $(do let rightOrder :: [TyVarBndr] -> Bool
-           rightOrder [KindedTV b _, KindedTV a _]
+  $(do let rightOrder :: [TyVarBndr flag] -> Bool
+           rightOrder [KindedTV b _ _, KindedTV a _ _]
              = nameBase b == "b" && nameBase a == "a"
            rightOrder _ = False
 
diff --git a/testsuite/tests/th/T12503.hs b/testsuite/tests/th/T12503.hs
index 78175bcf04..d1e3f27a93 100644
--- a/testsuite/tests/th/T12503.hs
+++ b/testsuite/tests/th/T12503.hs
@@ -9,7 +9,7 @@ import Language.Haskell.TH
 data T1 k
 class C1 a
 
-$(do TyConI (DataD [] tName [ KindedTV kName kKind] _ _ _)
+$(do TyConI (DataD [] tName [ KindedTV kName () kKind] _ _ _)
        <- reify ''T1
      d <- instanceD (cxt [])
                     (conT ''C1 `appT`
diff --git a/testsuite/tests/th/T13098.hs b/testsuite/tests/th/T13098.hs
index 8df07d230d..e6a541cc55 100644
--- a/testsuite/tests/th/T13098.hs
+++ b/testsuite/tests/th/T13098.hs
@@ -6,7 +6,7 @@ module T13098 where
 
 import Language.Haskell.TH
 
-$( sequence [ dataD (cxt []) (mkName "T") [PlainTV (mkName "a")]
+$( sequence [ dataD (cxt []) (mkName "T") [PlainTV (mkName "a") ()]
                      Nothing [normalC (mkName "T") []] []
           , pragCompleteD [mkName "T"] Nothing ] )
 
diff --git a/testsuite/tests/th/T13782.hs b/testsuite/tests/th/T13782.hs
index 0346749ce4..b7af84e0e6 100644
--- a/testsuite/tests/th/T13782.hs
+++ b/testsuite/tests/th/T13782.hs
@@ -6,10 +6,10 @@ module T13782 where
 
 import Language.Haskell.TH
 
-$(do TyConI (DataD _ _ [KindedTV a1 _] _ _ _) <- reify ''Maybe
+$(do TyConI (DataD _ _ [KindedTV a1 _ _] _ _ _) <- reify ''Maybe
      [f,a2] <- mapM newName ["f","a"]
-     return [ SigD f (ForallT [PlainTV a1,
-                               KindedTV a2 (AppT (ConT ''Maybe) (VarT a1))]
+     return [ SigD f (ForallT [PlainTV a1 SpecifiedSpec,
+                               KindedTV a2 SpecifiedSpec (AppT (ConT ''Maybe) (VarT a1))]
                    [] (ConT ''Int))
             , ValD (VarP f) (NormalB (LitE (IntegerL 42))) []
             ])
diff --git a/testsuite/tests/th/T13885.hs b/testsuite/tests/th/T13885.hs
index cdcc37f426..42f74a623d 100644
--- a/testsuite/tests/th/T13885.hs
+++ b/testsuite/tests/th/T13885.hs
@@ -17,8 +17,8 @@ main = print
   $(do TyConI (DataD _ _ tycon_tyvars _
                      [ForallC con_tyvars _ _] _) <- reify ''(:~:)
 
-       let tvbName :: TyVarBndr -> Name
-           tvbName (PlainTV  n)   = n
-           tvbName (KindedTV n _) = n
+       let tvbName :: TyVarBndr flag -> Name
+           tvbName (PlainTV  n _)   = n
+           tvbName (KindedTV n _ _) = n
 
-       lift $ and $ zipWith ((/=) `on` tvbName) tycon_tyvars con_tyvars)
+       lift $ and $ zipWith (/=) (map tvbName tycon_tyvars) (map tvbName con_tyvars))
diff --git a/testsuite/tests/th/T16976.stderr b/testsuite/tests/th/T16976.stderr
index b711aa4de3..7fe46fb5eb 100644
--- a/testsuite/tests/th/T16976.stderr
+++ b/testsuite/tests/th/T16976.stderr
@@ -1,9 +1,9 @@
-T16976.aNumber :: forall (p_0 :: *) . GHC.Num.Num p_0 => p_0
+T16976.aNumber :: forall {p_0 :: *} . GHC.Num.Num p_0 => p_0
 T16976.aString :: [GHC.Types.Char]
 T16976.MkT1 :: forall (s_0 :: *) . T16976.T s_0
 T16976.MkT2 :: forall (s_0 :: *) . T16976.T s_0
 T16976.T :: * -> *
-T16976.P :: forall (s_0 :: *) . T16976.T s_0
+T16976.P :: forall {s_0 :: *} . T16976.T s_0
 GHC.Classes.not :: GHC.Types.Bool -> GHC.Types.Bool
 GHC.Base.id :: forall (a_0 :: *) . a_0 -> a_0
 GHC.Maybe.Nothing :: forall (a_0 :: *) . GHC.Maybe.Maybe a_0
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index 78ad520e46..d6f775fa37 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -31,7 +31,7 @@ T5358.hs:10:21: error:
 
 T5358.hs:14:12: error:
     • Exception when trying to run compile-time code:
-        runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
+        runTest called error: forall {t_0 :: *} . t_0 -> GHC.Types.Bool
 CallStack (from HasCallStack):
   error, called at T5358.hs:15:18 in main:T5358
       Code: (do VarI _ t _ <- reify (mkName "prop_x1")
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
index d0f448b80a..41e0b5e607 100644
--- a/testsuite/tests/th/T6018th.hs
+++ b/testsuite/tests/th/T6018th.hs
@@ -14,8 +14,8 @@ import Language.Haskell.TH
 $( return
    [ OpenTypeFamilyD (TypeFamilyHead
        (mkName "F")
-       [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
-       (TyVarSig (KindedTV (mkName "result") (VarT (mkName "k"))))
+       [ PlainTV (mkName "a") (), PlainTV (mkName "b") (), PlainTV (mkName "c") () ]
+       (TyVarSig (KindedTV (mkName "result") () (VarT (mkName "k"))))
        (Just $ InjectivityAnn (mkName "result")
                              [(mkName "a"), (mkName "b"), (mkName "c") ]))
    , TySynInstD
@@ -41,8 +41,8 @@ $( return
 $( return
    [ OpenTypeFamilyD (TypeFamilyHead
        (mkName "J")
-       [ PlainTV (mkName "a"), KindedTV (mkName "b") (VarT (mkName "k")) ]
-       (TyVarSig (PlainTV (mkName "r")))
+       [ PlainTV (mkName "a") (), KindedTV (mkName "b") () (VarT (mkName "k")) ]
+       (TyVarSig (PlainTV (mkName "r") ()))
        (Just $ InjectivityAnn (mkName "r") [mkName "a"]))
    , TySynInstD
        (TySynEqn Nothing (AppT (AppT (ConT (mkName "J")) (ConT (mkName "Int")))
@@ -60,9 +60,9 @@ $( return
 $( return
    [ ClosedTypeFamilyD (TypeFamilyHead
        (mkName "I")
-       [ KindedTV (mkName "a") StarT, KindedTV (mkName "b") StarT
-       , KindedTV (mkName "c") StarT ]
-       (TyVarSig (PlainTV (mkName "r")))
+       [ KindedTV (mkName "a") () StarT, KindedTV (mkName "b") () StarT
+       , KindedTV (mkName "c") () StarT ]
+       (TyVarSig (PlainTV (mkName "r") ()))
        (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")]))
 
        [ TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "I")) (ConT (mkName "Int")))
@@ -98,8 +98,8 @@ $( do { decl@([ClosedTypeFamilyD (TypeFamilyHead _ _ _ (Just inj)) _]) <-
 $( return
    [ OpenTypeFamilyD (TypeFamilyHead
        (mkName "H")
-       [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
-       (TyVarSig (PlainTV (mkName "r")))
+       [ PlainTV (mkName "a") (), PlainTV (mkName "b") (), PlainTV (mkName "c") () ]
+       (TyVarSig (PlainTV (mkName "r") ()))
        (Just $ InjectivityAnn (mkName "r")
                              [(mkName "a"), (mkName "b") ]))
 
diff --git a/testsuite/tests/th/T7667.hs b/testsuite/tests/th/T7667.hs
index 59287f1448..eef6fd2cb0 100644
--- a/testsuite/tests/th/T7667.hs
+++ b/testsuite/tests/th/T7667.hs
@@ -4,5 +4,5 @@ module T7667 where
 
 import Language.Haskell.TH
 
-$( return [ TySynD (mkName "+") [PlainTV (mkName "a"), PlainTV (mkName "b")]
-                   (AppT (AppT (ConT ''Either) (VarT $ mkName "a")) (VarT $ mkName "b")) ] )
\ No newline at end of file
+$( return [ TySynD (mkName "+") [PlainTV (mkName "a") (), PlainTV (mkName "b") ()]
+                   (AppT (AppT (ConT ''Either) (VarT $ mkName "a")) (VarT $ mkName "b")) ] )
diff --git a/testsuite/tests/th/T8499.hs b/testsuite/tests/th/T8499.hs
index 29b9e1678c..d9278b4113 100644
--- a/testsuite/tests/th/T8499.hs
+++ b/testsuite/tests/th/T8499.hs
@@ -5,8 +5,8 @@ module T8499 where
 
 import Language.Haskell.TH
 
-$( do TyConI (DataD _ _ [KindedTV tvb_a _] _ _ _) <- reify ''Maybe
+$( do TyConI (DataD _ _ [KindedTV tvb_a _ _] _ _ _) <- reify ''Maybe
       my_a <- newName "a"
       return [TySynD (mkName "SMaybe")
-                     [KindedTV my_a (AppT (ConT ''Maybe) (VarT tvb_a))]
+                     [KindedTV my_a () (AppT (ConT ''Maybe) (VarT tvb_a))]
                      (TupleT 0)] )
diff --git a/testsuite/tests/th/TH_RichKinds2.hs b/testsuite/tests/th/TH_RichKinds2.hs
index 5cdf919f91..00387c7b4c 100644
--- a/testsuite/tests/th/TH_RichKinds2.hs
+++ b/testsuite/tests/th/TH_RichKinds2.hs
@@ -14,10 +14,10 @@ import Data.List (splitAt, span, elemIndex)
 import Language.Haskell.TH
 
 $(return [OpenTypeFamilyD (TypeFamilyHead
-          (mkName "Map") [KindedTV (mkName "f")
+          (mkName "Map") [KindedTV (mkName "f") ()
                           (AppT (AppT ArrowT (VarT (mkName "k1")))
                            (VarT (mkName "k2"))),
-                          KindedTV (mkName "l")
+                          KindedTV (mkName "l") ()
                           (AppT ListT
                            (VarT (mkName "k1")))]
           (KindSig (AppT ListT (VarT (mkName "k2")))) Nothing)])
diff --git a/testsuite/tests/th/TH_Roles1.hs b/testsuite/tests/th/TH_Roles1.hs
index 89d072c485..6ac6128885 100644
--- a/testsuite/tests/th/TH_Roles1.hs
+++ b/testsuite/tests/th/TH_Roles1.hs
@@ -4,6 +4,6 @@ module TH_Roles1 where
 
 import Language.Haskell.TH
 
-$( return [ DataD [] (mkName "T") [PlainTV (mkName "a")] Nothing [] []
+$( return [ DataD [] (mkName "T") [PlainTV (mkName "a") ()] Nothing [] []
           , RoleAnnotD (mkName "T") [RepresentationalR] ] )
 
diff --git a/testsuite/tests/th/TH_Roles2.hs b/testsuite/tests/th/TH_Roles2.hs
index 3f7b535b49..e6a0df0c52 100644
--- a/testsuite/tests/th/TH_Roles2.hs
+++ b/testsuite/tests/th/TH_Roles2.hs
@@ -4,7 +4,7 @@ module TH_Roles2 where
 
 import Language.Haskell.TH
 
-$( return [ DataD [] (mkName "T") [KindedTV (mkName "a") (VarT (mkName "k"))]
+$( return [ DataD [] (mkName "T") [KindedTV (mkName "a") () (VarT (mkName "k"))]
             Nothing [] []
           , RoleAnnotD (mkName "T") [RepresentationalR] ] )
 
diff --git a/testsuite/tests/th/TH_genExLib.hs b/testsuite/tests/th/TH_genExLib.hs
index d8b646ac90..c0f8bad8e6 100644
--- a/testsuite/tests/th/TH_genExLib.hs
+++ b/testsuite/tests/th/TH_genExLib.hs
@@ -15,7 +15,7 @@ genAnyClass name decls
   = DataD [] anyName [] Nothing [constructor] []
   where
     anyName = mkName ("Any" ++ nameBase name ++ "1111")
-    constructor = ForallC [PlainTV var_a] [AppT (ConT name) (VarT var_a)] $
+    constructor = ForallC [PlainTV var_a SpecifiedSpec] [AppT (ConT name) (VarT var_a)] $
                   NormalC anyName
                                 [(Bang NoSourceUnpackedness NoSourceStrictness, VarT var_a)]
     var_a = mkName "a"
diff --git a/testsuite/tests/th/TH_reifyDecl1.stderr b/testsuite/tests/th/TH_reifyDecl1.stderr
index 5ae01471f3..1984d85075 100644
--- a/testsuite/tests/th/TH_reifyDecl1.stderr
+++ b/testsuite/tests/th/TH_reifyDecl1.stderr
@@ -9,7 +9,7 @@ data TH_reifyDecl1.Tree (a_0 :: k_1)
     | (TH_reifyDecl1.Tree a_0) TH_reifyDecl1.:+: (TH_reifyDecl1.Tree a_0)
 type TH_reifyDecl1.IntList = [GHC.Types.Int]
 newtype TH_reifyDecl1.Length = TH_reifyDecl1.Length GHC.Types.Int
-Constructor from TH_reifyDecl1.Tree: TH_reifyDecl1.Leaf :: forall (k_0 :: *) (a_1 :: k_0) .
+Constructor from TH_reifyDecl1.Tree: TH_reifyDecl1.Leaf :: forall {k_0 :: *} (a_1 :: k_0) .
                                                            TH_reifyDecl1.Tree a_1
 Class op from TH_reifyDecl1.C1: TH_reifyDecl1.m1 :: forall (a_0 :: *) . TH_reifyDecl1.C1 a_0 =>
                                                     a_0 -> GHC.Types.Int
diff --git a/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA1.hs b/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA1.hs
new file mode 100644
index 0000000000..3da70ee59b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA1.hs
@@ -0,0 +1,108 @@
+{-# LANGUAGE RankNTypes
+           , PolyKinds
+           , GADTs
+           , TypeApplications
+           , PatternSynonyms
+           , ExistentialQuantification
+           , StandaloneKindSignatures
+           , DataKinds
+           , ExistentialQuantification
+#-}
+
+module ExplicitSpecificityA1 where
+
+import Data.Proxy
+import Data.Kind
+
+-- Type variables bound in RULES
+{-# RULES "parametricity" forall (f :: forall {a}. a -> a). map f = id #-}
+
+-- Type signatures
+foo1 :: a -> a
+foo1 x = x
+
+foo2 :: forall a. a -> a
+foo2 x = x
+
+foo3 :: forall {a}. a -> a
+foo3 x = x
+
+foo4 :: forall a {b}. a -> b -> b
+foo4 _ x = x
+
+foo5 :: forall {a} b. a -> b -> b
+foo5 _ x = x
+
+bar1 :: ()
+bar1 = let { x1 = foo1 42
+           ; x2 = foo2 @Int 42
+           ; x3 = foo3 42
+           ; x4 = foo4 @Bool True 42
+           ; x5 = foo5 @Int True 42
+           }
+       in ()
+
+-- Data declarations
+data T1 a = C1 a
+
+data T2 (a :: k) = C2 { f2 :: Proxy a }
+
+data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a
+
+data T4 a where C4 :: forall {k} (a::k). Proxy a -> T4 a
+
+data T5 k (a :: k) where C5 :: forall k (a::k). Proxy a -> T5 k a
+
+data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a
+
+bar2 :: ()
+bar2 = let { x1 = C1 @Int 42
+           ; x2 = C2 @Type @Int Proxy
+           ; x3 = C3 @Type @Int Proxy
+           ; x4 = C4 @Int Proxy
+           ; x5 = C5 @Type @Int Proxy
+           ; x6 = C6 @Int Proxy
+           }
+       in ()
+
+-- Pattern synonyms
+data T7 a where C7 :: forall a b. a -> b -> T7 a
+
+data T8 a where C8 :: forall a {b}. a -> b -> T8 a
+
+pattern Pat1 :: forall a. () => forall b. a -> b -> T7 a
+pattern Pat1 x y = C7 x y
+
+pattern Pat2 :: forall {a}. () => forall b. a -> b -> T7 a
+pattern Pat2 x y = C7 x y
+
+pattern Pat3 :: forall a. () => forall b. a -> b -> T8 a
+pattern Pat3 x y = C8 x y
+
+pattern Pat4 :: forall {a}. () => forall b. a -> b -> T8 a
+pattern Pat4 x y = C8 x y
+
+pattern Pat5 :: forall {a}. () => forall {b}. a -> b -> T7 a
+pattern Pat5 x y = C7 x y
+
+bar3 :: (T7 a) -> ()
+bar3 (Pat1 x y) = ()
+bar3 (Pat2 x y) = ()
+
+bar4 :: (T8 a) -> ()
+bar4 (Pat3 x y) = ()
+bar4 (Pat4 x y) = ()
+
+-- Existential variable quantification
+data HList = HNil
+           | forall {a}. HCons a HList
+
+-- Type synonyms
+type TySy = forall a {b}. Either a b
+
+-- Standalone kind signatures
+type Foo :: forall a {b}. a -> b -> b
+type Foo x y = y
+
+type Bar = Foo @Bool True 42
+
diff --git a/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA2.hs b/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA2.hs
new file mode 100644
index 0000000000..afac6c4725
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/ExplicitSpecificityA2.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+
+module ExplicitSpecificityA2 where
+
+class C a where
+
+-- D :: forall {k}. k -> *
+data D a where
+  K :: D a
+
+-- While the type of D abstracts over an implicit (inferred) variable `k`,
+-- this instance should not be rejected for implicitly including an inferred
+-- type variable, as it is not user written.
+instance C (D a) where
+
+
diff --git a/testsuite/tests/typecheck/should_compile/T18023.hs b/testsuite/tests/typecheck/should_compile/T18023.hs
index 4bc5c6eede..9961c95b24 100644
--- a/testsuite/tests/typecheck/should_compile/T18023.hs
+++ b/testsuite/tests/typecheck/should_compile/T18023.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 module T18023 where
 
 import Data.Kind
@@ -32,3 +34,12 @@ toP2True = MkP2 @True @True
 
 fromP2True :: P2 True True -> (Proxy True, Proxy True)
 fromP2True = unP2 @True @True
+
+type    P3 :: forall {k}. k -> Type
+newtype P3 a = MkP3 { unP3 :: Proxy a }
+
+toP3True :: Proxy True -> P3 True
+toP3True = MkP3 @True
+
+fromP3True :: P3 True -> Proxy True
+fromP3True = unP3 @True
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 56eecc0374..c4028d6e25 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -707,3 +707,5 @@ test('T18036', normal, compile, [''])
 test('T18036a', normal, compile, [''])
 test('T17873', normal, compile, [''])
 test('T18129', expect_broken(18129), compile, [''])
+test('ExplicitSpecificityA1', normal, compile, [''])
+test('ExplicitSpecificityA2', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.hs
new file mode 100644
index 0000000000..4fddd91272
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeApplications, RankNTypes #-}
+
+module ExplicitSpecificity1 where
+
+foo :: forall {a}. a -> a
+foo x = x
+
+bar :: ()
+bar = let x = foo @Int 42
+      in ()
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.stderr
new file mode 100644
index 0000000000..dd5b456230
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity1.stderr
@@ -0,0 +1,7 @@
+
+ExplicitSpecificity1.hs:9:15: error:
+    • Cannot apply expression of type ‘a0 -> a0’
+      to a visible type argument ‘Int’
+    • In the expression: foo @Int 42
+      In an equation for ‘x’: x = foo @Int 42
+      In the expression: let x = foo @Int 42 in ()
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.hs
new file mode 100644
index 0000000000..0f763b0a27
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeApplications, RankNTypes #-}
+
+module ExplicitSpecificity10 where
+
+newtype T = MkT { unT :: forall {a}. a -> a }
+
+test :: T -> Bool -> Bool
+test t = unT t @Bool
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.stderr
new file mode 100644
index 0000000000..0929129d5e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity10.stderr
@@ -0,0 +1,6 @@
+
+ExplicitSpecificity10.hs:8:10: error:
+    • Cannot apply expression of type ‘a0 -> a0’
+      to a visible type argument ‘Bool’
+    • In the expression: unT t @Bool
+      In an equation for ‘test’: test t = unT t @Bool
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.hs
new file mode 100644
index 0000000000..ec319e74f4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications, RankNTypes, GADTs, PolyKinds #-}
+
+module ExplicitSpecificity2 where
+
+import Data.Proxy
+import Data.Kind
+
+data T a where C :: forall {k} (a::k). Proxy a -> T a
+
+bar :: ()
+bar = let x = C @Type @Int Proxy
+      in ()
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.stderr
new file mode 100644
index 0000000000..8c43169157
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity2.stderr
@@ -0,0 +1,7 @@
+
+ExplicitSpecificity2.hs:11:15: error:
+    • Cannot apply expression of type ‘Proxy (*) -> T (*)’
+      to a visible type argument ‘Int’
+    • In the expression: C @Type @Int Proxy
+      In an equation for ‘x’: x = C @Type @Int Proxy
+      In the expression: let x = C @Type @Int Proxy in ()
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.hs
new file mode 100644
index 0000000000..7f8144a2a8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes, PolyKinds, TypeFamilies #-}
+
+module ExplicitSpecificity3 where
+
+type family F {k} (a::k) :: *
+type instance F String = Int
+
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.stderr
new file mode 100644
index 0000000000..751fbefa73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity3.stderr
@@ -0,0 +1,2 @@
+
+ExplicitSpecificity3.hs:5:17: error: parse error on input ‘}’
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs
new file mode 100644
index 0000000000..4d615631b6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module ExplicitSpecificity4 where
+
+class C a where
+  f         :: forall {z}. z -> a -> a
+  default f :: forall {z}. z -> a -> a
+  f _ x = x
+
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.stderr
new file mode 100644
index 0000000000..95a3286ce4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.stderr
@@ -0,0 +1,4 @@
+
+ExplicitSpecificity4.hs:8:3: error:
+    A default type signature cannot contain inferred type variables
+    In a class method signature for ‘f’
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.hs
new file mode 100644
index 0000000000..2788f952fe
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module ExplicitSpecificity5 where
+
+class C a where
+
+instance forall {a} {b}. C (Either a b) where
+
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.stderr
new file mode 100644
index 0000000000..c8fa860a57
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity5.stderr
@@ -0,0 +1,4 @@
+
+ExplicitSpecificity5.hs:7:1: error:
+    Inferred type variables are not allowed
+    In an instance declaration
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.hs
new file mode 100644
index 0000000000..88508071b8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module ExplicitSpecificity6 where
+
+class C a where
+
+instance forall {a} {b}. C (Either a b) where
+  {-# SPECIALISE instance forall {a}. C (Either a Int) #-}
+
+
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.stderr
new file mode 100644
index 0000000000..326c9b2ae9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity6.stderr
@@ -0,0 +1,8 @@
+
+ExplicitSpecificity6.hs:8:1: error:
+    Inferred type variables are not allowed
+    In an instance declaration
+
+ExplicitSpecificity6.hs:9:3: error:
+    Inferred type variables are not allowed
+    In a SPECIALISE instance pragma
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.hs
new file mode 100644
index 0000000000..c5b58cd758
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RankNTypes, StandaloneKindSignatures, DataKinds, PolyKinds, TypeApplications #-}
+
+module ExplicitSpecificity7 where
+
+type Foo :: forall a {b}. a -> b -> b
+type Foo x y = y
+
+type Bar = Foo @Bool @Int True 42
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.stderr
new file mode 100644
index 0000000000..2d98e47867
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity7.stderr
@@ -0,0 +1,6 @@
+
+ExplicitSpecificity7.hs:8:12: error:
+    • Cannot apply function of kind ‘Bool -> b0 -> b0’
+      to visible kind argument ‘Int’
+    • In the type ‘Foo @Bool @Int True 42’
+      In the type declaration for ‘Bar’
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.hs
new file mode 100644
index 0000000000..819a060d42
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes, PolyKinds, GADTs #-}
+
+module ExplicitSpecificity8 where
+
+import GHC.Types
+
+data T1 :: forall k -> k -> Type
+
+data T2 :: forall {k} -> k -> Type
+
+foo1 :: T1 Type Int -> ()
+foo1 _ = ()
+
+foo2 :: T2 Type Int -> ()
+foo2 _ = ()
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.stderr
new file mode 100644
index 0000000000..dcb79191d7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity8.stderr
@@ -0,0 +1,6 @@
+
+ExplicitSpecificity8.hs:9:12: error:
+    • Unexpected inferred variable in visible forall binder:
+        forall {k} -> k -> Type
+    • In the kind ‘forall {k} -> k -> Type’
+      In the data type declaration for ‘T2’
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.hs b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.hs
new file mode 100644
index 0000000000..829e771e46
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module Bug where
+
+data T a = MkT
+deriving instance forall {a}. Show (T a)
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.stderr b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.stderr
new file mode 100644
index 0000000000..59bb56cf66
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/ExplicitSpecificity9.stderr
@@ -0,0 +1,4 @@
+
+ExplicitSpecificity9.hs:6:1: error:
+    Inferred type variables are not allowed
+    In a deriving declaration
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 8735cead75..d97c6f96e1 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -564,3 +564,13 @@ test('T17021b', normal, compile_fail, [''])
 test('T17955', normal, compile_fail, [''])
 test('T17173', normal, compile_fail, [''])
 test('T18127a', normal, compile_fail, [''])
+test('ExplicitSpecificity1', normal, compile_fail, [''])
+test('ExplicitSpecificity2', normal, compile_fail, [''])
+test('ExplicitSpecificity3', normal, compile_fail, [''])
+test('ExplicitSpecificity4', normal, compile_fail, [''])
+test('ExplicitSpecificity5', normal, compile_fail, [''])
+test('ExplicitSpecificity6', normal, compile_fail, [''])
+test('ExplicitSpecificity7', normal, compile_fail, [''])
+test('ExplicitSpecificity8', normal, compile_fail, [''])
+test('ExplicitSpecificity9', normal, compile_fail, [''])
+test('ExplicitSpecificity10', normal, compile_fail, [''])