Visible kind application

Summary:
This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
application, just like in term-level.

There are a few remaining issues with this patch, as documented in
ticket #16082.

Includes a submodule update for Haddock.

Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a

Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack

Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter

GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`

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

111 files changed, 2039 insertions, 595 deletions

diff --git a/testsuite/tests/dependent/should_compile/T11241.stderr b/testsuite/tests/dependent/should_compile/T11241.stderr
index 97b2a33cf2..adb78694ba 100644
--- a/testsuite/tests/dependent/should_compile/T11241.stderr
+++ b/testsuite/tests/dependent/should_compile/T11241.stderr
@@ -1,4 +1,5 @@
 
 T11241.hs:5:21: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘*’
-    • In the type signature: foo :: forall (a :: _). a -> a
+    • In the kind ‘_’
+      In the type signature: foo :: forall (a :: _). a -> a
diff --git a/testsuite/tests/deriving/should_compile/T14579a.hs b/testsuite/tests/deriving/should_compile/T14579a.hs
new file mode 100644
index 0000000000..ac7ba6cca8
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14579a.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Bug where
+
+import Data.Coerce
+import Data.Kind
+import Data.Proxy
+
+newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
+  deriving Eq
+
+newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))
+
+instance Eq a => Eq (Glurp a) where
+  (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool)
+                @(Glurp a         -> Glurp a         -> Bool)
+                (==)
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index c49b808860..8c84bcc31a 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -105,6 +105,7 @@ test('T14339', normal, compile, [''])
 test('T14331', normal, compile, [''])
 test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14579', normal, compile, [''])
+test('T14579a', normal, compile, [''])
 test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14883', normal, compile, [''])
 test('T14932', normal, compile, [''])
diff --git a/testsuite/tests/ghci/scripts/T12447.stdout b/testsuite/tests/ghci/scripts/T12447.stdout
index 6c469eeef3..7a64e1546d 100644
--- a/testsuite/tests/ghci/scripts/T12447.stdout
+++ b/testsuite/tests/ghci/scripts/T12447.stdout
@@ -1,3 +1,3 @@
 deferEither @(_ ~ _)
-  :: (Typeable w1, Typeable w2) =>
-     proxy (w1 ~ w2) -> ((w1 ~ w2) => r) -> Either String r
+  :: (Typeable _1, Typeable _2) =>
+     proxy (_1 ~ _2) -> ((_1 ~ _2) => r) -> Either String r
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
index e7065cf3b4..ca0e33c5ff 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
@@ -57,18 +57,6 @@ ExplicitForAllFams4b.hs:23:17: error:
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:23:20: error:
-    Conflicting family instance declarations:
-      CT [a] (a, a) = Float -- Defined at ExplicitForAllFams4b.hs:23:20
-      CT _ _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:24:20
-
-ExplicitForAllFams4b.hs:24:3: error:
-    • Type indexes must match class instance head
-      Expected: CT Int _
-        Actual: CT _ _
-    • In the type instance declaration for ‘CT’
-      In the instance declaration for ‘C Int’
-
 ExplicitForAllFams4b.hs:24:15: error:
     • Type variable ‘b’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
@@ -88,18 +76,6 @@ ExplicitForAllFams4b.hs:26:17: error:
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:26:20: error:
-    Conflicting family instance declarations:
-      CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20
-      CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20
-
-ExplicitForAllFams4b.hs:27:3: error:
-    • Type indexes must match class instance head
-      Expected: CD Int _
-        Actual: CD _ _
-    • In the data instance declaration for ‘CD’
-      In the instance declaration for ‘C Int’
-
 ExplicitForAllFams4b.hs:27:15: error:
     • Type variable ‘b’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.hs b/testsuite/tests/parser/should_compile/DumpParsedAst.hs
index 0f83b12f65..f2bf433324 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.hs
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.hs
@@ -1,6 +1,8 @@
-{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies
+             , TypeApplications, TypeInType #-}
 
 module DumpParsedAst where
+import Data.Kind
 
 data Peano = Zero | Succ Peano
 
@@ -8,4 +10,10 @@ type family Length (as :: [k]) :: Peano where
   Length (a : as) = Succ (Length as)
   Length '[]      = Zero
 
+-- vis kind app
+data T f (a :: k) = MkT (f a)
+
+type family F1 (a :: k) (f :: k -> Type) :: Type where
+  F1 @Peano a f = T @Peano f a
+
 main = putStrLn "hello"
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index 408f28b4f7..81607d729e 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -4,16 +4,28 @@
 ({ DumpParsedAst.hs:1:1 }
  (HsModule
   (Just
-   ({ DumpParsedAst.hs:3:8-20 }
+   ({ DumpParsedAst.hs:4:8-20 }
     {ModuleName: DumpParsedAst}))
   (Nothing)
-  []
-  [({ DumpParsedAst.hs:5:1-30 }
+  [({ DumpParsedAst.hs:5:1-16 }
+    (ImportDecl
+     (NoExt)
+     (NoSourceText)
+     ({ DumpParsedAst.hs:5:8-16 }
+      {ModuleName: Data.Kind})
+     (Nothing)
+     (False)
+     (False)
+     (False)
+     (False)
+     (Nothing)
+     (Nothing)))]
+  [({ DumpParsedAst.hs:7:1-30 }
     (TyClD
      (NoExt)
      (DataDecl
       (NoExt)
-      ({ DumpParsedAst.hs:5:6-10 }
+      ({ DumpParsedAst.hs:7:6-10 }
        (Unqual
         {OccName: Peano}))
       (HsQTvs
@@ -27,10 +39,10 @@
         [])
        (Nothing)
        (Nothing)
-       [({ DumpParsedAst.hs:5:14-17 }
+       [({ DumpParsedAst.hs:7:14-17 }
          (ConDeclH98
           (NoExt)
-          ({ DumpParsedAst.hs:5:14-17 }
+          ({ DumpParsedAst.hs:7:14-17 }
            (Unqual
             {OccName: Zero}))
           ({ <no location info> }
@@ -40,10 +52,10 @@
           (PrefixCon
            [])
           (Nothing)))
-       ,({ DumpParsedAst.hs:5:21-30 }
+       ,({ DumpParsedAst.hs:7:21-30 }
          (ConDeclH98
           (NoExt)
-          ({ DumpParsedAst.hs:5:21-24 }
+          ({ DumpParsedAst.hs:7:21-24 }
            (Unqual
             {OccName: Succ}))
           ({ <no location info> }
@@ -51,17 +63,17 @@
           []
           (Nothing)
           (PrefixCon
-           [({ DumpParsedAst.hs:5:26-30 }
+           [({ DumpParsedAst.hs:7:26-30 }
              (HsTyVar
               (NoExt)
               (NotPromoted)
-              ({ DumpParsedAst.hs:5:26-30 }
+              ({ DumpParsedAst.hs:7:26-30 }
                (Unqual
                 {OccName: Peano}))))])
           (Nothing)))]
        ({ <no location info> }
         [])))))
-  ,({ DumpParsedAst.hs:7:1-39 }
+  ,({ DumpParsedAst.hs:9:1-39 }
     (TyClD
      (NoExt)
      (FamDecl
@@ -70,140 +82,346 @@
        (NoExt)
        (ClosedTypeFamily
         (Just
-         [({ DumpParsedAst.hs:8:3-36 }
+         [({ DumpParsedAst.hs:10:3-36 }
            (HsIB
             (NoExt)
             (FamEqn
              (NoExt)
-             ({ DumpParsedAst.hs:8:3-8 }
+             ({ DumpParsedAst.hs:10:3-8 }
               (Unqual
                {OccName: Length}))
              (Nothing)
-             [({ DumpParsedAst.hs:8:10-17 }
-               (HsParTy
-                (NoExt)
-                ({ DumpParsedAst.hs:8:11-16 }
-                 (HsOpTy
-                  (NoExt)
-                  ({ DumpParsedAst.hs:8:11 }
-                   (HsTyVar
-                    (NoExt)
-                    (NotPromoted)
-                    ({ DumpParsedAst.hs:8:11 }
-                     (Unqual
-                      {OccName: a}))))
-                  ({ DumpParsedAst.hs:8:13 }
-                   (Exact
-                    {Name: :}))
-                  ({ DumpParsedAst.hs:8:15-16 }
-                   (HsTyVar
-                    (NoExt)
-                    (NotPromoted)
-                    ({ DumpParsedAst.hs:8:15-16 }
-                     (Unqual
-                      {OccName: as}))))))))]
+             [(HsValArg
+               ({ DumpParsedAst.hs:10:10-17 }
+                (HsParTy
+                 (NoExt)
+                 ({ DumpParsedAst.hs:10:11-16 }
+                  (HsOpTy
+                   (NoExt)
+                   ({ DumpParsedAst.hs:10:11 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpParsedAst.hs:10:11 }
+                      (Unqual
+                       {OccName: a}))))
+                   ({ DumpParsedAst.hs:10:13 }
+                    (Exact
+                     {Name: :}))
+                   ({ DumpParsedAst.hs:10:15-16 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpParsedAst.hs:10:15-16 }
+                      (Unqual
+                       {OccName: as})))))))))]
              (Prefix)
-             ({ DumpParsedAst.hs:8:21-36 }
+             ({ DumpParsedAst.hs:10:21-36 }
               (HsAppTy
                (NoExt)
-               ({ DumpParsedAst.hs:8:21-24 }
+               ({ DumpParsedAst.hs:10:21-24 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpParsedAst.hs:8:21-24 }
+                 ({ DumpParsedAst.hs:10:21-24 }
                   (Unqual
                    {OccName: Succ}))))
-               ({ DumpParsedAst.hs:8:26-36 }
+               ({ DumpParsedAst.hs:10:26-36 }
                 (HsParTy
                  (NoExt)
-                 ({ DumpParsedAst.hs:8:27-35 }
+                 ({ DumpParsedAst.hs:10:27-35 }
                   (HsAppTy
                    (NoExt)
-                   ({ DumpParsedAst.hs:8:27-32 }
+                   ({ DumpParsedAst.hs:10:27-32 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpParsedAst.hs:8:27-32 }
+                     ({ DumpParsedAst.hs:10:27-32 }
                       (Unqual
                        {OccName: Length}))))
-                   ({ DumpParsedAst.hs:8:34-35 }
+                   ({ DumpParsedAst.hs:10:34-35 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpParsedAst.hs:8:34-35 }
+                     ({ DumpParsedAst.hs:10:34-35 }
                       (Unqual
                        {OccName: as})))))))))))))
-         ,({ DumpParsedAst.hs:9:3-24 }
+         ,({ DumpParsedAst.hs:11:3-24 }
            (HsIB
             (NoExt)
             (FamEqn
              (NoExt)
-             ({ DumpParsedAst.hs:9:3-8 }
+             ({ DumpParsedAst.hs:11:3-8 }
               (Unqual
                {OccName: Length}))
              (Nothing)
-             [({ DumpParsedAst.hs:9:10-12 }
-               (HsExplicitListTy
-                (NoExt)
-                (IsPromoted)
-                []))]
+             [(HsValArg
+               ({ DumpParsedAst.hs:11:10-12 }
+                (HsExplicitListTy
+                 (NoExt)
+                 (IsPromoted)
+                 [])))]
              (Prefix)
-             ({ DumpParsedAst.hs:9:21-24 }
+             ({ DumpParsedAst.hs:11:21-24 }
               (HsTyVar
                (NoExt)
                (NotPromoted)
-               ({ DumpParsedAst.hs:9:21-24 }
+               ({ DumpParsedAst.hs:11:21-24 }
                 (Unqual
                  {OccName: Zero})))))))]))
-       ({ DumpParsedAst.hs:7:13-18 }
+       ({ DumpParsedAst.hs:9:13-18 }
         (Unqual
          {OccName: Length}))
        (HsQTvs
         (NoExt)
-        [({ DumpParsedAst.hs:7:21-29 }
+        [({ DumpParsedAst.hs:9:21-29 }
           (KindedTyVar
            (NoExt)
-           ({ DumpParsedAst.hs:7:21-22 }
+           ({ DumpParsedAst.hs:9:21-22 }
             (Unqual
              {OccName: as}))
-           ({ DumpParsedAst.hs:7:27-29 }
+           ({ DumpParsedAst.hs:9:27-29 }
             (HsListTy
              (NoExt)
-             ({ DumpParsedAst.hs:7:28 }
+             ({ DumpParsedAst.hs:9:28 }
               (HsTyVar
                (NoExt)
                (NotPromoted)
-               ({ DumpParsedAst.hs:7:28 }
+               ({ DumpParsedAst.hs:9:28 }
                 (Unqual
                  {OccName: k}))))))))])
        (Prefix)
-       ({ DumpParsedAst.hs:7:32-39 }
+       ({ DumpParsedAst.hs:9:32-39 }
         (KindSig
          (NoExt)
-         ({ DumpParsedAst.hs:7:35-39 }
+         ({ DumpParsedAst.hs:9:35-39 }
           (HsTyVar
            (NoExt)
            (NotPromoted)
-           ({ DumpParsedAst.hs:7:35-39 }
+           ({ DumpParsedAst.hs:9:35-39 }
             (Unqual
              {OccName: Peano}))))))
        (Nothing)))))
-  ,({ DumpParsedAst.hs:11:1-23 }
+  ,({ DumpParsedAst.hs:14:1-29 }
+    (TyClD
+     (NoExt)
+     (DataDecl
+      (NoExt)
+      ({ DumpParsedAst.hs:14:6 }
+       (Unqual
+        {OccName: T}))
+      (HsQTvs
+       (NoExt)
+       [({ DumpParsedAst.hs:14:8 }
+         (UserTyVar
+          (NoExt)
+          ({ DumpParsedAst.hs:14:8 }
+           (Unqual
+            {OccName: f}))))
+       ,({ DumpParsedAst.hs:14:11-16 }
+         (KindedTyVar
+          (NoExt)
+          ({ DumpParsedAst.hs:14:11 }
+           (Unqual
+            {OccName: a}))
+          ({ DumpParsedAst.hs:14:16 }
+           (HsTyVar
+            (NoExt)
+            (NotPromoted)
+            ({ DumpParsedAst.hs:14:16 }
+             (Unqual
+              {OccName: k}))))))])
+      (Prefix)
+      (HsDataDefn
+       (NoExt)
+       (DataType)
+       ({ <no location info> }
+        [])
+       (Nothing)
+       (Nothing)
+       [({ DumpParsedAst.hs:14:21-29 }
+         (ConDeclH98
+          (NoExt)
+          ({ DumpParsedAst.hs:14:21-23 }
+           (Unqual
+            {OccName: MkT}))
+          ({ <no location info> }
+           (False))
+          []
+          (Nothing)
+          (PrefixCon
+           [({ DumpParsedAst.hs:14:25-29 }
+             (HsParTy
+              (NoExt)
+              ({ DumpParsedAst.hs:14:26-28 }
+               (HsAppTy
+                (NoExt)
+                ({ DumpParsedAst.hs:14:26 }
+                 (HsTyVar
+                  (NoExt)
+                  (NotPromoted)
+                  ({ DumpParsedAst.hs:14:26 }
+                   (Unqual
+                    {OccName: f}))))
+                ({ DumpParsedAst.hs:14:28 }
+                 (HsTyVar
+                  (NoExt)
+                  (NotPromoted)
+                  ({ DumpParsedAst.hs:14:28 }
+                   (Unqual
+                    {OccName: a}))))))))])
+          (Nothing)))]
+       ({ <no location info> }
+        [])))))
+  ,({ DumpParsedAst.hs:16:1-48 }
+    (TyClD
+     (NoExt)
+     (FamDecl
+      (NoExt)
+      (FamilyDecl
+       (NoExt)
+       (ClosedTypeFamily
+        (Just
+         [({ DumpParsedAst.hs:17:3-30 }
+           (HsIB
+            (NoExt)
+            (FamEqn
+             (NoExt)
+             ({ DumpParsedAst.hs:17:3-4 }
+              (Unqual
+               {OccName: F1}))
+             (Nothing)
+             [(HsTypeArg
+               ({ DumpParsedAst.hs:17:7-11 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpParsedAst.hs:17:7-11 }
+                  (Unqual
+                   {OccName: Peano})))))
+             ,(HsValArg
+               ({ DumpParsedAst.hs:17:13 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpParsedAst.hs:17:13 }
+                  (Unqual
+                   {OccName: a})))))
+             ,(HsValArg
+               ({ DumpParsedAst.hs:17:15 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpParsedAst.hs:17:15 }
+                  (Unqual
+                   {OccName: f})))))]
+             (Prefix)
+             ({ DumpParsedAst.hs:17:19-30 }
+              (HsAppTy
+               (NoExt)
+               ({ DumpParsedAst.hs:17:19-28 }
+                (HsAppTy
+                 (NoExt)
+                 ({ DumpParsedAst.hs:17:19-26 }
+                  (HsAppKindTy
+                   (NoExt)
+                   ({ DumpParsedAst.hs:17:19 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpParsedAst.hs:17:19 }
+                      (Unqual
+                       {OccName: T}))))
+                   ({ DumpParsedAst.hs:17:22-26 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpParsedAst.hs:17:22-26 }
+                      (Unqual
+                       {OccName: Peano}))))))
+                 ({ DumpParsedAst.hs:17:28 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpParsedAst.hs:17:28 }
+                    (Unqual
+                     {OccName: f}))))))
+               ({ DumpParsedAst.hs:17:30 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpParsedAst.hs:17:30 }
+                  (Unqual
+                   {OccName: a})))))))))]))
+       ({ DumpParsedAst.hs:16:13-14 }
+        (Unqual
+         {OccName: F1}))
+       (HsQTvs
+        (NoExt)
+        [({ DumpParsedAst.hs:16:17-22 }
+          (KindedTyVar
+           (NoExt)
+           ({ DumpParsedAst.hs:16:17 }
+            (Unqual
+             {OccName: a}))
+           ({ DumpParsedAst.hs:16:22 }
+            (HsTyVar
+             (NoExt)
+             (NotPromoted)
+             ({ DumpParsedAst.hs:16:22 }
+              (Unqual
+               {OccName: k}))))))
+        ,({ DumpParsedAst.hs:16:26-39 }
+          (KindedTyVar
+           (NoExt)
+           ({ DumpParsedAst.hs:16:26 }
+            (Unqual
+             {OccName: f}))
+           ({ DumpParsedAst.hs:16:31-39 }
+            (HsFunTy
+             (NoExt)
+             ({ DumpParsedAst.hs:16:31 }
+              (HsTyVar
+               (NoExt)
+               (NotPromoted)
+               ({ DumpParsedAst.hs:16:31 }
+                (Unqual
+                 {OccName: k}))))
+             ({ DumpParsedAst.hs:16:36-39 }
+              (HsTyVar
+               (NoExt)
+               (NotPromoted)
+               ({ DumpParsedAst.hs:16:36-39 }
+                (Unqual
+                 {OccName: Type}))))))))])
+       (Prefix)
+       ({ DumpParsedAst.hs:16:42-48 }
+        (KindSig
+         (NoExt)
+         ({ DumpParsedAst.hs:16:45-48 }
+          (HsTyVar
+           (NoExt)
+           (NotPromoted)
+           ({ DumpParsedAst.hs:16:45-48 }
+            (Unqual
+             {OccName: Type}))))))
+       (Nothing)))))
+  ,({ DumpParsedAst.hs:19:1-23 }
     (ValD
      (NoExt)
      (FunBind
       (NoExt)
-      ({ DumpParsedAst.hs:11:1-4 }
+      ({ DumpParsedAst.hs:19:1-4 }
        (Unqual
         {OccName: main}))
       (MG
        (NoExt)
-       ({ DumpParsedAst.hs:11:1-23 }
-        [({ DumpParsedAst.hs:11:1-23 }
+       ({ DumpParsedAst.hs:19:1-23 }
+        [({ DumpParsedAst.hs:19:1-23 }
           (Match
            (NoExt)
            (FunRhs
-            ({ DumpParsedAst.hs:11:1-4 }
+            ({ DumpParsedAst.hs:19:1-4 }
              (Unqual
               {OccName: main}))
             (Prefix)
@@ -211,20 +429,20 @@
            []
            (GRHSs
             (NoExt)
-            [({ DumpParsedAst.hs:11:6-23 }
+            [({ DumpParsedAst.hs:19:6-23 }
               (GRHS
                (NoExt)
                []
-               ({ DumpParsedAst.hs:11:8-23 }
+               ({ DumpParsedAst.hs:19:8-23 }
                 (HsApp
                  (NoExt)
-                 ({ DumpParsedAst.hs:11:8-15 }
+                 ({ DumpParsedAst.hs:19:8-15 }
                   (HsVar
                    (NoExt)
-                   ({ DumpParsedAst.hs:11:8-15 }
+                   ({ DumpParsedAst.hs:19:8-15 }
                     (Unqual
                      {OccName: putStrLn}))))
-                 ({ DumpParsedAst.hs:11:17-23 }
+                 ({ DumpParsedAst.hs:19:17-23 }
                   (HsLit
                    (NoExt)
                    (HsString
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
index c617febd40..d5be8627be 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
@@ -1,7 +1,8 @@
 {-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators,
-             TypeFamilies #-}
+             TypeFamilies, StarIsType, TypeApplications #-}
 
 module DumpRenamedAst where
+import Data.Kind
 
 import Data.Kind (Type)
 
@@ -17,4 +18,9 @@ data family Nat :: k -> k -> Type
 newtype instance Nat (a :: k -> Type) :: (k -> Type) -> Type where
   Nat :: (forall xx. f xx -> g xx) -> Nat f g
 
+data T f (a :: k) = MkT (f a)
+
+type family F1 (a :: k) (f :: k -> Type) :: Type where
+  F1 @Peano a f = T @Peano f a
+
 main = putStrLn "hello"
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 5a35b0037c..8df66c806f 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -10,39 +10,39 @@
      [((,)
        (NonRecursive)
        {Bag(Located (HsBind Name)):
-        [({ DumpRenamedAst.hs:20:1-23 }
+        [({ DumpRenamedAst.hs:26:1-23 }
           (FunBind
            {NameSet:
             []}
-           ({ DumpRenamedAst.hs:20:1-4 }
+           ({ DumpRenamedAst.hs:26:1-4 }
             {Name: DumpRenamedAst.main})
            (MG
             (NoExt)
-            ({ DumpRenamedAst.hs:20:1-23 }
-             [({ DumpRenamedAst.hs:20:1-23 }
+            ({ DumpRenamedAst.hs:26:1-23 }
+             [({ DumpRenamedAst.hs:26:1-23 }
                (Match
                 (NoExt)
                 (FunRhs
-                 ({ DumpRenamedAst.hs:20:1-4 }
+                 ({ DumpRenamedAst.hs:26:1-4 }
                   {Name: DumpRenamedAst.main})
                  (Prefix)
                  (NoSrcStrict))
                 []
                 (GRHSs
                  (NoExt)
-                 [({ DumpRenamedAst.hs:20:6-23 }
+                 [({ DumpRenamedAst.hs:26:6-23 }
                    (GRHS
                     (NoExt)
                     []
-                    ({ DumpRenamedAst.hs:20:8-23 }
+                    ({ DumpRenamedAst.hs:26:8-23 }
                      (HsApp
                       (NoExt)
-                      ({ DumpRenamedAst.hs:20:8-15 }
+                      ({ DumpRenamedAst.hs:26:8-15 }
                        (HsVar
                         (NoExt)
-                        ({ DumpRenamedAst.hs:20:8-15 }
+                        ({ DumpRenamedAst.hs:26:8-15 }
                          {Name: System.IO.putStrLn})))
-                      ({ DumpRenamedAst.hs:20:17-23 }
+                      ({ DumpRenamedAst.hs:26:17-23 }
                        (HsLit
                         (NoExt)
                         (HsString
@@ -59,13 +59,13 @@
    []
    [(TyClGroup
      (NoExt)
-     [({ DumpRenamedAst.hs:8:1-30 }
+     [({ DumpRenamedAst.hs:9:1-30 }
        (DataDecl
         (DataDeclRn
          (True)
          {NameSet:
           [{Name: DumpRenamedAst.Peano}]})
-        ({ DumpRenamedAst.hs:8:6-10 }
+        ({ DumpRenamedAst.hs:9:6-10 }
          {Name: DumpRenamedAst.Peano})
         (HsQTvs
          (HsQTvsRn
@@ -81,10 +81,10 @@
           [])
          (Nothing)
          (Nothing)
-         [({ DumpRenamedAst.hs:8:14-17 }
+         [({ DumpRenamedAst.hs:9:14-17 }
            (ConDeclH98
             (NoExt)
-            ({ DumpRenamedAst.hs:8:14-17 }
+            ({ DumpRenamedAst.hs:9:14-17 }
              {Name: DumpRenamedAst.Zero})
             ({ <no location info> }
              (False))
@@ -93,21 +93,21 @@
             (PrefixCon
              [])
             (Nothing)))
-         ,({ DumpRenamedAst.hs:8:21-30 }
+         ,({ DumpRenamedAst.hs:9:21-30 }
            (ConDeclH98
             (NoExt)
-            ({ DumpRenamedAst.hs:8:21-24 }
+            ({ DumpRenamedAst.hs:9:21-24 }
              {Name: DumpRenamedAst.Succ})
             ({ <no location info> }
              (False))
             []
             (Nothing)
             (PrefixCon
-             [({ DumpRenamedAst.hs:8:26-30 }
+             [({ DumpRenamedAst.hs:9:26-30 }
                (HsTyVar
                 (NoExt)
                 (NotPromoted)
-                ({ DumpRenamedAst.hs:8:26-30 }
+                ({ DumpRenamedAst.hs:9:26-30 }
                  {Name: DumpRenamedAst.Peano})))])
             (Nothing)))]
          ({ <no location info> }
@@ -116,133 +116,135 @@
      [])
    ,(TyClGroup
      (NoExt)
-     [({ DumpRenamedAst.hs:10:1-39 }
+     [({ DumpRenamedAst.hs:11:1-39 }
        (FamDecl
         (NoExt)
         (FamilyDecl
          (NoExt)
          (ClosedTypeFamily
           (Just
-           [({ DumpRenamedAst.hs:11:3-36 }
+           [({ DumpRenamedAst.hs:12:3-36 }
              (HsIB
               [{Name: a}
               ,{Name: as}]
               (FamEqn
                (NoExt)
-               ({ DumpRenamedAst.hs:11:3-8 }
+               ({ DumpRenamedAst.hs:12:3-8 }
                 {Name: DumpRenamedAst.Length})
                (Nothing)
-               [({ DumpRenamedAst.hs:11:10-17 }
-                 (HsParTy
-                  (NoExt)
-                  ({ DumpRenamedAst.hs:11:11-16 }
-                   (HsOpTy
-                    (NoExt)
-                    ({ DumpRenamedAst.hs:11:11 }
-                     (HsTyVar
-                      (NoExt)
-                      (NotPromoted)
-                      ({ DumpRenamedAst.hs:11:11 }
-                       {Name: a})))
-                    ({ DumpRenamedAst.hs:11:13 }
-                     {Name: :})
-                    ({ DumpRenamedAst.hs:11:15-16 }
-                     (HsTyVar
-                      (NoExt)
-                      (NotPromoted)
-                      ({ DumpRenamedAst.hs:11:15-16 }
-                       {Name: as})))))))]
+               [(HsValArg
+                 ({ DumpRenamedAst.hs:12:10-17 }
+                  (HsParTy
+                   (NoExt)
+                   ({ DumpRenamedAst.hs:12:11-16 }
+                    (HsOpTy
+                     (NoExt)
+                     ({ DumpRenamedAst.hs:12:11 }
+                      (HsTyVar
+                       (NoExt)
+                       (NotPromoted)
+                       ({ DumpRenamedAst.hs:12:11 }
+                        {Name: a})))
+                     ({ DumpRenamedAst.hs:12:13 }
+                      {Name: :})
+                     ({ DumpRenamedAst.hs:12:15-16 }
+                      (HsTyVar
+                       (NoExt)
+                       (NotPromoted)
+                       ({ DumpRenamedAst.hs:12:15-16 }
+                        {Name: as}))))))))]
                (Prefix)
-               ({ DumpRenamedAst.hs:11:21-36 }
+               ({ DumpRenamedAst.hs:12:21-36 }
                 (HsAppTy
                  (NoExt)
-                 ({ DumpRenamedAst.hs:11:21-24 }
+                 ({ DumpRenamedAst.hs:12:21-24 }
                   (HsTyVar
                    (NoExt)
                    (NotPromoted)
-                   ({ DumpRenamedAst.hs:11:21-24 }
+                   ({ DumpRenamedAst.hs:12:21-24 }
                     {Name: DumpRenamedAst.Succ})))
-                 ({ DumpRenamedAst.hs:11:26-36 }
+                 ({ DumpRenamedAst.hs:12:26-36 }
                   (HsParTy
                    (NoExt)
-                   ({ DumpRenamedAst.hs:11:27-35 }
+                   ({ DumpRenamedAst.hs:12:27-35 }
                     (HsAppTy
                      (NoExt)
-                     ({ DumpRenamedAst.hs:11:27-32 }
+                     ({ DumpRenamedAst.hs:12:27-32 }
                       (HsTyVar
                        (NoExt)
                        (NotPromoted)
-                       ({ DumpRenamedAst.hs:11:27-32 }
+                       ({ DumpRenamedAst.hs:12:27-32 }
                         {Name: DumpRenamedAst.Length})))
-                     ({ DumpRenamedAst.hs:11:34-35 }
+                     ({ DumpRenamedAst.hs:12:34-35 }
                       (HsTyVar
                        (NoExt)
                        (NotPromoted)
-                       ({ DumpRenamedAst.hs:11:34-35 }
+                       ({ DumpRenamedAst.hs:12:34-35 }
                         {Name: as}))))))))))))
-           ,({ DumpRenamedAst.hs:12:3-24 }
+           ,({ DumpRenamedAst.hs:13:3-24 }
              (HsIB
               []
               (FamEqn
                (NoExt)
-               ({ DumpRenamedAst.hs:12:3-8 }
+               ({ DumpRenamedAst.hs:13:3-8 }
                 {Name: DumpRenamedAst.Length})
                (Nothing)
-               [({ DumpRenamedAst.hs:12:10-12 }
-                 (HsExplicitListTy
-                  (NoExt)
-                  (IsPromoted)
-                  []))]
+               [(HsValArg
+                 ({ DumpRenamedAst.hs:13:10-12 }
+                  (HsExplicitListTy
+                   (NoExt)
+                   (IsPromoted)
+                   [])))]
                (Prefix)
-               ({ DumpRenamedAst.hs:12:21-24 }
+               ({ DumpRenamedAst.hs:13:21-24 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:12:21-24 }
+                 ({ DumpRenamedAst.hs:13:21-24 }
                   {Name: DumpRenamedAst.Zero}))))))]))
-         ({ DumpRenamedAst.hs:10:13-18 }
+         ({ DumpRenamedAst.hs:11:13-18 }
           {Name: DumpRenamedAst.Length})
          (HsQTvs
           (HsQTvsRn
            [{Name: k}]
            {NameSet:
             []})
-          [({ DumpRenamedAst.hs:10:21-29 }
+          [({ DumpRenamedAst.hs:11:21-29 }
             (KindedTyVar
              (NoExt)
-             ({ DumpRenamedAst.hs:10:21-22 }
+             ({ DumpRenamedAst.hs:11:21-22 }
               {Name: as})
-             ({ DumpRenamedAst.hs:10:27-29 }
+             ({ DumpRenamedAst.hs:11:27-29 }
               (HsListTy
                (NoExt)
-               ({ DumpRenamedAst.hs:10:28 }
+               ({ DumpRenamedAst.hs:11:28 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:10:28 }
+                 ({ DumpRenamedAst.hs:11:28 }
                   {Name: k})))))))])
          (Prefix)
-         ({ DumpRenamedAst.hs:10:32-39 }
+         ({ DumpRenamedAst.hs:11:32-39 }
           (KindSig
            (NoExt)
-           ({ DumpRenamedAst.hs:10:35-39 }
+           ({ DumpRenamedAst.hs:11:35-39 }
             (HsTyVar
              (NoExt)
              (NotPromoted)
-             ({ DumpRenamedAst.hs:10:35-39 }
+             ({ DumpRenamedAst.hs:11:35-39 }
               {Name: DumpRenamedAst.Peano})))))
          (Nothing))))]
      []
      [])
    ,(TyClGroup
      (NoExt)
-     [({ DumpRenamedAst.hs:14:1-33 }
+     [({ DumpRenamedAst.hs:15:1-33 }
        (FamDecl
         (NoExt)
         (FamilyDecl
          (NoExt)
          (DataFamily)
-         ({ DumpRenamedAst.hs:14:13-15 }
+         ({ DumpRenamedAst.hs:15:13-15 }
           {Name: DumpRenamedAst.Nat})
          (HsQTvs
           (HsQTvsRn
@@ -251,36 +253,36 @@
             []})
           [])
          (Prefix)
-         ({ DumpRenamedAst.hs:14:17-33 }
+         ({ DumpRenamedAst.hs:15:17-33 }
           (KindSig
            (NoExt)
-           ({ DumpRenamedAst.hs:14:20-33 }
+           ({ DumpRenamedAst.hs:15:20-33 }
             (HsFunTy
              (NoExt)
-             ({ DumpRenamedAst.hs:14:20 }
+             ({ DumpRenamedAst.hs:15:20 }
               (HsTyVar
                (NoExt)
                (NotPromoted)
-               ({ DumpRenamedAst.hs:14:20 }
+               ({ DumpRenamedAst.hs:15:20 }
                 {Name: k})))
-             ({ DumpRenamedAst.hs:14:25-33 }
+             ({ DumpRenamedAst.hs:15:25-33 }
               (HsFunTy
                (NoExt)
-               ({ DumpRenamedAst.hs:14:25 }
+               ({ DumpRenamedAst.hs:15:25 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:14:25 }
+                 ({ DumpRenamedAst.hs:15:25 }
                   {Name: k})))
-               ({ DumpRenamedAst.hs:14:30-33 }
+               ({ DumpRenamedAst.hs:15:30-33 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:14:30-33 }
+                 ({ DumpRenamedAst.hs:15:30-33 }
                   {Name: GHC.Types.Type})))))))))
          (Nothing))))]
      []
-     [({ DumpRenamedAst.hs:(17,1)-(18,45) }
+     [({ DumpRenamedAst.hs:(18,1)-(19,45) }
        (DataFamInstD
         (NoExt)
         (DataFamInstDecl
@@ -289,36 +291,37 @@
           ,{Name: a}]
           (FamEqn
            (NoExt)
-           ({ DumpRenamedAst.hs:17:18-20 }
+           ({ DumpRenamedAst.hs:18:18-20 }
             {Name: DumpRenamedAst.Nat})
            (Nothing)
-           [({ DumpRenamedAst.hs:17:22-37 }
-             (HsParTy
-              (NoExt)
-              ({ DumpRenamedAst.hs:17:23-36 }
-               (HsKindSig
-                (NoExt)
-                ({ DumpRenamedAst.hs:17:23 }
-                 (HsTyVar
-                  (NoExt)
-                  (NotPromoted)
-                  ({ DumpRenamedAst.hs:17:23 }
-                   {Name: a})))
-                ({ DumpRenamedAst.hs:17:28-36 }
-                 (HsFunTy
-                  (NoExt)
-                  ({ DumpRenamedAst.hs:17:28 }
-                   (HsTyVar
-                    (NoExt)
-                    (NotPromoted)
-                    ({ DumpRenamedAst.hs:17:28 }
-                     {Name: k})))
-                  ({ DumpRenamedAst.hs:17:33-36 }
-                   (HsTyVar
-                    (NoExt)
-                    (NotPromoted)
-                    ({ DumpRenamedAst.hs:17:33-36 }
-                     {Name: GHC.Types.Type})))))))))]
+           [(HsValArg
+             ({ DumpRenamedAst.hs:18:22-37 }
+              (HsParTy
+               (NoExt)
+               ({ DumpRenamedAst.hs:18:23-36 }
+                (HsKindSig
+                 (NoExt)
+                 ({ DumpRenamedAst.hs:18:23 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:18:23 }
+                    {Name: a})))
+                 ({ DumpRenamedAst.hs:18:28-36 }
+                  (HsFunTy
+                   (NoExt)
+                   ({ DumpRenamedAst.hs:18:28 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpRenamedAst.hs:18:28 }
+                      {Name: k})))
+                   ({ DumpRenamedAst.hs:18:33-36 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpRenamedAst.hs:18:33-36 }
+                      {Name: GHC.Types.Type}))))))))))]
            (Prefix)
            (HsDataDefn
             (NoExt)
@@ -327,39 +330,39 @@
              [])
             (Nothing)
             (Just
-             ({ DumpRenamedAst.hs:17:42-60 }
+             ({ DumpRenamedAst.hs:18:42-60 }
               (HsFunTy
                (NoExt)
-               ({ DumpRenamedAst.hs:17:42-52 }
+               ({ DumpRenamedAst.hs:18:42-52 }
                 (HsParTy
                  (NoExt)
-                 ({ DumpRenamedAst.hs:17:43-51 }
+                 ({ DumpRenamedAst.hs:18:43-51 }
                   (HsFunTy
                    (NoExt)
-                   ({ DumpRenamedAst.hs:17:43 }
+                   ({ DumpRenamedAst.hs:18:43 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:17:43 }
+                     ({ DumpRenamedAst.hs:18:43 }
                       {Name: k})))
-                   ({ DumpRenamedAst.hs:17:48-51 }
+                   ({ DumpRenamedAst.hs:18:48-51 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:17:48-51 }
+                     ({ DumpRenamedAst.hs:18:48-51 }
                       {Name: GHC.Types.Type})))))))
-               ({ DumpRenamedAst.hs:17:57-60 }
+               ({ DumpRenamedAst.hs:18:57-60 }
                 (HsTyVar
                  (NoExt)
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:17:57-60 }
+                 ({ DumpRenamedAst.hs:18:57-60 }
                   {Name: GHC.Types.Type}))))))
-            [({ DumpRenamedAst.hs:18:3-45 }
+            [({ DumpRenamedAst.hs:19:3-45 }
               (ConDeclGADT
                (NoExt)
-               [({ DumpRenamedAst.hs:18:3-5 }
+               [({ DumpRenamedAst.hs:19:3-5 }
                  {Name: DumpRenamedAst.Nat})]
-               ({ DumpRenamedAst.hs:18:10-45 }
+               ({ DumpRenamedAst.hs:19:10-45 }
                 (False))
                (HsQTvs
                 (HsQTvsRn
@@ -370,77 +373,274 @@
                 [])
                (Nothing)
                (PrefixCon
-                [({ DumpRenamedAst.hs:18:10-34 }
+                [({ DumpRenamedAst.hs:19:10-34 }
                   (HsParTy
                    (NoExt)
-                   ({ DumpRenamedAst.hs:18:11-33 }
+                   ({ DumpRenamedAst.hs:19:11-33 }
                     (HsForAllTy
                      (NoExt)
-                     [({ DumpRenamedAst.hs:18:18-19 }
+                     [({ DumpRenamedAst.hs:19:18-19 }
                        (UserTyVar
                         (NoExt)
-                        ({ DumpRenamedAst.hs:18:18-19 }
+                        ({ DumpRenamedAst.hs:19:18-19 }
                          {Name: xx})))]
-                     ({ DumpRenamedAst.hs:18:22-33 }
+                     ({ DumpRenamedAst.hs:19:22-33 }
                       (HsFunTy
                        (NoExt)
-                       ({ DumpRenamedAst.hs:18:22-25 }
+                       ({ DumpRenamedAst.hs:19:22-25 }
                         (HsAppTy
                          (NoExt)
-                         ({ DumpRenamedAst.hs:18:22 }
+                         ({ DumpRenamedAst.hs:19:22 }
                           (HsTyVar
                            (NoExt)
                            (NotPromoted)
-                           ({ DumpRenamedAst.hs:18:22 }
+                           ({ DumpRenamedAst.hs:19:22 }
                             {Name: f})))
-                         ({ DumpRenamedAst.hs:18:24-25 }
+                         ({ DumpRenamedAst.hs:19:24-25 }
                           (HsTyVar
                            (NoExt)
                            (NotPromoted)
-                           ({ DumpRenamedAst.hs:18:24-25 }
+                           ({ DumpRenamedAst.hs:19:24-25 }
                             {Name: xx})))))
-                       ({ DumpRenamedAst.hs:18:30-33 }
+                       ({ DumpRenamedAst.hs:19:30-33 }
                         (HsAppTy
                          (NoExt)
-                         ({ DumpRenamedAst.hs:18:30 }
+                         ({ DumpRenamedAst.hs:19:30 }
                           (HsTyVar
                            (NoExt)
                            (NotPromoted)
-                           ({ DumpRenamedAst.hs:18:30 }
+                           ({ DumpRenamedAst.hs:19:30 }
                             {Name: g})))
-                         ({ DumpRenamedAst.hs:18:32-33 }
+                         ({ DumpRenamedAst.hs:19:32-33 }
                           (HsTyVar
                            (NoExt)
                            (NotPromoted)
-                           ({ DumpRenamedAst.hs:18:32-33 }
+                           ({ DumpRenamedAst.hs:19:32-33 }
                             {Name: xx})))))))))))])
-               ({ DumpRenamedAst.hs:18:39-45 }
+               ({ DumpRenamedAst.hs:19:39-45 }
                 (HsAppTy
                  (NoExt)
-                 ({ DumpRenamedAst.hs:18:39-43 }
+                 ({ DumpRenamedAst.hs:19:39-43 }
                   (HsAppTy
                    (NoExt)
-                   ({ DumpRenamedAst.hs:18:39-41 }
+                   ({ DumpRenamedAst.hs:19:39-41 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:18:39-41 }
+                     ({ DumpRenamedAst.hs:19:39-41 }
                       {Name: DumpRenamedAst.Nat})))
-                   ({ DumpRenamedAst.hs:18:43 }
+                   ({ DumpRenamedAst.hs:19:43 }
                     (HsTyVar
                      (NoExt)
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:18:43 }
+                     ({ DumpRenamedAst.hs:19:43 }
                       {Name: f})))))
-                 ({ DumpRenamedAst.hs:18:45 }
+                 ({ DumpRenamedAst.hs:19:45 }
                   (HsTyVar
                    (NoExt)
                    (NotPromoted)
-                   ({ DumpRenamedAst.hs:18:45 }
+                   ({ DumpRenamedAst.hs:19:45 }
                     {Name: g})))))
                (Nothing)))]
             ({ <no location info> }
-             [])))))))])]
+             [])))))))])
+   ,(TyClGroup
+     (NoExt)
+     [({ DumpRenamedAst.hs:21:1-29 }
+       (DataDecl
+        (DataDeclRn
+         (False)
+         {NameSet:
+          [{Name: a}
+          ,{Name: f}]})
+        ({ DumpRenamedAst.hs:21:6 }
+         {Name: DumpRenamedAst.T})
+        (HsQTvs
+         (HsQTvsRn
+          [{Name: k}]
+          {NameSet:
+           []})
+         [({ DumpRenamedAst.hs:21:8 }
+           (UserTyVar
+            (NoExt)
+            ({ DumpRenamedAst.hs:21:8 }
+             {Name: f})))
+         ,({ DumpRenamedAst.hs:21:11-16 }
+           (KindedTyVar
+            (NoExt)
+            ({ DumpRenamedAst.hs:21:11 }
+             {Name: a})
+            ({ DumpRenamedAst.hs:21:16 }
+             (HsTyVar
+              (NoExt)
+              (NotPromoted)
+              ({ DumpRenamedAst.hs:21:16 }
+               {Name: k})))))])
+        (Prefix)
+        (HsDataDefn
+         (NoExt)
+         (DataType)
+         ({ <no location info> }
+          [])
+         (Nothing)
+         (Nothing)
+         [({ DumpRenamedAst.hs:21:21-29 }
+           (ConDeclH98
+            (NoExt)
+            ({ DumpRenamedAst.hs:21:21-23 }
+             {Name: DumpRenamedAst.MkT})
+            ({ <no location info> }
+             (False))
+            []
+            (Nothing)
+            (PrefixCon
+             [({ DumpRenamedAst.hs:21:25-29 }
+               (HsParTy
+                (NoExt)
+                ({ DumpRenamedAst.hs:21:26-28 }
+                 (HsAppTy
+                  (NoExt)
+                  ({ DumpRenamedAst.hs:21:26 }
+                   (HsTyVar
+                    (NoExt)
+                    (NotPromoted)
+                    ({ DumpRenamedAst.hs:21:26 }
+                     {Name: f})))
+                  ({ DumpRenamedAst.hs:21:28 }
+                   (HsTyVar
+                    (NoExt)
+                    (NotPromoted)
+                    ({ DumpRenamedAst.hs:21:28 }
+                     {Name: a})))))))])
+            (Nothing)))]
+         ({ <no location info> }
+          []))))]
+     []
+     [])
+   ,(TyClGroup
+     (NoExt)
+     [({ DumpRenamedAst.hs:23:1-48 }
+       (FamDecl
+        (NoExt)
+        (FamilyDecl
+         (NoExt)
+         (ClosedTypeFamily
+          (Just
+           [({ DumpRenamedAst.hs:24:3-30 }
+             (HsIB
+              [{Name: a}
+              ,{Name: f}]
+              (FamEqn
+               (NoExt)
+               ({ DumpRenamedAst.hs:24:3-4 }
+                {Name: DumpRenamedAst.F1})
+               (Nothing)
+               [(HsTypeArg
+                 ({ DumpRenamedAst.hs:24:7-11 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:24:7-11 }
+                    {Name: DumpRenamedAst.Peano}))))
+               ,(HsValArg
+                 ({ DumpRenamedAst.hs:24:13 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:24:13 }
+                    {Name: a}))))
+               ,(HsValArg
+                 ({ DumpRenamedAst.hs:24:15 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:24:15 }
+                    {Name: f}))))]
+               (Prefix)
+               ({ DumpRenamedAst.hs:24:19-30 }
+                (HsAppTy
+                 (NoExt)
+                 ({ DumpRenamedAst.hs:24:19-28 }
+                  (HsAppTy
+                   (NoExt)
+                   ({ DumpRenamedAst.hs:24:19-26 }
+                    (HsAppKindTy
+                     (NoExt)
+                     ({ DumpRenamedAst.hs:24:19 }
+                      (HsTyVar
+                       (NoExt)
+                       (NotPromoted)
+                       ({ DumpRenamedAst.hs:24:19 }
+                        {Name: DumpRenamedAst.T})))
+                     ({ DumpRenamedAst.hs:24:22-26 }
+                      (HsTyVar
+                       (NoExt)
+                       (NotPromoted)
+                       ({ DumpRenamedAst.hs:24:22-26 }
+                        {Name: DumpRenamedAst.Peano})))))
+                   ({ DumpRenamedAst.hs:24:28 }
+                    (HsTyVar
+                     (NoExt)
+                     (NotPromoted)
+                     ({ DumpRenamedAst.hs:24:28 }
+                      {Name: f})))))
+                 ({ DumpRenamedAst.hs:24:30 }
+                  (HsTyVar
+                   (NoExt)
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:24:30 }
+                    {Name: a}))))))))]))
+         ({ DumpRenamedAst.hs:23:13-14 }
+          {Name: DumpRenamedAst.F1})
+         (HsQTvs
+          (HsQTvsRn
+           [{Name: k}]
+           {NameSet:
+            []})
+          [({ DumpRenamedAst.hs:23:17-22 }
+            (KindedTyVar
+             (NoExt)
+             ({ DumpRenamedAst.hs:23:17 }
+              {Name: a})
+             ({ DumpRenamedAst.hs:23:22 }
+              (HsTyVar
+               (NoExt)
+               (NotPromoted)
+               ({ DumpRenamedAst.hs:23:22 }
+                {Name: k})))))
+          ,({ DumpRenamedAst.hs:23:26-39 }
+            (KindedTyVar
+             (NoExt)
+             ({ DumpRenamedAst.hs:23:26 }
+              {Name: f})
+             ({ DumpRenamedAst.hs:23:31-39 }
+              (HsFunTy
+               (NoExt)
+               ({ DumpRenamedAst.hs:23:31 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpRenamedAst.hs:23:31 }
+                  {Name: k})))
+               ({ DumpRenamedAst.hs:23:36-39 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ DumpRenamedAst.hs:23:36-39 }
+                  {Name: GHC.Types.Type})))))))])
+         (Prefix)
+         ({ DumpRenamedAst.hs:23:42-48 }
+          (KindSig
+           (NoExt)
+           ({ DumpRenamedAst.hs:23:45-48 }
+            (HsTyVar
+             (NoExt)
+             (NotPromoted)
+             ({ DumpRenamedAst.hs:23:45-48 }
+              {Name: GHC.Types.Type})))))
+         (Nothing))))]
+     []
+     [])]
    []
    []
    []
@@ -462,11 +662,24 @@
      (True)
      (Nothing)
      (Nothing)))
-  ,({ DumpRenamedAst.hs:6:1-23 }
+  ,({ DumpRenamedAst.hs:5:1-16 }
+    (ImportDecl
+     (NoExt)
+     (NoSourceText)
+     ({ DumpRenamedAst.hs:5:8-16 }
+      {ModuleName: Data.Kind})
+     (Nothing)
+     (False)
+     (False)
+     (False)
+     (False)
+     (Nothing)
+     (Nothing)))
+  ,({ DumpRenamedAst.hs:7:1-23 }
     (ImportDecl
      (NoExt)
      (NoSourceText)
-     ({ DumpRenamedAst.hs:6:8-16 }
+     ({ DumpRenamedAst.hs:7:8-16 }
       {ModuleName: Data.Kind})
      (Nothing)
      (False)
@@ -477,13 +690,13 @@
      (Just
       ((,)
        (False)
-       ({ DumpRenamedAst.hs:6:18-23 }
-        [({ DumpRenamedAst.hs:6:19-22 }
+       ({ DumpRenamedAst.hs:7:18-23 }
+        [({ DumpRenamedAst.hs:7:19-22 }
           (IEThingAbs
            (NoExt)
-           ({ DumpRenamedAst.hs:6:19-22 }
+           ({ DumpRenamedAst.hs:7:19-22 }
             (IEName
-             ({ DumpRenamedAst.hs:6:19-22 }
+             ({ DumpRenamedAst.hs:7:19-22 }
               {Name: GHC.Types.Type})))))])))))]
   (Nothing)
   (Nothing)))
diff --git a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs
index 35887649a7..82cf107e5d 100644
--- a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs
+++ b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs
@@ -1,6 +1,8 @@
-{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies
+             , TypeApplications #-}
 
 module DumpTypecheckedAst where
+import Data.Kind
 
 data Peano = Zero | Succ Peano
 
@@ -8,4 +10,9 @@ type family Length (as :: [k]) :: Peano where
   Length (a : as) = Succ (Length as)
   Length '[]      = Zero
 
+data T f (a :: k) = MkT (f a)
+
+type family F (a :: k) (f :: k -> Type) :: Type where
+  F @Peano a f = T @Peano f a
+
 main = putStrLn "hello"
diff --git a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
index 8e3e868fb9..7c6bfd72d0 100644
--- a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
@@ -5,6 +5,138 @@
  [({ <no location info> }
    (VarBind
     (NoExt)
+    {Var: DumpTypecheckedAst.$tcT}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsApp
+          (NoExt)
+          ({ <no location info> }
+           (HsApp
+            (NoExt)
+            ({ <no location info> }
+             (HsApp
+              (NoExt)
+              ({ <no location info> }
+               (HsApp
+                (NoExt)
+                ({ <no location info> }
+                 (HsConLikeOut
+                  (NoExt)
+                  ({abstract:ConLike})))
+                ({ <no location info> }
+                 (HsLit
+                  (NoExt)
+                  {HsWord{64}Prim (1374752024144278257) (NoSourceText)}))))
+              ({ <no location info> }
+               (HsLit
+                (NoExt)
+                {HsWord{64}Prim (13654949607623281177) (NoSourceText)}))))
+            ({ <no location info> }
+             (HsVar
+              (NoExt)
+              ({ <no location info> }
+               {Var: DumpTypecheckedAst.$trModule})))))
+          ({ <no location info> }
+           (HsPar
+            (NoExt)
+            ({ <no location info> }
+             (HsApp
+              (NoExt)
+              ({ <no location info> }
+               (HsConLikeOut
+                (NoExt)
+                ({abstract:ConLike})))
+              ({ <no location info> }
+               (HsLit
+                (NoExt)
+                (HsStringPrim
+                 (NoSourceText)
+                 "T")))))))))
+        ({ <no location info> }
+         (HsLit
+          (NoExt)
+          {HsInt{64}Prim (1) (SourceText
+                              "1")}))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: $krep})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: DumpTypecheckedAst.$tc'MkT}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsApp
+          (NoExt)
+          ({ <no location info> }
+           (HsApp
+            (NoExt)
+            ({ <no location info> }
+             (HsApp
+              (NoExt)
+              ({ <no location info> }
+               (HsApp
+                (NoExt)
+                ({ <no location info> }
+                 (HsConLikeOut
+                  (NoExt)
+                  ({abstract:ConLike})))
+                ({ <no location info> }
+                 (HsLit
+                  (NoExt)
+                  {HsWord{64}Prim (10715337633704422415) (NoSourceText)}))))
+              ({ <no location info> }
+               (HsLit
+                (NoExt)
+                {HsWord{64}Prim (12411373583424111944) (NoSourceText)}))))
+            ({ <no location info> }
+             (HsVar
+              (NoExt)
+              ({ <no location info> }
+               {Var: DumpTypecheckedAst.$trModule})))))
+          ({ <no location info> }
+           (HsPar
+            (NoExt)
+            ({ <no location info> }
+             (HsApp
+              (NoExt)
+              ({ <no location info> }
+               (HsConLikeOut
+                (NoExt)
+                ({abstract:ConLike})))
+              ({ <no location info> }
+               (HsLit
+                (NoExt)
+                (HsStringPrim
+                 (NoSourceText)
+                 "'MkT")))))))))
+        ({ <no location info> }
+         (HsLit
+          (NoExt)
+          {HsInt{64}Prim (3) (SourceText
+                              "3")}))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: $krep})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
     {Var: DumpTypecheckedAst.$tcPeano}
     ({ <no location info> }
      (HsApp
@@ -208,6 +340,147 @@
      (HsApp
       (NoExt)
       ({ <no location info> }
+       (HsConLikeOut
+        (NoExt)
+        ({abstract:ConLike})))
+      ({ <no location info> }
+       (HsLit
+        (NoExt)
+        (HsInt
+         (NoExt)
+         (IL
+          (SourceText
+           "2")
+          (False)
+          (2)))))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsConLikeOut
+        (NoExt)
+        ({abstract:ConLike})))
+      ({ <no location info> }
+       (HsLit
+        (NoExt)
+        (HsInt
+         (NoExt)
+         (IL
+          (SourceText
+           "1")
+          (False)
+          (1)))))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsConLikeOut
+        (NoExt)
+        ({abstract:ConLike})))
+      ({ <no location info> }
+       (HsLit
+        (NoExt)
+        (HsInt
+         (NoExt)
+         (IL
+          (SourceText
+           "0")
+          (False)
+          (0)))))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsConLikeOut
+          (NoExt)
+          ({abstract:ConLike})))
+        ({ <no location info> }
+         (HsVar
+          (NoExt)
+          ({ <no location info> }
+           {Var: $krep})))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: $krep})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsConLikeOut
+          (NoExt)
+          ({abstract:ConLike})))
+        ({ <no location info> }
+         (HsVar
+          (NoExt)
+          ({ <no location info> }
+           {Var: $krep})))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: GHC.Types.krep$*})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsConLikeOut
+          (NoExt)
+          ({abstract:ConLike})))
+        ({ <no location info> }
+         (HsVar
+          (NoExt)
+          ({ <no location info> }
+           {Var: $krep})))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: $krep})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
        (HsApp
         (NoExt)
         ({ <no location info> }
@@ -243,6 +516,133 @@
          (HsVar
           (NoExt)
           ({ <no location info> }
+           {Var: $krep})))))
+      ({ <no location info> }
+       (HsVar
+        (NoExt)
+        ({ <no location info> }
+         {Var: $krep})))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsConLikeOut
+          (NoExt)
+          ({abstract:ConLike})))
+        ({ <no location info> }
+         (HsVar
+          (NoExt)
+          ({ <no location info> }
+           {Var: DumpTypecheckedAst.$tcT})))))
+      ({ <no location info> }
+       (HsPar
+        (NoExt)
+        ({ <no location info> }
+         (HsApp
+          (NoExt)
+          ({ <no location info> }
+           (HsApp
+            (NoExt)
+            ({ <no location info> }
+             (HsWrap
+              (NoExt)
+              (WpTyApp
+               (TyConApp
+                ({abstract:TyCon})
+                []))
+              (HsConLikeOut
+               (NoExt)
+               ({abstract:ConLike}))))
+            ({ <no location info> }
+             (HsVar
+              (NoExt)
+              ({ <no location info> }
+               {Var: $krep})))))
+          ({ <no location info> }
+           (HsPar
+            (NoExt)
+            ({ <no location info> }
+             (HsApp
+              (NoExt)
+              ({ <no location info> }
+               (HsApp
+                (NoExt)
+                ({ <no location info> }
+                 (HsWrap
+                  (NoExt)
+                  (WpTyApp
+                   (TyConApp
+                    ({abstract:TyCon})
+                    []))
+                  (HsConLikeOut
+                   (NoExt)
+                   ({abstract:ConLike}))))
+                ({ <no location info> }
+                 (HsVar
+                  (NoExt)
+                  ({ <no location info> }
+                   {Var: $krep})))))
+              ({ <no location info> }
+               (HsPar
+                (NoExt)
+                ({ <no location info> }
+                 (HsApp
+                  (NoExt)
+                  ({ <no location info> }
+                   (HsApp
+                    (NoExt)
+                    ({ <no location info> }
+                     (HsWrap
+                      (NoExt)
+                      (WpTyApp
+                       (TyConApp
+                        ({abstract:TyCon})
+                        []))
+                      (HsConLikeOut
+                       (NoExt)
+                       ({abstract:ConLike}))))
+                    ({ <no location info> }
+                     (HsVar
+                      (NoExt)
+                      ({ <no location info> }
+                       {Var: $krep})))))
+                  ({ <no location info> }
+                   (HsWrap
+                    (NoExt)
+                    (WpTyApp
+                     (TyConApp
+                      ({abstract:TyCon})
+                      []))
+                    (HsConLikeOut
+                     (NoExt)
+                     ({abstract:ConLike}))))))))))))))))))
+    (False)))
+ ,({ <no location info> }
+   (VarBind
+    (NoExt)
+    {Var: $krep}
+    ({ <no location info> }
+     (HsApp
+      (NoExt)
+      ({ <no location info> }
+       (HsApp
+        (NoExt)
+        ({ <no location info> }
+         (HsConLikeOut
+          (NoExt)
+          ({abstract:ConLike})))
+        ({ <no location info> }
+         (HsVar
+          (NoExt)
+          ({ <no location info> }
            {Var: DumpTypecheckedAst.$tcPeano})))))
       ({ <no location info> }
        (HsWrap
@@ -302,7 +702,7 @@
              (NoSourceText)
              "DumpTypecheckedAst")))))))))
     (False)))
- ,({ DumpTypecheckedAst.hs:11:1-23 }
+ ,({ DumpTypecheckedAst.hs:18:1-23 }
    (AbsBinds
     (NoExt)
     []
@@ -316,11 +716,11 @@
        []))]
     [({abstract:TcEvBinds})]
     {Bag(Located (HsBind Var)):
-     [({ DumpTypecheckedAst.hs:11:1-23 }
+     [({ DumpTypecheckedAst.hs:18:1-23 }
        (FunBind
         {NameSet:
          []}
-        ({ DumpTypecheckedAst.hs:11:1-4 }
+        ({ DumpTypecheckedAst.hs:18:1-4 }
          {Var: main})
         (MG
          (MatchGroupTc
@@ -330,31 +730,31 @@
            [(TyConApp
              ({abstract:TyCon})
              [])]))
-         ({ DumpTypecheckedAst.hs:11:1-23 }
-          [({ DumpTypecheckedAst.hs:11:1-23 }
+         ({ DumpTypecheckedAst.hs:18:1-23 }
+          [({ DumpTypecheckedAst.hs:18:1-23 }
             (Match
              (NoExt)
              (FunRhs
-              ({ DumpTypecheckedAst.hs:11:1-4 }
+              ({ DumpTypecheckedAst.hs:18:1-4 }
                {Name: main})
               (Prefix)
               (NoSrcStrict))
              []
              (GRHSs
               (NoExt)
-              [({ DumpTypecheckedAst.hs:11:6-23 }
+              [({ DumpTypecheckedAst.hs:18:6-23 }
                 (GRHS
                  (NoExt)
                  []
-                 ({ DumpTypecheckedAst.hs:11:8-23 }
+                 ({ DumpTypecheckedAst.hs:18:8-23 }
                   (HsApp
                    (NoExt)
-                   ({ DumpTypecheckedAst.hs:11:8-15 }
+                   ({ DumpTypecheckedAst.hs:18:8-15 }
                     (HsVar
                      (NoExt)
                      ({ <no location info> }
                       {Var: putStrLn})))
-                   ({ DumpTypecheckedAst.hs:11:17-23 }
+                   ({ DumpTypecheckedAst.hs:18:17-23 }
                     (HsLit
                      (NoExt)
                      (HsString
diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr
index 125e88084a..8ea6ec5322 100644
--- a/testsuite/tests/parser/should_compile/KindSigs.stderr
+++ b/testsuite/tests/parser/should_compile/KindSigs.stderr
@@ -38,13 +38,14 @@
               (Unqual
                {OccName: Foo}))
              (Nothing)
-             [({ KindSigs.hs:12:7 }
-               (HsTyVar
-                (NoExt)
-                (NotPromoted)
-                ({ KindSigs.hs:12:7 }
-                 (Unqual
-                  {OccName: a}))))]
+             [(HsValArg
+               ({ KindSigs.hs:12:7 }
+                (HsTyVar
+                 (NoExt)
+                 (NotPromoted)
+                 ({ KindSigs.hs:12:7 }
+                  (Unqual
+                   {OccName: a})))))]
              (Prefix)
              ({ KindSigs.hs:12:11-21 }
               (HsKindSig
diff --git a/testsuite/tests/parser/should_compile/T12045e.hs b/testsuite/tests/parser/should_compile/T12045e.hs
new file mode 100644
index 0000000000..1be903adfb
--- /dev/null
+++ b/testsuite/tests/parser/should_compile/T12045e.hs
@@ -0,0 +1,13 @@
+{-# Language DataKinds             #-}
+{-# Language TypeApplications         #-}
+{-# Language PolyKinds             #-}
+
+module T12045e where
+
+import Data.Kind
+
+data Nat = Zero | Succ Nat
+data T (n :: k) = MkT
+data D1 n = T @Nat n :! ()
+data D2 n = () :!! T @Nat n
+data D3 n = T @Nat n :!!! T @Nat n
diff --git a/testsuite/tests/parser/should_compile/all.T b/testsuite/tests/parser/should_compile/all.T
index a85b09cbb7..b3f693d783 100644
--- a/testsuite/tests/parser/should_compile/all.T
+++ b/testsuite/tests/parser/should_compile/all.T
@@ -113,6 +113,7 @@ test('T11622', normal, compile, [''])
 test('DumpParsedAst',      normal, compile, ['-dsuppress-uniques -ddump-parsed-ast'])
 test('DumpRenamedAst',     normal, compile, ['-dsuppress-uniques -ddump-rn-ast'])
 test('DumpTypecheckedAst', normal, compile, ['-dsuppress-uniques -ddump-tc-ast'])
+test('T12045e', normal, compile, [''])
 test('T13087', normal, compile, [''])
 test('T13747', normal, compile, [''])
 test('T14189',     normal, compile, ['-dsuppress-uniques -ddump-rn-ast'])
diff --git a/testsuite/tests/parser/should_fail/T12045d.hs b/testsuite/tests/parser/should_fail/T12045d.hs
new file mode 100644
index 0000000000..3c4b2a6c10
--- /dev/null
+++ b/testsuite/tests/parser/should_fail/T12045d.hs
@@ -0,0 +1,11 @@
+{-# Language DataKinds             #-}
+{-# Language TypeApplications         #-}
+{-# Language PolyKinds             #-}
+
+module Bug where
+
+import Data.Kind
+
+data Nat = Zero | Succ Nat
+
+data D n = MkD @Nat Bool
diff --git a/testsuite/tests/parser/should_fail/T12045d.stderr b/testsuite/tests/parser/should_fail/T12045d.stderr
new file mode 100644
index 0000000000..128cf58d86
--- /dev/null
+++ b/testsuite/tests/parser/should_fail/T12045d.stderr
@@ -0,0 +1,4 @@
+
+T12045d.hs:11:16: error:
+    Unexpected kind application in a data/newtype declaration:
+      MkD @Nat Bool
diff --git a/testsuite/tests/parser/should_fail/all.T b/testsuite/tests/parser/should_fail/all.T
index f1f5122c5a..2d7c241ed0 100644
--- a/testsuite/tests/parser/should_fail/all.T
+++ b/testsuite/tests/parser/should_fail/all.T
@@ -110,6 +110,7 @@ test('T13414', literate, compile_fail, [''])
 test('T8501a', normal, compile_fail, [''])
 test('T8501b', normal, compile_fail, [''])
 test('T8501c', normal, compile_fail, [''])
+test('T12045d', normal, compile_fail, [''])
 test('T12610', normal, compile_fail, [''])
 test('T13450', normal, compile_fail, [''])
 test('T13450TH', normal, compile_fail, [''])
diff --git a/testsuite/tests/partial-sigs/should_compile/Defaulting2MROff.stderr b/testsuite/tests/partial-sigs/should_compile/Defaulting2MROff.stderr
index 008a1fc5c5..beb850c5fe 100644
--- a/testsuite/tests/partial-sigs/should_compile/Defaulting2MROff.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/Defaulting2MROff.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  bravo :: forall w. Num w => w
+  bravo :: forall _. Num _ => _
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/Defaulting2MROn.stderr b/testsuite/tests/partial-sigs/should_compile/Defaulting2MROn.stderr
index 008a1fc5c5..beb850c5fe 100644
--- a/testsuite/tests/partial-sigs/should_compile/Defaulting2MROn.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/Defaulting2MROn.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  bravo :: forall w. Num w => w
+  bravo :: forall _. Num _ => _
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/Either.stderr b/testsuite/tests/partial-sigs/should_compile/Either.stderr
index 86fe4a03b4..9769909910 100644
--- a/testsuite/tests/partial-sigs/should_compile/Either.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/Either.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  barry :: forall w. w -> (Either [Char] w, Either [Char] w)
+  barry :: forall _. _ -> (Either [Char] _, Either [Char] _)
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/EveryNamed.stderr b/testsuite/tests/partial-sigs/should_compile/EveryNamed.stderr
index e6f8a9042c..59e2054c8c 100644
--- a/testsuite/tests/partial-sigs/should_compile/EveryNamed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/EveryNamed.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  every :: forall w. (w -> Bool) -> [w] -> Bool
+  every :: forall _. (_ -> Bool) -> [_] -> Bool
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
index cfe5aeb6d0..a6dbd5a143 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
@@ -4,14 +4,16 @@ ExprSigLocal.hs:9:35: warning: [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of <expression> :: a -> a
                at ExprSigLocal.hs:9:20-35
-    • In an expression type signature: forall a. a -> _
+    • In the type ‘a -> _’
+      In an expression type signature: forall a. a -> _
       In the expression: ((\ x -> x) :: forall a. a -> _)
-      In an equation for ‘y’: y = ((\ x -> x) :: forall a. a -> _)
     • Relevant bindings include
         y :: b -> b (bound at ExprSigLocal.hs:9:1)
 
 ExprSigLocal.hs:11:21: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of g :: a -> a at ExprSigLocal.hs:12:1-7
-    • In the type signature: g :: forall a. a -> _
+               the inferred type of g :: a -> a
+               at ExprSigLocal.hs:12:1-7
+    • In the type ‘a -> _’
+      In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
index c49b1a025b..8bd167fdb7 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
@@ -125,12 +125,12 @@ TYPE SIGNATURES
     (P.Foldable t, Monad m) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
-  maxBound :: forall w. Bounded w => w
+  maxBound :: forall _. Bounded _ => _
   maximum ::
     forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
   maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
-  minBound :: forall w. Bounded w => w
+  minBound :: forall _. Bounded _ => _
   minimum ::
     forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
   mod :: forall a. Integral a => a -> a -> a
@@ -142,7 +142,7 @@ TYPE SIGNATURES
   odd :: forall a. Integral a => a -> Bool
   or :: forall (t :: * -> *). P.Foldable t => t Bool -> Bool
   otherwise :: Bool
-  pi :: forall w. Floating w => w
+  pi :: forall _. Floating _ => _
   pred :: forall a. Enum a => a -> a
   print :: forall a. Show a => a -> IO ()
   product ::
@@ -212,7 +212,7 @@ TYPE SIGNATURES
   toRational :: forall a. Real a => a -> Rational
   truncate :: forall a b. (RealFrac a, Integral b) => a -> b
   uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
-  undefined :: forall w. w
+  undefined :: forall _. _
   unlines :: [String] -> String
   until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
   unwords :: [String] -> String
diff --git a/testsuite/tests/partial-sigs/should_compile/SimpleGen.stderr b/testsuite/tests/partial-sigs/should_compile/SimpleGen.stderr
index bae5060aab..9d10860ff9 100644
--- a/testsuite/tests/partial-sigs/should_compile/SimpleGen.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SimpleGen.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  bar :: forall w. w -> Bool
+  bar :: forall _. _ -> Bool
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
index ea974895e2..88fc8d50b9 100644
--- a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
@@ -3,12 +3,13 @@
 
 SplicesUsed.hs:7:16: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Maybe Bool’
-    • In the type signature: maybeBool :: (_)
+    • In the type ‘_’
+      In the type signature: maybeBool :: (_)
 
 SplicesUsed.hs:8:15: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_a’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of <expression> :: w -> w
+    • Found type wildcard ‘_a’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of <expression> :: _ -> _
                at SplicesUsed.hs:8:15-22
     • In an expression type signature: _a -> _a
       In the expression: id :: _a -> _a
@@ -18,10 +19,9 @@ SplicesUsed.hs:8:15: warning: [-Wpartial-type-signatures (in -Wdefault)]
 
 SplicesUsed.hs:8:27: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Bool’
-    • In an expression type signature: Maybe _
-      In the first argument of ‘id :: _a -> _a’, namely
-        ‘(Just True :: Maybe _)’
-      In the expression: (id :: _a -> _a) (Just True :: Maybe _)
+    • In the first argument of ‘Maybe’, namely ‘_’
+      In the type ‘Maybe _’
+      In an expression type signature: Maybe _
     • Relevant bindings include
         maybeBool :: Maybe Bool (bound at SplicesUsed.hs:8:1)
 
@@ -30,28 +30,32 @@ SplicesUsed.hs:10:17: warning: [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of charA :: a -> (Char, a)
                at SplicesUsed.hs:11:1-18
-    • In the type signature: charA :: a -> (_)
+    • In the type ‘a -> (_)’
+      In the type signature: charA :: a -> (_)
 
 SplicesUsed.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a -> Bool’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type signature: filter' :: (_ -> _ -> _)
+    • In the type ‘_ -> _ -> _’
+      In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘[a]’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type signature: filter' :: (_ -> _ -> _)
+    • In the type ‘_ -> _ -> _’
+      In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘[a]’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type signature: filter' :: (_ -> _ -> _)
+    • In the type ‘_ -> _ -> _’
+      In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:16:3: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Eq a’
@@ -72,8 +76,8 @@ SplicesUsed.hs:18:3: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • In the type signature: bar :: _a -> _b -> (_a, _b)
 
 SplicesUsed.hs:18:3: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_b’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Bool -> w -> (Bool, w)
+    • Found type wildcard ‘_b’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Bool -> _ -> (Bool, _)
                at SplicesUsed.hs:18:3-10
     • In the type signature: bar :: _a -> _b -> (_a, _b)
diff --git a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
index a11164482c..a24928a70b 100644
--- a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
@@ -1,4 +1,4 @@
 
-SuperCls.hs:4:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+SuperCls.hs:4:6: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: f :: (Ord a, _) => a -> Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 229b9e1df1..870a72ed5a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -1,25 +1,23 @@
 
 T10403.hs:15:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Functor f’
-      Where: ‘f’ is a rigid type variable
-               bound by the inferred type of
-                        h1 :: Functor f => (a -> b) -> f a -> H f
+      Where: ‘f’ is a rigid type variable bound by
+               the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
                at T10403.hs:17:1-41
     • In the type signature: h1 :: _ => _
 
 T10403.hs:15:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(a -> b) -> f a -> H f’
-      Where: ‘b’, ‘a’, ‘f’ are rigid type variables
-               bound by the inferred type of
-                        h1 :: Functor f => (a -> b) -> f a -> H f
+      Where: ‘b’, ‘a’, ‘f’ are rigid type variables bound by
+               the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
                at T10403.hs:17:1-41
     • In the type signature: h1 :: _ => _
 
 T10403.hs:19:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(a -> b) -> f0 a -> H f0’
       Where: ‘f0’ is an ambiguous type variable
-             ‘b’, ‘a’ are rigid type variables
-               bound by the inferred type of h2 :: (a -> b) -> f0 a -> H f0
+             ‘b’, ‘a’ are rigid type variables bound by
+               the inferred type of h2 :: (a -> b) -> f0 a -> H f0
                at T10403.hs:22:1-41
     • In the type signature: h2 :: _
 
diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
index 5acc3fa15b..164007679c 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
@@ -2,7 +2,8 @@
 T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘p2’
       Where: ‘p2’ is a rigid type variable bound by
-               the inferred type of g :: p2 -> p2 at T10438.hs:(6,9)-(8,21)
+               the inferred type of g :: p2 -> p2
+               at T10438.hs:(6,9)-(8,21)
     • In the type signature: x :: _
       In an equation for ‘g’:
           g r
diff --git a/testsuite/tests/partial-sigs/should_compile/T10519.stderr b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
index f57144dcd1..31d525cda0 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10519.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
@@ -1,5 +1,5 @@
 
-T10519.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T10519.hs:5:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Eq a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: Eq a => a -> a -> Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T11016.stderr b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
index 49363fb24c..01e8b1ae4b 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11016.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
@@ -1,5 +1,5 @@
 
-T11016.hs:5:19: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T11016.hs:5:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: f1 :: (?x :: Int, _) => Int
 
diff --git a/testsuite/tests/partial-sigs/should_compile/T11339a.stderr b/testsuite/tests/partial-sigs/should_compile/T11339a.stderr
index af8d47d4b6..c5c5e6f312 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11339a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11339a.stderr
@@ -2,5 +2,6 @@
 T11339a.hs:5:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a -> a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of bar :: a -> a at T11339a.hs:6:1-10
+               the inferred type of bar :: a -> a
+               at T11339a.hs:6:1-10
     • In the type signature: bar :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T11670.stderr b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
index 04d6af5450..1a0e7df6ef 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11670.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
@@ -1,18 +1,17 @@
 
 T11670.hs:10:42: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘CLong’
-    • In an expression type signature: IO _
-      In the expression: peekElemOff undefined 0 :: IO _
-      In an equation for ‘T11670.peek’:
-          T11670.peek ptr = peekElemOff undefined 0 :: IO _
+    • In the first argument of ‘IO’, namely ‘_’
+      In the type ‘IO _’
+      In an expression type signature: IO _
     • Relevant bindings include
         ptr :: Ptr a (bound at T11670.hs:10:6)
         peek :: Ptr a -> IO CLong (bound at T11670.hs:10:1)
 
 T11670.hs:13:40: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Storable w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of <expression> :: Storable w => IO w
+    • Found type wildcard ‘_’ standing for ‘Storable _’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of <expression> :: Storable _ => IO _
                at T11670.hs:13:40-48
     • In an expression type signature: _ => IO _
       In the expression: peekElemOff undefined 0 :: _ => IO _
@@ -23,14 +22,13 @@ T11670.hs:13:40: warning: [-Wpartial-type-signatures (in -Wdefault)]
         peek2 :: Ptr a -> IO CLong (bound at T11670.hs:13:1)
 
 T11670.hs:13:48: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of <expression> :: Storable w => IO w
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of <expression> :: Storable _ => IO _
                at T11670.hs:13:40-48
-    • In an expression type signature: _ => IO _
-      In the expression: peekElemOff undefined 0 :: _ => IO _
-      In an equation for ‘peek2’:
-          peek2 ptr = peekElemOff undefined 0 :: _ => IO _
+    • In the first argument of ‘IO’, namely ‘_’
+      In the type ‘IO _’
+      In an expression type signature: _ => IO _
     • Relevant bindings include
         ptr :: Ptr a (bound at T11670.hs:13:7)
         peek2 :: Ptr a -> IO CLong (bound at T11670.hs:13:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T12844.stderr b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
index 0e01cd30f3..b8cdba7968 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12844.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
@@ -1,5 +1,5 @@
 
-T12844.hs:12:9: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T12844.hs:12:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’
         standing for ‘(Foo rngs, Head rngs ~ '(r, r'))’
       Where: ‘rngs’, ‘k’, ‘r’, ‘k1’, ‘r'’
diff --git a/testsuite/tests/partial-sigs/should_compile/T12845.stderr b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
index a483c84231..0c01a80fc0 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12845.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
@@ -1,5 +1,5 @@
 
-T12845.hs:18:70: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T12845.hs:18:11: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature:
         broken :: forall r r' rngs.
diff --git a/testsuite/tests/partial-sigs/should_compile/T13482.stderr b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
index a21b7dcac4..017cc1535c 100644
--- a/testsuite/tests/partial-sigs/should_compile/T13482.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
@@ -1,5 +1,5 @@
 
-T13482.hs:10:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T13482.hs:10:20: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of
@@ -8,21 +8,21 @@ T13482.hs:10:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • In the type signature:
         minimal1_noksig :: forall m. _ => Int -> Bool
 
-T13482.hs:13:33: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T13482.hs:13:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal1 :: (Eq m, Monoid m) => Bool
                at T13482.hs:14:1-41
     • In the type signature: minimal1 :: forall (m :: Type). _ => Bool
 
-T13482.hs:16:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T13482.hs:16:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Monoid m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal2 :: (Eq m, Monoid m) => Bool
                at T13482.hs:17:1-41
     • In the type signature: minimal2 :: forall m. (Eq m, _) => Bool
 
-T13482.hs:19:34: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T13482.hs:19:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Eq m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal3 :: (Monoid m, Eq m) => Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T14217.stderr b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
index ebecbb9d5c..e4b9598d9e 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14217.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
@@ -1,5 +1,5 @@
 
-T14217.hs:32:11: error:
+T14217.hs:32:10: error:
     • Found type wildcard ‘_’
         standing for ‘(Eq a1, Eq a2, Eq a3, Eq a4, Eq a5, Eq a6, Eq a7,
                        Eq a8, Eq a9, Eq a10, Eq a11, Eq a12, Eq a13, Eq a14, Eq a15,
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643.stderr b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
index c5f204e799..5f1762743a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
@@ -1,8 +1,8 @@
 
-T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T14643.hs:5:11: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: af :: (Num a, _) => a -> a
 
-T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T14643.hs:5:11: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
index 1514ac92ed..11eab72ebb 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
@@ -1,8 +1,8 @@
 
-T14643a.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T14643a.hs:5:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: af :: (Num a, _) => a -> a
 
-T14643a.hs:8:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+T14643a.hs:8:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘()’
     • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
index c846b47dd2..b34c4a5b72 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
@@ -1,10 +1,11 @@
-T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    Found type wildcard ‘_’ standing for ‘Reduce (LiftOf zq) zq’
-     Where: ‘zq’ is a rigid type variable bound by
-              the inferred type of
-                bench_mulPublic :: (z ~ LiftOf zq, Reduce (LiftOf zq) zq) =>
-                                   Cyc zp -> Cyc z -> IO (zp, zq)
-              at T14715.hs:(14,1)-(16,14)
-    In the type signature:
-       bench_mulPublic :: forall z zp zq.
-                          (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp, zq)
+
+T14715.hs:13:20: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Reduce (LiftOf zq) zq’
+      Where: ‘zq’ is a rigid type variable bound by
+               the inferred type of
+                 bench_mulPublic :: (z ~ LiftOf zq, Reduce (LiftOf zq) zq) =>
+                                    Cyc zp -> Cyc z -> IO (zp, zq)
+               at T14715.hs:(14,1)-(16,14)
+    • In the type signature:
+        bench_mulPublic :: forall z zp zq.
+                           (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp, zq)
diff --git a/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr b/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
index a132b725e8..49ecb6c911 100644
--- a/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
@@ -1,9 +1,9 @@
 
 TypedSplice.hs:9:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Bool’
-    • In an expression type signature: _ -> _b
+    • In the type ‘_ -> _b’
+      In an expression type signature: _ -> _b
       In the Template Haskell quotation [|| not :: _ -> _b ||]
-      In the expression: [|| not :: _ -> _b ||]
     • Relevant bindings include
         metaExp :: Q (TExp (Bool -> Bool)) (bound at TypedSplice.hs:9:1)
 
diff --git a/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr b/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
index b9816b9339..e9931d23dd 100644
--- a/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  unc :: forall w1 w2 w3. (w1 -> w2 -> w3) -> (w1, w2) -> w3
+  unc :: forall _1 _2 _3. (_1 -> _2 -> _3) -> (_1, _2) -> _3
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr b/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
index f04dfbb0e9..666fb23620 100644
--- a/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  unc :: forall a b w. (a -> b -> w) -> (a, b) -> w
+  unc :: forall a b _. (a -> b -> _) -> (a, b) -> _
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index 2c891dc69d..cef1dedf6d 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -1,19 +1,19 @@
 TYPE SIGNATURES
-  bar :: forall t w. t -> (t -> w) -> w
+  bar :: forall t _. t -> (t -> _) -> _
   foo :: forall a. (Show a, Enum a) => a -> String
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
 
-WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_a’ standing for ‘a’
+WarningWildcardInstantiations.hs:5:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Enum a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WarningWildcardInstantiations.hs:6:1-21
     • In the type signature: foo :: (Show _a, _) => _a -> _
 
-WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Enum a’
+WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WarningWildcardInstantiations.hs:6:1-21
@@ -21,25 +21,29 @@ WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -
 
 WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘String’
-    • In the type signature: foo :: (Show _a, _) => _a -> _
+    • In the type ‘_a -> _’
+      In the type signature: foo :: (Show _a, _) => _a -> _
 
 WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘t’
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+               the inferred type of bar :: t -> (t -> _) -> _
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
 
 WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t -> w’
-      Where: ‘t’, ‘w’ are rigid type variables bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+    • Found type wildcard ‘_’ standing for ‘t -> _’
+      Where: ‘t’, ‘_’ are rigid type variables bound by
+               the inferred type of bar :: t -> (t -> _) -> _
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
 
 WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> _) -> _
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSplice.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSplice.stderr
index d1f5270d64..2426e4cd27 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSplice.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSplice.stderr
@@ -1,13 +1,13 @@
 
 ExtraConstraintsWildcardInPatternSplice.hs:5:8: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of foo :: w -> ()
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of foo :: _ -> ()
                at ExtraConstraintsWildcardInPatternSplice.hs:5:1-29
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
       In the pattern: _ :: _
       In an equation for ‘foo’: foo (_ :: _) = ()
     • Relevant bindings include
-        foo :: w -> ()
+        foo :: _ -> ()
           (bound at ExtraConstraintsWildcardInPatternSplice.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
index 69207b1af1..4837168487 100644
--- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
@@ -1,14 +1,14 @@
 
-InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
-    • Found type wildcard ‘_a’ standing for ‘b’
+InstantiatedNamedWildcardsInConstraints.hs:4:8: error:
+    • Found type wildcard ‘_’ standing for ‘Show b’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:5:1-26
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (Enum _a, _) => _a -> (String, b)
 
-InstantiatedNamedWildcardsInConstraints.hs:4:18: error:
-    • Found type wildcard ‘_’ standing for ‘Show b’
+InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
+    • Found type wildcard ‘_a’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:5:1-26
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedExtraConstraintsWildcard.stderr b/testsuite/tests/partial-sigs/should_fail/NamedExtraConstraintsWildcard.stderr
index c1a7d84896..c573747c02 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedExtraConstraintsWildcard.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedExtraConstraintsWildcard.stderr
@@ -1,11 +1,11 @@
 
 NamedExtraConstraintsWildcard.hs:5:1: error:
-    • Could not deduce: w0
-      from the context: (Eq a, w)
+    • Could not deduce: _0
+      from the context: (Eq a, _)
         bound by the inferred type for ‘foo’:
-                   forall a (w :: Constraint). (Eq a, w) => a -> a
+                   forall a (_ :: Constraint). (Eq a, _) => a -> a
         at NamedExtraConstraintsWildcard.hs:5:1-15
     • In the ambiguity check for the inferred type for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        foo :: forall a (w :: Constraint). (Eq a, w) => a -> a
+        foo :: forall a (_ :: Constraint). (Eq a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
index 7d7320f0fb..89b71e5959 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
@@ -1,12 +1,12 @@
 
 NamedWildcardsNotInMonotype.hs:5:1: error:
-    • Could not deduce (Eq w0)
-      from the context: (Show a, Eq w, Eq a)
+    • Could not deduce (Eq _0)
+      from the context: (Show a, Eq _, Eq a)
         bound by the inferred type for ‘foo’:
-                   forall a w. (Show a, Eq w, Eq a) => a -> a -> String
+                   forall a _. (Show a, Eq _, Eq a) => a -> a -> String
         at NamedWildcardsNotInMonotype.hs:5:1-33
-      The type variable ‘w0’ is ambiguous
+      The type variable ‘_0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        foo :: forall a w. (Show a, Eq w, Eq a) => a -> a -> String
+        foo :: forall a _. (Show a, Eq _, Eq a) => a -> a -> String
diff --git a/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr b/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
index 8e20d3fe98..be6ea0ae80 100644
--- a/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
@@ -2,9 +2,11 @@
 PartialTypeSignaturesDisabled.hs:4:8: error:
     • Found type wildcard ‘_’ standing for ‘Bool’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: foo :: _ -> _
+    • In the type ‘_ -> _’
+      In the type signature: foo :: _ -> _
 
 PartialTypeSignaturesDisabled.hs:4:13: error:
     • Found type wildcard ‘_’ standing for ‘Bool’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: foo :: _ -> _
+    • In the type ‘_ -> _’
+      In the type signature: foo :: _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
index f20ae3c563..8ca3dcd540 100644
--- a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
@@ -1,9 +1,9 @@
 
 PatBind3.hs:6:12: error:
-    • Couldn't match type ‘(Bool, w)’ with ‘Char’
-      Expected type: Maybe ((Bool, w) -> Char)
-        Actual type: Maybe ((Bool, w) -> (Bool, w))
+    • Couldn't match type ‘(Bool, _)’ with ‘Char’
+      Expected type: Maybe ((Bool, _) -> Char)
+        Actual type: Maybe ((Bool, _) -> (Bool, _))
     • In the expression: Just id
       In a pattern binding: Just foo = Just id
     • Relevant bindings include
-        foo :: (Bool, w) -> Char (bound at PatBind3.hs:6:6)
+        foo :: (Bool, _) -> Char (bound at PatBind3.hs:6:6)
diff --git a/testsuite/tests/partial-sigs/should_fail/T10615.stderr b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
index 0b9bcb811c..f95df86dad 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10615.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
@@ -3,7 +3,8 @@ T10615.hs:4:7: error:
     • Found type wildcard ‘_’ standing for ‘a1’
       Where: ‘a1’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: f1 :: _ -> f
+    • In the type ‘_ -> f’
+      In the type signature: f1 :: _ -> f
 
 T10615.hs:5:6: error:
     • Couldn't match type ‘f’ with ‘b1 -> a1’
@@ -20,7 +21,8 @@ T10615.hs:7:7: error:
     • Found type wildcard ‘_’ standing for ‘a0’
       Where: ‘a0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: f2 :: _ -> _f
+    • In the type ‘_ -> _f’
+      In the type signature: f2 :: _ -> _f
 
 T10615.hs:8:6: error:
     • Couldn't match type ‘_f’ with ‘b0 -> a0’
diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
index 5da96928c4..6352548bd8 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
@@ -13,7 +13,8 @@ T10999.hs:5:17: error:
                the inferred type of f :: Ord a => () -> Set.Set a
                at T10999.hs:6:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: f :: _ => () -> _
+    • In the type ‘() -> _’
+      In the type signature: f :: _ => () -> _
 
 T10999.hs:8:28: error:
     • Ambiguous type variable ‘b0’ arising from a use of ‘f’
diff --git a/testsuite/tests/partial-sigs/should_fail/T11122.stderr b/testsuite/tests/partial-sigs/should_fail/T11122.stderr
index d308c4771d..a6b4c618ec 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11122.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11122.stderr
@@ -1,4 +1,6 @@
 
 T11122.hs:19:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Int’
-    • In the type signature: parser :: Parser _
+    • In the first argument of ‘Parser’, namely ‘_’
+      In the type ‘Parser _’
+      In the type signature: parser :: Parser _
diff --git a/testsuite/tests/partial-sigs/should_fail/T11515.stderr b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
index 2870457500..0c8ff61cff 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11515.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
@@ -1,5 +1,5 @@
 
-T11515.hs:7:20: error:
+T11515.hs:7:8: error:
     • Found type wildcard ‘_’ standing for ‘()’
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (ShowSyn a, _) => a -> String
diff --git a/testsuite/tests/partial-sigs/should_fail/T11976.stderr b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
index 28104625e1..c4c3d50e59 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11976.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
@@ -1,12 +1,12 @@
 
 T11976.hs:7:7: error:
     • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls: Lens w3 w4 w5
+      with a type involving foralls: Lens _3 _4 _5
         GHC doesn't yet support impredicative polymorphism
     • In the expression: undefined :: Lens _ _ _
       In an equation for ‘foo’: foo = undefined :: Lens _ _ _
     • Relevant bindings include
-        foo :: Lens w w1 w2 (bound at T11976.hs:7:1)
+        foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
 
 T11976.hs:7:20: error:
     • Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
@@ -14,4 +14,4 @@ T11976.hs:7:20: error:
       In an expression type signature: Lens _ _ _
       In the expression: undefined :: Lens _ _ _
     • Relevant bindings include
-        foo :: Lens w w1 w2 (bound at T11976.hs:7:1)
+        foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T12634.stderr b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
index 316f7eb2c5..7aab25f5f8 100644
--- a/testsuite/tests/partial-sigs/should_fail/T12634.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
@@ -1,5 +1,5 @@
 
-T12634.hs:14:37: error:
+T12634.hs:14:19: error:
     • Found type wildcard ‘_’ standing for ‘()’
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 67fae7b31e..0a07f0590d 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,10 +1,10 @@
 
 T14040a.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl0
-                                       -> (forall y. p0 w0 'WeirdNil)
+                                       -> (forall y. p0 _0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                                           Sing x -> Sing xs -> p0 w1 xs -> p0 w2 ('WeirdCons x xs))
-                                       -> p0 w3 wl0’
+                                           Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs))
+                                       -> p0 _3 wl0’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index f22178774e..80c8ce2683 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -55,10 +55,8 @@ T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
              ‘m’ is a rigid type variable bound by
                the instance declaration
                at T14584.hs:54:10-89
-    • In an expression type signature: Sing _
-      In the second argument of ‘fromSing’, namely
-        ‘(sing @m @a :: Sing _)’
-      In the fourth argument of ‘act’, namely
-        ‘(fromSing @m (sing @m @a :: Sing _))’
+    • In the first argument of ‘Sing’, namely ‘_’
+      In the type ‘Sing _’
+      In an expression type signature: Sing _
     • Relevant bindings include
         monHom :: a -> a (bound at T14584.hs:56:3)
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
index 15282550b5..6ec4c440cc 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
@@ -1,16 +1,18 @@
 
 TidyClash.hs:8:19: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: w_ -> (w_, w -> w1)
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: w_ -> (w_, _ -> _1)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: bar :: w_ -> (w_, _ -> _)
+    • In the type ‘w_ -> (w_, _ -> _)’
+      In the type signature: bar :: w_ -> (w_, _ -> _)
 
 TidyClash.hs:8:24: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of bar :: w_ -> (w_, w -> w1)
+    • Found type wildcard ‘_’ standing for ‘_1’
+      Where: ‘_1’ is a rigid type variable bound by
+               the inferred type of bar :: w_ -> (w_, _ -> _1)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: bar :: w_ -> (w_, _ -> _)
+    • In the type ‘w_ -> (w_, _ -> _)’
+      In the type signature: bar :: w_ -> (w_, _ -> _)
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
index 42a98ad8ef..a2c63ecbbc 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
@@ -1,53 +1,60 @@
 
 TidyClash2.hs:13:20: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t at TidyClash2.hs:14:1-40
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of barry :: _ -> _1 -> t
+               at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: barry :: forall t. _ -> _ -> t
+    • In the type ‘_ -> _ -> t’
+      In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:13:25: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t at TidyClash2.hs:14:1-40
+    • Found type wildcard ‘_’ standing for ‘_1’
+      Where: ‘_1’ is a rigid type variable bound by
+               the inferred type of barry :: _ -> _1 -> t
+               at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: barry :: forall t. _ -> _ -> t
+    • In the type ‘_ -> _ -> t’
+      In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:14:13: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t at TidyClash2.hs:14:1-40
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of barry :: _ -> _1 -> t
+               at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
       In the pattern: x :: _
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        barry :: _ -> _1 -> t (bound at TidyClash2.hs:14:1)
 
 TidyClash2.hs:14:22: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t at TidyClash2.hs:14:1-40
+    • Found type wildcard ‘_’ standing for ‘_1’
+      Where: ‘_1’ is a rigid type variable bound by
+               the inferred type of barry :: _ -> _1 -> t
+               at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
       In the pattern: y :: _
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        x :: w (bound at TidyClash2.hs:14:8)
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        x :: _ (bound at TidyClash2.hs:14:8)
+        barry :: _ -> _1 -> t (bound at TidyClash2.hs:14:1)
 
 TidyClash2.hs:14:40: error:
-    • Found type wildcard ‘_’ standing for ‘w2’
-      Where: ‘w2’ is a rigid type variable bound by
-               the inferred type of <expression> :: w2 at TidyClash2.hs:14:40
+    • Found type wildcard ‘_’ standing for ‘_2’
+      Where: ‘_2’ is a rigid type variable bound by
+               the inferred type of <expression> :: _2
+               at TidyClash2.hs:14:40
       To use the inferred type, enable PartialTypeSignatures
     • In an expression type signature: _
       In the expression: undefined :: _
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        y :: w1 (bound at TidyClash2.hs:14:17)
-        x :: w (bound at TidyClash2.hs:14:8)
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        y :: _1 (bound at TidyClash2.hs:14:17)
+        x :: _ (bound at TidyClash2.hs:14:8)
+        barry :: _ -> _1 -> t (bound at TidyClash2.hs:14:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index aa5e8247f3..02e9c970ed 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -1,14 +1,14 @@
 
-WildcardInstantiations.hs:5:14: error:
-    • Found type wildcard ‘_a’ standing for ‘a’
+WildcardInstantiations.hs:5:8: error:
+    • Found type wildcard ‘_’ standing for ‘Enum a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WildcardInstantiations.hs:6:1-21
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (Show _a, _) => _a -> _
 
-WildcardInstantiations.hs:5:18: error:
-    • Found type wildcard ‘_’ standing for ‘Enum a’
+WildcardInstantiations.hs:5:14: error:
+    • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WildcardInstantiations.hs:6:1-21
@@ -18,28 +18,32 @@ WildcardInstantiations.hs:5:18: error:
 WildcardInstantiations.hs:5:30: error:
     • Found type wildcard ‘_’ standing for ‘String’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: foo :: (Show _a, _) => _a -> _
+    • In the type ‘_a -> _’
+      In the type signature: foo :: (Show _a, _) => _a -> _
 
 WildcardInstantiations.hs:8:8: error:
     • Found type wildcard ‘_’ standing for ‘t’
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+               the inferred type of bar :: t -> (t -> _) -> _
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
 
 WildcardInstantiations.hs:8:13: error:
-    • Found type wildcard ‘_’ standing for ‘t -> w’
-      Where: ‘t’, ‘w’ are rigid type variables bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+    • Found type wildcard ‘_’ standing for ‘t -> _’
+      Where: ‘t’, ‘_’ are rigid type variables bound by
+               the inferred type of bar :: t -> (t -> _) -> _
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
 
 WildcardInstantiations.hs:8:18: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: t -> (t -> w) -> w
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> _) -> _
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: bar :: _ -> _ -> _
+    • In the type ‘_ -> _ -> _’
+      In the type signature: bar :: _ -> _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardsInPatternAndExprSig.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardsInPatternAndExprSig.stderr
index 726b43898e..d75a630d04 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardsInPatternAndExprSig.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardsInPatternAndExprSig.stderr
@@ -1,34 +1,34 @@
 
 WildcardsInPatternAndExprSig.hs:4:18: error:
-    • Found type wildcard ‘_a’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Maybe [w] -> w -> [w]
+    • Found type wildcard ‘_a’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Maybe [_] -> _ -> [_]
                at WildcardsInPatternAndExprSig.hs:4:1-68
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _a
       In the pattern: x :: _a
       In the pattern: [x :: _a]
     • Relevant bindings include
-        bar :: Maybe [w] -> w -> [w]
+        bar :: Maybe [_] -> _ -> [_]
           (bound at WildcardsInPatternAndExprSig.hs:4:1)
 
 WildcardsInPatternAndExprSig.hs:4:25: error:
-    • Found type wildcard ‘_’ standing for ‘[w]’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Maybe [w] -> w -> [w]
+    • Found type wildcard ‘_’ standing for ‘[_]’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Maybe [_] -> _ -> [_]
                at WildcardsInPatternAndExprSig.hs:4:1-68
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
       In the pattern: [x :: _a] :: _
       In the pattern: Just ([x :: _a] :: _)
     • Relevant bindings include
-        bar :: Maybe [w] -> w -> [w]
+        bar :: Maybe [_] -> _ -> [_]
           (bound at WildcardsInPatternAndExprSig.hs:4:1)
 
 WildcardsInPatternAndExprSig.hs:4:38: error:
-    • Found type wildcard ‘_b’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Maybe [w] -> w -> [w]
+    • Found type wildcard ‘_b’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Maybe [_] -> _ -> [_]
                at WildcardsInPatternAndExprSig.hs:4:1-68
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: Maybe [_b]
@@ -37,13 +37,13 @@ WildcardsInPatternAndExprSig.hs:4:38: error:
           bar (Just ([x :: _a] :: _) :: Maybe [_b]) (z :: _c)
             = [x, z] :: [_d]
     • Relevant bindings include
-        bar :: Maybe [w] -> w -> [w]
+        bar :: Maybe [_] -> _ -> [_]
           (bound at WildcardsInPatternAndExprSig.hs:4:1)
 
 WildcardsInPatternAndExprSig.hs:4:49: error:
-    • Found type wildcard ‘_c’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Maybe [w] -> w -> [w]
+    • Found type wildcard ‘_c’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Maybe [_] -> _ -> [_]
                at WildcardsInPatternAndExprSig.hs:4:1-68
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _c
@@ -52,14 +52,14 @@ WildcardsInPatternAndExprSig.hs:4:49: error:
           bar (Just ([x :: _a] :: _) :: Maybe [_b]) (z :: _c)
             = [x, z] :: [_d]
     • Relevant bindings include
-        x :: w (bound at WildcardsInPatternAndExprSig.hs:4:13)
-        bar :: Maybe [w] -> w -> [w]
+        x :: _ (bound at WildcardsInPatternAndExprSig.hs:4:13)
+        bar :: Maybe [_] -> _ -> [_]
           (bound at WildcardsInPatternAndExprSig.hs:4:1)
 
 WildcardsInPatternAndExprSig.hs:4:66: error:
-    • Found type wildcard ‘_d’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: Maybe [w] -> w -> [w]
+    • Found type wildcard ‘_d’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of bar :: Maybe [_] -> _ -> [_]
                at WildcardsInPatternAndExprSig.hs:4:1-68
       To use the inferred type, enable PartialTypeSignatures
     • In an expression type signature: [_d]
@@ -68,7 +68,7 @@ WildcardsInPatternAndExprSig.hs:4:66: error:
           bar (Just ([x :: _a] :: _) :: Maybe [_b]) (z :: _c)
             = [x, z] :: [_d]
     • Relevant bindings include
-        z :: w (bound at WildcardsInPatternAndExprSig.hs:4:44)
-        x :: w (bound at WildcardsInPatternAndExprSig.hs:4:13)
-        bar :: Maybe [w] -> w -> [w]
+        z :: _ (bound at WildcardsInPatternAndExprSig.hs:4:44)
+        x :: _ (bound at WildcardsInPatternAndExprSig.hs:4:13)
+        bar :: Maybe [_] -> _ -> [_]
           (bound at WildcardsInPatternAndExprSig.hs:4:1)
diff --git a/testsuite/tests/partial-sigs/should_run/T15415.stderr b/testsuite/tests/partial-sigs/should_run/T15415.stderr
index daa791ffa4..a43f80e6bd 100644
--- a/testsuite/tests/partial-sigs/should_run/T15415.stderr
+++ b/testsuite/tests/partial-sigs/should_run/T15415.stderr
@@ -1,27 +1,41 @@
 
 <interactive>:1:7: error:
-    Found type wildcard ‘_’ standing for ‘w0 :: k0’
-    Where: ‘k0’ is an ambiguous type variable
-           ‘w0’ is an ambiguous type variable
-    To use the inferred type, enable PartialTypeSignatures
+    • Found type wildcard ‘_’ standing for ‘_0 :: k0’
+      Where: ‘k0’ is an ambiguous type variable
+             ‘_0’ is an ambiguous type variable
+      To use the inferred type, enable PartialTypeSignatures
+    • In the first argument of ‘Proxy’, namely ‘_’
+      In the type ‘Proxy _’
 
 <interactive>:1:17: error:
-    Found type wildcard ‘_’ standing for ‘* -> *’
-    To use the inferred type, enable PartialTypeSignatures
+    • Found type wildcard ‘_’ standing for ‘* -> *’
+      To use the inferred type, enable PartialTypeSignatures
+    • In the kind ‘_’
+      In the first argument of ‘Proxy’, namely ‘(Maybe :: _)’
+      In the type ‘Proxy (Maybe :: _)’
 
 <interactive>:1:11: error:
-    Found type wildcard ‘_’ standing for ‘w0’
-    Where: ‘w0’ is an ambiguous type variable
-    To use the inferred type, enable PartialTypeSignatures
+    • Found type wildcard ‘_’ standing for ‘_0’
+      Where: ‘_0’ is an ambiguous type variable
+      To use the inferred type, enable PartialTypeSignatures
+    • In the first argument of ‘Dependent’, namely ‘_’
+      In the type ‘Dependent _’
 
 <interactive>:1:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    Found type wildcard ‘_’ standing for ‘w0 :: k0’
-    Where: ‘k0’ is an ambiguous type variable
-           ‘w0’ is an ambiguous type variable
+    • Found type wildcard ‘_’ standing for ‘_0 :: k0’
+      Where: ‘k0’ is an ambiguous type variable
+             ‘_0’ is an ambiguous type variable
+    • In the first argument of ‘Proxy’, namely ‘_’
+      In the type ‘Proxy _’
 
 <interactive>:1:17: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    Found type wildcard ‘_’ standing for ‘* -> *’
+    • Found type wildcard ‘_’ standing for ‘* -> *’
+    • In the kind ‘_’
+      In the first argument of ‘Proxy’, namely ‘(Maybe :: _)’
+      In the type ‘Proxy (Maybe :: _)’
 
 <interactive>:1:11: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    Found type wildcard ‘_’ standing for ‘w0’
-    Where: ‘w0’ is an ambiguous type variable
+    • Found type wildcard ‘_’ standing for ‘_0’
+      Where: ‘_0’ is an ambiguous type variable
+    • In the first argument of ‘Dependent’, namely ‘_’
+      In the type ‘Dependent _’
diff --git a/testsuite/tests/partial-sigs/should_run/T15415.stdout b/testsuite/tests/partial-sigs/should_run/T15415.stdout
index 709da2f17c..17af08faea 100644
--- a/testsuite/tests/partial-sigs/should_run/T15415.stdout
+++ b/testsuite/tests/partial-sigs/should_run/T15415.stdout
@@ -1,6 +1,6 @@
 Proxy _ :: *
 Proxy (Maybe :: _) :: *
-Dependent _ :: w -> *
+Dependent _ :: _ -> *
 Proxy _ :: *
 Proxy (Maybe :: _) :: *
-Dependent _ :: w -> *
+Dependent _ :: _ -> *
diff --git a/testsuite/tests/perf/compiler/T13035.stderr b/testsuite/tests/perf/compiler/T13035.stderr
index 3dca3d71f2..50ee3a64aa 100644
--- a/testsuite/tests/perf/compiler/T13035.stderr
+++ b/testsuite/tests/perf/compiler/T13035.stderr
@@ -1,4 +1,6 @@
 
 T13035.hs:144:28: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘'[ 'Author] :: [Fields]’
-    • In the type signature: g :: MyRec RecipeFormatter _
+    • In the second argument of ‘MyRec’, namely ‘_’
+      In the type ‘MyRec RecipeFormatter _’
+      In the type signature: g :: MyRec RecipeFormatter _
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index 487b006ec1..f85cf66d79 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -6,8 +6,9 @@ T14172.hs:6:46: error:
                  traverseCompose :: (a -> f b) -> g a -> f (h a')
                at T14172.hs:7:1-46
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature:
-        traverseCompose :: (a -> f b) -> g a -> f (h _)
+    • In the first argument of ‘h’, namely ‘_’
+      In the first argument of ‘f’, namely ‘(h _)’
+      In the type ‘(a -> f b) -> g a -> f (h _)’
 
 T14172.hs:7:19: error:
     • Occurs check: cannot construct the infinite type: a ~ g'1 a
diff --git a/testsuite/tests/polykinds/T14265.stderr b/testsuite/tests/polykinds/T14265.stderr
index 43366fccb7..fa951ad920 100644
--- a/testsuite/tests/polykinds/T14265.stderr
+++ b/testsuite/tests/polykinds/T14265.stderr
@@ -1,24 +1,30 @@
 
 T14265.hs:7:12: error:
-    • Found type wildcard ‘_’ standing for ‘w :: k’
-      Where: ‘k’, ‘w’ are rigid type variables bound by
-               the inferred type of f :: proxy w -> ()
+    • Found type wildcard ‘_’ standing for ‘_ :: k’
+      Where: ‘k’, ‘_’ are rigid type variables bound by
+               the inferred type of f :: proxy _ -> ()
                at T14265.hs:8:1-8
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: f :: proxy _ -> ()
+    • In the first argument of ‘proxy’, namely ‘_’
+      In the type ‘proxy _ -> ()’
+      In the type signature: f :: proxy _ -> ()
 
 T14265.hs:10:15: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of foo :: StateT w w1 ()
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred type of foo :: StateT _ _1 ()
                at T14265.hs:11:1-15
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: foo :: StateT _ _ ()
+    • In the first argument of ‘StateT’, namely ‘_’
+      In the type ‘StateT _ _ ()’
+      In the type signature: foo :: StateT _ _ ()
 
 T14265.hs:10:17: error:
-    • Found type wildcard ‘_’ standing for ‘w1 :: * -> *’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of foo :: StateT w w1 ()
+    • Found type wildcard ‘_’ standing for ‘_1 :: * -> *’
+      Where: ‘_1’ is a rigid type variable bound by
+               the inferred type of foo :: StateT _ _1 ()
                at T14265.hs:11:1-15
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: foo :: StateT _ _ ()
+    • In the second argument of ‘StateT’, namely ‘_’
+      In the type ‘StateT _ _ ()’
+      In the type signature: foo :: StateT _ _ ()
diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs
index 2a8b3b4ab6..2237aba651 100644
--- a/testsuite/tests/th/ClosedFam2TH.hs
+++ b/testsuite/tests/th/ClosedFam2TH.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds, TypeApplications #-}
 
 module ClosedFam2 where
 
@@ -12,12 +12,12 @@ $( return [ ClosedTypeFamilyD
                 ( TyVarSig (KindedTV (mkName "r") (VarT (mkName "k"))))
                 Nothing)
               [ TySynEqn Nothing
-                         [ (VarT (mkName "a"))
-                         , (VarT (mkName "a")) ]
+                         (AppT (AppT (ConT (mkName "Equals")) (VarT (mkName "a")))
+                               (VarT (mkName "a")))
                          (ConT (mkName "Int"))
               , TySynEqn Nothing
-                         [ (VarT (mkName "a"))
-                         , (VarT (mkName "b")) ]
+                         (AppT (AppT (ConT (mkName "Equals")) (VarT (mkName "a")))
+                               (VarT (mkName "b")))
                          (ConT (mkName "Bool")) ] ])
 
 a :: Equals b b
@@ -25,3 +25,25 @@ a = (5 :: Int)
 
 b :: Equals Int Bool
 b = False
+
+$( return [ ClosedTypeFamilyD
+               (TypeFamilyHead
+                (mkName "Foo")
+                [ KindedTV (mkName "a") (VarT (mkName "k"))]
+                (KindSig StarT ) Nothing )
+                [ TySynEqn Nothing
+                           (AppT (AppKindT (ConT (mkName "Foo")) StarT)
+                                 (VarT (mkName "a")))
+                           (ConT (mkName "Int"))
+                , TySynEqn Nothing
+                           (AppT (AppKindT (ConT (mkName "Foo")) (AppT (AppT ArrowT StarT) (StarT)))
+                                 (VarT (mkName "a")))
+                           (ConT (mkName "Bool")) ] ])
+c :: Foo Int
+c = 5
+
+d :: Foo Bool
+d = 6
+
+e :: Foo Maybe
+e = False
diff --git a/testsuite/tests/th/T12045TH1.hs b/testsuite/tests/th/T12045TH1.hs
new file mode 100644
index 0000000000..c16bab29f9
--- /dev/null
+++ b/testsuite/tests/th/T12045TH1.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds
+             , TypeInType, TypeApplications, TypeFamilies  #-}
+
+module T12045TH1 where
+import Data.Kind
+import Language.Haskell.TH hiding (Type)
+
+$([d| type family F (a :: k) :: Type where
+                     F @Type Int = Bool
+                     F @(Type->Type) Maybe = Char |])
+
+
+$([d| data family D (a :: k) |])
+
+$([d| data instance D @Type a = DBool |])
+
+$([d| data instance D @(Type -> Type) b = DChar |])
diff --git a/testsuite/tests/th/T12045TH1.stderr b/testsuite/tests/th/T12045TH1.stderr
new file mode 100644
index 0000000000..fb4bf1a302
--- /dev/null
+++ b/testsuite/tests/th/T12045TH1.stderr
@@ -0,0 +1,18 @@
+T12045TH1.hs:(8,3)-(10,52): Splicing declarations
+    [d| type family F (a :: k) :: Type where
+          F @Type Int = Bool
+          F @(Type -> Type) Maybe = Char |]
+  ======>
+    type family F (a :: k) :: Type where
+      F @Type Int = Bool
+      F @Type -> Type Maybe = Char
+T12045TH1.hs:13:3-31: Splicing declarations
+    [d| data family D (a :: k) |] ======> data family D (a :: k)
+T12045TH1.hs:15:3-40: Splicing declarations
+    [d| data instance D @Type a = DBool |]
+  ======>
+    data instance D @Type a = DBool
+T12045TH1.hs:17:3-50: Splicing declarations
+    [d| data instance D @(Type -> Type) b = DChar |]
+  ======>
+    data instance D @Type -> Type b = DChar
diff --git a/testsuite/tests/th/T12045TH2.hs b/testsuite/tests/th/T12045TH2.hs
new file mode 100644
index 0000000000..21d04cb826
--- /dev/null
+++ b/testsuite/tests/th/T12045TH2.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TemplateHaskell, TypeApplications, PolyKinds
+             , TypeFamilies, DataKinds #-}
+
+module T12045TH2 where
+
+import Data.Kind
+import Language.Haskell.TH hiding (Type)
+import System.IO
+
+type family Foo (a :: k) :: Type where
+  Foo @Type a = Bool
+
+type family Baz (a :: k)
+type instance Baz @(Type->Type->Type) a = Char
+
+$( do FamilyI foo@(ClosedTypeFamilyD (TypeFamilyHead _ tvbs1 res1 m_kind1)
+                   [TySynEqn (Just bndrs1) (AppT _ lhs1) rhs1])
+              [] <- reify ''Foo
+      FamilyI baz@(OpenTypeFamilyD (TypeFamilyHead _ tvbs2 res2 m_kind2))
+              [inst@(TySynInstD (TySynEqn (Just bndrs2) (AppT _ lhs2) rhs2))] <- reify ''Baz
+      runIO $ putStrLn $ pprint foo
+      runIO $ putStrLn $ pprint baz
+      runIO $ putStrLn $ pprint inst
+      runIO $ hFlush stdout
+      return [ ClosedTypeFamilyD
+                 (TypeFamilyHead (mkName "Foo'") tvbs1 res1 m_kind1)
+                 [TySynEqn (Just bndrs1) (AppT (ConT (mkName "Foo'")) lhs1) rhs1]
+             , OpenTypeFamilyD
+                 (TypeFamilyHead (mkName "Baz'") tvbs2 res2 m_kind2)
+             , TySynInstD (TySynEqn (Just bndrs2) (AppT (ConT (mkName "Baz'")) lhs2) rhs2)] )
diff --git a/testsuite/tests/th/T12045TH2.stderr b/testsuite/tests/th/T12045TH2.stderr
new file mode 100644
index 0000000000..ce626e5e01
--- /dev/null
+++ b/testsuite/tests/th/T12045TH2.stderr
@@ -0,0 +1,5 @@
+type family T12045TH2.Foo (a_0 :: k_1) :: * where
+    forall (a_2 :: *). T12045TH2.Foo (a_2 :: *) = GHC.Types.Bool
+type family T12045TH2.Baz (a_0 :: k_1) :: *
+type instance forall (a_0 :: * ->
+                             * -> *). T12045TH2.Baz (a_0 :: * -> * -> *) = GHC.Types.Char
diff --git a/testsuite/tests/th/T12503.hs b/testsuite/tests/th/T12503.hs
index eef302c429..78175bcf04 100644
--- a/testsuite/tests/th/T12503.hs
+++ b/testsuite/tests/th/T12503.hs
@@ -21,9 +21,9 @@ 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))
+                    (conT ''C2 `appT` return tyVar)
                     []
      return [d])
diff --git a/testsuite/tests/th/T13618.hs b/testsuite/tests/th/T13618.hs
index 1156aada39..7ef6e4e9ea 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 (ConT _) (AppT _ (VarT v1))) _
+                                       [NormalC _ [(_, VarT v2)]] _
                            -> v1 == v2
-                         NewtypeInstD _ _ _ [AppT _ (VarT v1)] _
-                                            (NormalC _ [(_, VarT v2)]) _
+                         NewtypeInstD _ _ (AppT (ConT _) (AppT _ (VarT v1))) _
+                                          (NormalC _ [(_, VarT v2)]) _
                            -> v1 == v2
                          _ -> error "Not a data or newtype instance")
               insts)
diff --git a/testsuite/tests/th/T15360b.stderr b/testsuite/tests/th/T15360b.stderr
index 8175c12556..aa3f6d93de 100644
--- a/testsuite/tests/th/T15360b.stderr
+++ b/testsuite/tests/th/T15360b.stderr
@@ -1,20 +1,20 @@
 
 T15360b.hs:10:14: error:
-    • Expected kind ‘* -> k4’, but ‘Type’ has kind ‘*’
+    • Expected kind ‘* -> k3’, but ‘Type’ has kind ‘*’
     • In the first argument of ‘Proxy’, namely ‘(Type Double)’
       In the type signature: x :: Proxy (Type Double)
 
 T15360b.hs:13:14: error:
-    • Expected kind ‘* -> k3’, but ‘1’ has kind ‘GHC.Types.Nat’
+    • Expected kind ‘* -> k2’, but ‘1’ has kind ‘GHC.Types.Nat’
     • In the first argument of ‘Proxy’, namely ‘(1 Int)’
       In the type signature: y :: Proxy (1 Int)
 
 T15360b.hs:16:14: error:
-    • Expected kind ‘* -> k2’, but ‘Constraint’ has kind ‘*’
+    • Expected kind ‘* -> k1’, but ‘Constraint’ has kind ‘*’
     • In the first argument of ‘Proxy’, namely ‘(Constraint Bool)’
       In the type signature: z :: Proxy (Constraint Bool)
 
 T15360b.hs:19:14: error:
-    • Expected kind ‘* -> k1’, but ‘'[]’ has kind ‘[k0]’
+    • Expected kind ‘* -> k0’, but ‘'[]’ has kind ‘[a0]’
     • In the first argument of ‘Proxy’, namely ‘('[] Int)’
       In the type signature: w :: Proxy ('[] Int)
diff --git a/testsuite/tests/th/T15362.hs b/testsuite/tests/th/T15362.hs
new file mode 100644
index 0000000000..183f887252
--- /dev/null
+++ b/testsuite/tests/th/T15362.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators, DataKinds #-}
+
+module T15362 where
+
+data Nat = Zero | Succ Nat
+
+$( [d| type family a + b where
+         Maybe Zero b = b
+         Succ a + b = Succ (a + b) |] )
diff --git a/testsuite/tests/th/T15362.stderr b/testsuite/tests/th/T15362.stderr
new file mode 100644
index 0000000000..0ec2dd8e48
--- /dev/null
+++ b/testsuite/tests/th/T15362.stderr
@@ -0,0 +1,10 @@
+
+T15362.hs:8:10: error:
+    • Mismatched type name in type family instance.
+        Expected: +
+          Actual: Maybe
+      In the declaration for type family ‘+’
+    • In the Template Haskell quotation
+        [d| type family a + b where
+              Maybe Zero b = b
+              Succ a + b = Succ (a + b) |]
diff --git a/testsuite/tests/th/T5886a.hs b/testsuite/tests/th/T5886a.hs
index 5756fcc513..66992014f9 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 Nothing [ConT ''Int] (ConT ''Int))]]
+bang = return [InstanceD Nothing [] (AppT (ConT ''C) (ConT ''Int))
+                [TySynInstD (TySynEqn Nothing (AppT (ConT ''AT) (ConT ''Int)) (ConT ''Int))]]
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
index 6b7b67d5a9..d0f448b80a 100644
--- a/testsuite/tests/th/T6018th.hs
+++ b/testsuite/tests/th/T6018th.hs
@@ -19,23 +19,18 @@ $( return
        (Just $ InjectivityAnn (mkName "result")
                              [(mkName "a"), (mkName "b"), (mkName "c") ]))
    , TySynInstD
-       (mkName "F")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Int"), ConT (mkName "Char")
-                 , ConT (mkName "Bool")]
-                 ( ConT (mkName "Bool")))
+       (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "F")) (ConT (mkName "Int")))
+                       (ConT (mkName "Char"))) (ConT (mkName "Bool")))
+                 (ConT (mkName "Bool")))
+
    , TySynInstD
-       (mkName "F")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Char"), ConT (mkName "Bool")
-                 , ConT (mkName "Int")]
-                 ( ConT (mkName "Int")))
+       (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "F")) (ConT (mkName "Char")))
+                       (ConT (mkName "Bool"))) (ConT (mkName "Int")))
+                 (ConT (mkName "Int")))
    , TySynInstD
-       (mkName "F")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Bool"), ConT (mkName "Int")
-                 , ConT (mkName "Char")]
-                 ( ConT (mkName "Char")))
+       (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "F")) (ConT (mkName "Bool")))
+                       (ConT (mkName "Int"))) (ConT (mkName "Char")))
+                 (ConT (mkName "Char")))
    ] )
 
 -- this is injective - a type variables mentioned on LHS is not mentioned on RHS
@@ -50,10 +45,9 @@ $( return
        (TyVarSig (PlainTV (mkName "r")))
        (Just $ InjectivityAnn (mkName "r") [mkName "a"]))
    , TySynInstD
-       (mkName "J")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Int"), VarT (mkName "b") ]
-                 ( ConT (mkName "Int")))
+       (TySynEqn Nothing (AppT (AppT (ConT (mkName "J")) (ConT (mkName "Int")))
+                       (VarT (mkName "b")))
+                 (ConT (mkName "Char")))
    ] )
 
 -- Closed type families
@@ -70,18 +64,18 @@ $( return
        , KindedTV (mkName "c") StarT ]
        (TyVarSig (PlainTV (mkName "r")))
        (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")]))
-       [ TySynEqn Nothing
-                  [ ConT (mkName "Int"), ConT (mkName "Char")
-                  , ConT (mkName "Bool")]
-                  ( ConT (mkName "Bool"))
-       , TySynEqn Nothing
-                  [ ConT (mkName "Int"), ConT (mkName "Char")
-                  , ConT (mkName "Int")]
-                  ( ConT (mkName "Bool"))
-       , TySynEqn Nothing
-                  [ ConT (mkName "Bool"), ConT (mkName "Int")
-                  , ConT (mkName "Int")]
-                  ( ConT (mkName "Int"))
+
+       [ TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "I")) (ConT (mkName "Int")))
+                                      (ConT (mkName "Char"))) (ConT (mkName "Bool")))
+                          (ConT (mkName "Bool"))
+
+       , TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "I")) (ConT (mkName "Int")))
+                                      (ConT (mkName "Char"))) (ConT (mkName "Int")))
+                          (ConT (mkName "Bool"))
+
+       , TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "I")) (ConT (mkName "Bool")))
+                                      (ConT (mkName "Int"))) (ConT (mkName "Int")))
+                          (ConT (mkName "Int"))
        ]
    ] )
 
@@ -108,22 +102,19 @@ $( return
        (TyVarSig (PlainTV (mkName "r")))
        (Just $ InjectivityAnn (mkName "r")
                              [(mkName "a"), (mkName "b") ]))
+
    , TySynInstD
-       (mkName "H")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Int"), ConT (mkName "Char")
-                 , ConT (mkName "Bool")]
-                 ( ConT (mkName "Bool")))
+         (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "H")) (ConT (mkName "Int")))
+                                       (ConT (mkName "Char"))) (ConT (mkName "Bool")))
+                           (ConT (mkName "Bool")))
+
    , TySynInstD
-       (mkName "H")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Int"), ConT (mkName "Int")
-                 , ConT (mkName "Int")]
-                 ( ConT (mkName "Bool")))
+         (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "H")) (ConT (mkName "Int")))
+                                       (ConT (mkName "Int"))) (ConT (mkName "Int")))
+                           (ConT (mkName "Bool")))
+
    , TySynInstD
-       (mkName "H")
-       (TySynEqn Nothing
-                 [ ConT (mkName "Bool"), ConT (mkName "Int")
-                 , ConT (mkName "Int")]
-                 ( ConT (mkName "Int")))
+         (TySynEqn Nothing (AppT (AppT (AppT (ConT (mkName "H")) (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 9566b1acd5..56e3f471f7 100644
--- a/testsuite/tests/th/T6018th.stderr
+++ b/testsuite/tests/th/T6018th.stderr
@@ -1,5 +1,5 @@
 
-T6018th.hs:104:4:
+T6018th.hs:98:4: error:
     Type family equations violate injectivity annotation:
-      H Int Int Int = Bool -- Defined at T6018th.hs:104:4
-      H Int Char Bool = Bool -- Defined at T6018th.hs:104:4
+      H Int Int Int = Bool -- Defined at T6018th.hs:98:4
+      H Int Char Bool = Bool -- Defined at T6018th.hs:98:4
diff --git a/testsuite/tests/th/T7532a.hs b/testsuite/tests/th/T7532a.hs
index 8f686fe206..d28a59e87c 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 Nothing [ConT ''Int] Nothing [
+         DataInstD [] Nothing (AppT (ConT ''D) (ConT ''Int)) Nothing [
              NormalC (mkName "T") []] []]]
diff --git a/testsuite/tests/th/T8884.hs b/testsuite/tests/th/T8884.hs
index cdc1a93c09..168f529ec4 100644
--- a/testsuite/tests/th/T8884.hs
+++ b/testsuite/tests/th/T8884.hs
@@ -11,16 +11,18 @@ type family Foo a = r | r -> a where
 type family Baz (a :: k) = (r :: k) | r -> a
 type instance Baz x = x
 
-$( do FamilyI foo@(ClosedTypeFamilyD (TypeFamilyHead _ tvbs1 res1 m_kind1) eqs1)
+$( do FamilyI foo@(ClosedTypeFamilyD (TypeFamilyHead _ tvbs1 res1 m_kind1)
+                   [TySynEqn (Just bndrs1) (AppT _ lhs1) rhs1])
               [] <- reify ''Foo
       FamilyI baz@(OpenTypeFamilyD (TypeFamilyHead _ tvbs2 res2 m_kind2))
-              [inst@(TySynInstD _ eqn2)] <- reify ''Baz
+              [inst@(TySynInstD (TySynEqn (Just bndrs2) (AppT _ lhs2) rhs2))] <- reify ''Baz
       runIO $ putStrLn $ pprint foo
       runIO $ putStrLn $ pprint baz
       runIO $ putStrLn $ pprint inst
       runIO $ hFlush stdout
       return [ ClosedTypeFamilyD
-                 (TypeFamilyHead (mkName "Foo'") tvbs1 res1 m_kind1) eqs1
+                 (TypeFamilyHead (mkName "Foo'") tvbs1 res1 m_kind1)
+                 [TySynEqn (Just bndrs1) (AppT (ConT (mkName "Foo'")) lhs1) rhs1]
              , OpenTypeFamilyD
                  (TypeFamilyHead (mkName "Baz'") tvbs2 res2 m_kind2)
-             , TySynInstD (mkName "Baz'") eqn2 ] )
+             , TySynInstD (TySynEqn (Just bndrs2) (AppT (ConT (mkName "Baz'")) lhs2) rhs2)] )
diff --git a/testsuite/tests/th/TH_TyInstWhere2.hs b/testsuite/tests/th/TH_TyInstWhere2.hs
index 47fedad8da..bfd0975b8f 100644
--- a/testsuite/tests/th/TH_TyInstWhere2.hs
+++ b/testsuite/tests/th/TH_TyInstWhere2.hs
@@ -1,8 +1,9 @@
-{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies #-}
+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies, TypeApplications #-}
 
 module TH_TyInstWhere2 where
 
-import Language.Haskell.TH
+import Language.Haskell.TH hiding (Type)
+import Data.Kind
 
 $( do { decs <- [d| type family F (a :: k) (b :: k) :: Bool where
                       F a a = True
@@ -10,4 +11,8 @@ $( do { decs <- [d| type family F (a :: k) (b :: k) :: Bool where
       ; reportWarning (pprint decs)
       ; return [] })
 
-
+$( do { dec1 <- [d| type family F1 (a :: k) :: Type where
+                      F1 @Type Int = Bool
+                      F1 @Bool 'False = Char |]
+      ; reportWarning (pprint dec1)
+      ; return [] })
diff --git a/testsuite/tests/th/TH_TyInstWhere2.stderr b/testsuite/tests/th/TH_TyInstWhere2.stderr
index 17caf61bad..717fb0e170 100644
--- a/testsuite/tests/th/TH_TyInstWhere2.stderr
+++ b/testsuite/tests/th/TH_TyInstWhere2.stderr
@@ -1,5 +1,10 @@
 
-TH_TyInstWhere2.hs:7:4: Warning:
+TH_TyInstWhere2.hs:8:4: warning:
     type family F_0 (a_1 :: k_2) (b_3 :: k_2) :: GHC.Types.Bool where
     F_0 a_4 a_4 = 'GHC.Types.True
     F_0 a_5 b_6 = 'GHC.Types.False
+
+TH_TyInstWhere2.hs:14:4: warning:
+    type family F1_0 (a_1 :: k_2) :: * where
+    F1_0 @* GHC.Types.Int = GHC.Types.Bool
+    F1_0 @GHC.Types.Bool 'GHC.Types.False = GHC.Types.Char
diff --git a/testsuite/tests/th/TH_reifyDecl1.hs b/testsuite/tests/th/TH_reifyDecl1.hs
index c4ae3c065d..5437837611 100644
--- a/testsuite/tests/th/TH_reifyDecl1.hs
+++ b/testsuite/tests/th/TH_reifyDecl1.hs
@@ -1,8 +1,9 @@
 -- test reification of data declarations
 
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilies, TypeApplications, PolyKinds #-}
 module TH_reifyDecl1 where
 
+import Data.Kind as K
 import System.IO
 import Language.Haskell.TH
 import Text.PrettyPrint.HughesPJ
@@ -60,6 +61,10 @@ data family DF1 a
 data family DF2 a
 data instance DF2 Bool = DBool
 
+data family DF3 (a :: k)
+data instance DF3 @K.Type a = DF3Bool
+data instance DF3 @(K.Type -> K.Type) b = DF3Char
+
 $(return [])
 
 test :: ()
@@ -83,4 +88,5 @@ test = $(let
           ; display ''TF2
           ; display ''DF1
           ; display ''DF2
+          ; display ''DF3
           ; [| () |] })
diff --git a/testsuite/tests/th/TH_reifyDecl1.stderr b/testsuite/tests/th/TH_reifyDecl1.stderr
index b18089b3a0..5ae01471f3 100644
--- a/testsuite/tests/th/TH_reifyDecl1.stderr
+++ b/testsuite/tests/th/TH_reifyDecl1.stderr
@@ -4,13 +4,13 @@ data TH_reifyDecl1.R (a_0 :: *)
 data TH_reifyDecl1.List (a_0 :: *)
     = TH_reifyDecl1.Nil
     | TH_reifyDecl1.Cons a_0 (TH_reifyDecl1.List a_0)
-data TH_reifyDecl1.Tree (a_0 :: *)
+data TH_reifyDecl1.Tree (a_0 :: k_1)
     = TH_reifyDecl1.Leaf
     | (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 (a_0 :: *) .
-                                                           TH_reifyDecl1.Tree a_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
 class TH_reifyDecl1.C1 (a_0 :: *)
@@ -18,13 +18,13 @@ class TH_reifyDecl1.C1 (a_0 :: *)
 class TH_reifyDecl1.C2 (a_0 :: *)
     where TH_reifyDecl1.m2 :: a_0 -> GHC.Types.Int
 instance TH_reifyDecl1.C2 GHC.Types.Int
-class TH_reifyDecl1.C3 (a_0 :: *)
-    where type TH_reifyDecl1.AT1 (a_0 :: *) :: *
-          data TH_reifyDecl1.AT2 (a_0 :: *) :: *
+class TH_reifyDecl1.C3 (a_0 :: k_1)
+    where type TH_reifyDecl1.AT1 (a_0 :: k_1) :: *
+          data TH_reifyDecl1.AT2 (a_0 :: k_1) :: *
 instance TH_reifyDecl1.C3 GHC.Types.Int
-type family TH_reifyDecl1.AT1 (a_0 :: *) :: *
+type family TH_reifyDecl1.AT1 (a_0 :: k_1) :: *
 type instance TH_reifyDecl1.AT1 GHC.Types.Int = GHC.Types.Bool
-data family TH_reifyDecl1.AT2 (a_0 :: *) :: *
+data family TH_reifyDecl1.AT2 (a_0 :: k_1) :: *
 data instance TH_reifyDecl1.AT2 GHC.Types.Int
     = TH_reifyDecl1.AT2Int
 type family TH_reifyDecl1.TF1 (a_0 :: *) :: *
@@ -34,3 +34,9 @@ data family TH_reifyDecl1.DF1 (a_0 :: *) :: *
 data family TH_reifyDecl1.DF2 (a_0 :: *) :: *
 data instance TH_reifyDecl1.DF2 GHC.Types.Bool
     = TH_reifyDecl1.DBool
+data family TH_reifyDecl1.DF3 (a_0 :: k_1) :: *
+data instance forall (a_2 :: *). TH_reifyDecl1.DF3 (a_2 :: *)
+    = TH_reifyDecl1.DF3Bool
+data instance forall (b_3 :: * ->
+                             *). TH_reifyDecl1.DF3 (b_3 :: * -> *)
+    = TH_reifyDecl1.DF3Char
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 881ba81b18..7f420fb6e7 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -367,6 +367,8 @@ test('T11484', normal, compile, ['-v0'])
 test('T11629', normal, compile, ['-v0'])
 
 test('T8761', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('T12045TH1', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('T12045TH2', normal, compile, ['-v0'])
 test('T12130', [], multimod_compile,
      ['T12130', '-v0 ' + config.ghc_th_way_flags])
 test('T12387', normal, compile_fail, ['-v0'])
@@ -435,6 +437,7 @@ test('T15331', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T15365', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T15360a', normal, compile, [''])
 test('T15360b', normal, compile_fail, [''])
+test('T15362', normal, compile_fail,['-v0'])
 # Note: T9693 should be only_ways(['ghci']) once it's fixed.
 test('T9693', expect_broken(9693), ghci_script, ['T9693.script'])
 test('T14471', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T10072.stderr b/testsuite/tests/typecheck/should_compile/T10072.stderr
index 848c9158e8..ad7fe2602a 100644
--- a/testsuite/tests/typecheck/should_compile/T10072.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10072.stderr
@@ -2,7 +2,9 @@
 T10072.hs:3:31: error:
     • Found type wildcard ‘_’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
-               the RULE "map/empty" at T10072.hs:3:1-47
+               the RULE "map/empty"
+               at T10072.hs:3:1-47
       To use the inferred type, enable PartialTypeSignatures
-    • In a RULE for ‘f’: a -> _
+    • In the type ‘a -> _’
+      In a RULE for ‘f’: a -> _
       When checking the transformation rule "map/empty"
diff --git a/testsuite/tests/typecheck/should_compile/T12045a.hs b/testsuite/tests/typecheck/should_compile/T12045a.hs
new file mode 100644
index 0000000000..469a3307a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12045a.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE PolyKinds, GADTs, TypeApplications, TypeInType, DataKinds,
+    RankNTypes, ConstraintKinds, TypeFamilies #-}
+
+module T12045a where
+
+import Data.Kind
+import Data.Typeable
+
+data T (f :: k -> Type) a = MkT (f a)
+
+newtype TType f a= MkTType (T @Type f a)
+
+t1 :: TType Maybe Bool
+t1 = MkTType (MkT (Just True))
+
+t2 :: TType Maybe a
+t2 = MkTType (MkT Nothing)
+
+data Nat = O | S Nat
+
+data T1 :: forall k1 k2. k1 -> k2 -> Type where
+  MkT1 :: T1 a b
+
+x :: T1 @_ @Nat False n
+x = MkT1
+
+-- test from trac 12045
+type Cat k = k -> k -> Type
+
+data FreeCat :: Cat k -> Cat k where
+  Nil  :: FreeCat f a a
+  Cons :: f a b -> FreeCat f b c -> FreeCat f a c
+
+liftCat :: f a b -> FreeCat f a b
+liftCat x = Cons x Nil
+
+data Node = Unit | N
+
+data NatGraph :: Cat Node where
+  One  :: NatGraph Unit N
+  Succ :: NatGraph N    N
+
+one :: (FreeCat @Node NatGraph) Unit N
+one = liftCat One
+
+type Typeable1 = Typeable @(Type -> Type)
+type Typeable2 = Typeable @(Type -> Type -> Type)
+type Typeable3 = Typeable @(Cat Bool)
+
+type family F a where
+  F Type = Type -> Type
+  F (Type -> Type) = Type
+  F other = other
+
+data T2 :: F k -> Type
+
+foo :: T2 @Type Maybe -> T2 @(Type -> Type) Int -> Type
+foo a b = undefined
+
+data family D (a :: k)
+data instance D @Type a = DBool
+data instance D @(Type -> Type) b = DChar
+
+class C a where
+  tc :: (D a) -> Int
+
+instance C Int where
+  tc DBool = 5
+
+instance C Bool where
+  tc DBool = 6
+
+instance C Maybe where
+  tc DChar = 7
+
+-- Tests from D5229
+data P a = MkP
+type MkPTrue = MkP @Bool
+
+type BoolEmpty = '[] @Bool
+
+type family F1 (a :: k) :: Type
+type G2 (a :: Bool) = F1 @Bool a
diff --git a/testsuite/tests/typecheck/should_compile/T14366.hs b/testsuite/tests/typecheck/should_compile/T14366.hs
new file mode 100644
index 0000000000..56abad5d30
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14366.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T14366 where
+import Data.Kind
+import Data.Type.Equality
+
+type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
+  Cast _ _ Refl x = x
+
+type family F (a :: Type) :: Type where
+  F (a :: _) = a
diff --git a/testsuite/tests/typecheck/should_compile/T15788.hs b/testsuite/tests/typecheck/should_compile/T15788.hs
new file mode 100644
index 0000000000..732afb6932
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15788.hs
@@ -0,0 +1,11 @@
+{-# Language RankNTypes       #-}
+{-# Language GADTs            #-}
+{-# Language TypeApplications #-}
+{-# Language PolyKinds        #-}
+
+{-# Options_GHC -dcore-lint #-}
+module T15788 where
+import Data.Kind
+
+data A :: forall k. Type where
+ MkA :: A @k
diff --git a/testsuite/tests/typecheck/should_compile/T15793.hs b/testsuite/tests/typecheck/should_compile/T15793.hs
new file mode 100644
index 0000000000..4e96d83f10
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15793.hs
@@ -0,0 +1,18 @@
+{-# Language RankNTypes       #-}
+{-# Language TypeFamilies     #-}
+{-# Language TypeApplications #-}
+{-# Language PolyKinds        #-}
+
+module T15793 where
+import Data.Kind
+
+type family
+  F1 (a :: Type) :: Type where
+  F1 a = Maybe a
+
+f1 :: F1 a
+f1 = Nothing
+
+type family
+  F2 :: forall (a :: Type). Type where
+  F2 @a = Maybe a
diff --git a/testsuite/tests/typecheck/should_compile/T15807a.hs b/testsuite/tests/typecheck/should_compile/T15807a.hs
new file mode 100644
index 0000000000..7aa37358a8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15807a.hs
@@ -0,0 +1,12 @@
+{-# Language RankNTypes       #-}
+{-# Language TypeApplications #-}
+{-# Language PolyKinds        #-}
+{-# Language GADTs            #-}
+
+module T15807a where
+import Data.Kind
+
+data
+  App :: forall (f :: Type -> Type). Type -> Type
+  where
+  MkApp :: f a -> App @f a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3fed2a9466..9d1fc185d0 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -511,6 +511,7 @@ test('T11811', normal, compile, [''])
 test('T11793', normal, compile, [''])
 test('T11348', normal, compile, [''])
 test('T11947', normal, compile, [''])
+test('T12045a', normal, compile, [''])
 test('T12064', [], multimod_compile, ['T12064', '-v0'])
 test('ExPat', normal, compile, [''])
 test('ExPatFail', normal, compile_fail, [''])
@@ -606,6 +607,7 @@ test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits']
 # output we expect (T13032.stderr).
 test('T13032', omit_ways(['hpc', 'profasm']), compile, [''])
 test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits'])
+test('T14366', normal, compile, [''])
 test('T14732', normal, compile, [''])
 test('T14774', [], run_command, ['$MAKE -s --no-print-directory T14774'])
 test('T14763', normal, compile, [''])
@@ -626,6 +628,9 @@ test('T15050', normal, compile, [''])
 test('T14735', normal, compile, [''])
 test('T15180', normal, compile, [''])
 test('T15232', normal, compile, [''])
+test('T15788', normal, compile, [''])
+test('T15793', normal, compile, [''])
+test('T15807a', normal, compile, [''])
 test('T13833', normal, compile, [''])
 test('T14185', expect_broken(14185), compile, [''])
 
diff --git a/testsuite/tests/typecheck/should_fail/T12045b.hs b/testsuite/tests/typecheck/should_fail/T12045b.hs
new file mode 100644
index 0000000000..19191c05f1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12045b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeApplications #-}
+
+module T12045b where
+
+import Data.Kind
+
+x :: Int @Type
+x = 5
diff --git a/testsuite/tests/typecheck/should_fail/T12045b.stderr b/testsuite/tests/typecheck/should_fail/T12045b.stderr
new file mode 100644
index 0000000000..fcb65b133d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12045b.stderr
@@ -0,0 +1,5 @@
+
+T12045b.hs:7:6: error:
+    • Cannot apply function of kind ‘*’
+      to visible kind argument ‘Type’
+    • In the type signature: x :: Int @Type
diff --git a/testsuite/tests/typecheck/should_fail/T12045c.hs b/testsuite/tests/typecheck/should_fail/T12045c.hs
new file mode 100644
index 0000000000..56c2d15abc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12045c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, TypeApplications, KindSignatures, DataKinds, GADTs
+             , TypeFamilies, RankNTypes #-}
+
+module T12045c where
+import Data.Kind
+
+type family F a where
+  F @Type a = Bool
+  F @(Type -> Type) b = Char
diff --git a/testsuite/tests/typecheck/should_fail/T12045c.stderr b/testsuite/tests/typecheck/should_fail/T12045c.stderr
new file mode 100644
index 0000000000..86a51a49ac
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12045c.stderr
@@ -0,0 +1,5 @@
+
+T12045c.hs:8:3: error:
+    • Cannot apply function of kind ‘k0 -> k1’
+      to visible kind argument ‘Type’
+    • In the type family declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/T13819.stderr b/testsuite/tests/typecheck/should_fail/T13819.stderr
index ab818f399b..89959cba39 100644
--- a/testsuite/tests/typecheck/should_fail/T13819.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13819.stderr
@@ -1,8 +1,8 @@
 
 T13819.hs:12:10: error:
-    • Couldn't match type ‘w0 -> A w0’ with ‘A a’
+    • Couldn't match type ‘_0 -> A _0’ with ‘A a’
       Expected type: a -> A a
-        Actual type: (w1 -> WrappedMonad A w2) (w0 -> A w0)
+        Actual type: (_1 -> WrappedMonad A _2) (_0 -> A _0)
     • In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
       In an equation for ‘pure’:
           pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
diff --git a/testsuite/tests/typecheck/should_fail/T15592a.hs b/testsuite/tests/typecheck/should_fail/T15592a.hs
new file mode 100644
index 0000000000..1f28c73d2a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15592a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, TypeApplications, DataKinds, RankNTypes #-}
+
+module T15592 where
+import Data.Proxy
+
+data VisProxy k (a :: k) = MkVP
+class D (a :: Proxy j) (b :: Proxy k) c where
+  meth1 :: forall z. D @j @k a b z => z -> Proxy '(a, b)
+  meth2 :: Proxy k j -> Proxy '(a, b, c)
diff --git a/testsuite/tests/typecheck/should_fail/T15592a.stderr b/testsuite/tests/typecheck/should_fail/T15592a.stderr
new file mode 100644
index 0000000000..5002b4771d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15592a.stderr
@@ -0,0 +1,8 @@
+
+T15592a.hs:8:22: error:
+    • Cannot apply function of kind ‘Proxy j
+                                     -> Proxy k -> k2 -> Constraint’
+      to visible kind argument ‘j’
+    • In the type signature:
+        meth1 :: forall z. D @j @k a b z => z -> Proxy '(a, b)
+      In the class declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/T15797.hs b/testsuite/tests/typecheck/should_fail/T15797.hs
new file mode 100644
index 0000000000..eadd8cb972
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15797.hs
@@ -0,0 +1,26 @@
+{-# Language    RankNTypes          #-}
+{-# Language    TypeFamilies        #-}
+{-# Language    ScopedTypeVariables #-}
+{-# Language    TypeApplications    #-}
+{-# Language    DataKinds           #-}
+{-# Language    PolyKinds           #-}
+{-# Language    TypeOperators       #-}
+{-# Language    GADTs               #-}
+{-# Language    FlexibleInstances   #-}
+
+module T15797 where
+import Data.Kind
+
+class Ríki (obj :: Type) where
+  type Obj :: obj -> Constraint
+  type Obj = Bæ @obj
+
+class    Bæ    (a :: k)
+instance Bæ @k (a :: k)
+
+data
+  EQ :: forall ob. ob -> ob -> Type where
+  EQ :: EQ a a
+
+instance
+  Ríki (EQ @ob)
diff --git a/testsuite/tests/typecheck/should_fail/T15797.stderr b/testsuite/tests/typecheck/should_fail/T15797.stderr
new file mode 100644
index 0000000000..04c2a5fc50
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15797.stderr
@@ -0,0 +1,6 @@
+
+T15797.hs:26:9: error:
+    • Expecting two more arguments to ‘EQ @ob’
+      Expected a type, but ‘EQ @ob’ has kind ‘ob -> ob -> *’
+    • In the first argument of ‘Ríki’, namely ‘(EQ @ob)’
+      In the instance declaration for ‘Ríki (EQ @ob)’
diff --git a/testsuite/tests/typecheck/should_fail/T15799.hs b/testsuite/tests/typecheck/should_fail/T15799.hs
new file mode 100644
index 0000000000..fe692620a6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15799.hs
@@ -0,0 +1,47 @@
+{-# Language CPP               #-}
+{-# Language DataKinds         #-}
+{-# Language RankNTypes        #-}
+{-# Language PatternSynonyms   #-}
+{-# Language TypeOperators     #-}
+{-# Language PolyKinds         #-}
+{-# Language GADTs             #-}
+{-# Language TypeFamilies      #-}
+{-# Language TypeApplications  #-}
+{-# Language FlexibleContexts  #-}
+{-# Language FlexibleInstances #-}
+{-# Language InstanceSigs      #-}
+
+module T15799 where
+import qualified GHC.TypeLits as TypeLits
+import GHC.TypeLits (Nat, KnownNat)
+import Data.Kind
+
+data Op obj = Op obj
+
+type family
+ UnOp (op_a :: Op obj) :: obj where
+ UnOp ('Op obj) = obj
+
+class
+ Ríki (obj :: Type) where
+ type (-->) :: Op obj -> obj -> Type
+ type (<--) :: obj -> Op obj -> Type
+
+ unop :: forall (a :: obj) (b :: obj). (a <-- 'Op b) -> ('Op b --> a)
+
+data (<=) :: Op Nat -> Nat -> Type where
+  LessThan :: (KnownNat (UnOp op_a), KnownNat b, UnOp op_a TypeLits.<= b)
+           => (op_a <= b)
+
+newtype (>=) :: Nat -> Op Nat -> Type where
+  Y :: (a <= b) -> (b >= a)
+
+instance Ríki Nat where
+ type (-->) = (<=)
+ type (<--) = (>=)
+
+ unop :: (a >= b) -> (b <= a)
+ unop GreaterThan = LessThan
+
+pattern GreaterThan :: () => (KnownNat (UnOp b), KnownNat a, UnOp b <= a) => a >= b
+pattern GreaterThan = Y LessThan
diff --git a/testsuite/tests/typecheck/should_fail/T15799.stderr b/testsuite/tests/typecheck/should_fail/T15799.stderr
new file mode 100644
index 0000000000..f93e043471
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15799.stderr
@@ -0,0 +1,7 @@
+
+T15799.hs:46:62: error:
+    • Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’
+    • In the first argument of ‘(<=)’, namely ‘UnOp b’
+
+T15799.hs:46:62: error:
+    Expected a constraint, but ‘UnOp b <= a’ has kind ‘*’
diff --git a/testsuite/tests/typecheck/should_fail/T15801.hs b/testsuite/tests/typecheck/should_fail/T15801.hs
new file mode 100644
index 0000000000..9b39408aef
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15801.hs
@@ -0,0 +1,53 @@
+{-# Language CPP                   #-}
+{-# Language QuantifiedConstraints #-}
+{-# Language TypeApplications      #-}
+{-# Language PolyKinds             #-}
+{-# Language TypeOperators         #-}
+{-# Language DataKinds             #-}
+{-# Language TypeFamilies          #-}
+{-# Language TypeSynonymInstances  #-}
+{-# Language FlexibleInstances     #-}
+{-# Language GADTs                 #-}
+{-# Language UndecidableInstances  #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language FlexibleContexts      #-}
+
+module Bug where
+import Data.Coerce
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+type Obj = Type
+
+class    Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
+instance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
+
+class    (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
+instance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
+
+class
+  Ríki (obj :: Obj) where
+  type (-->) :: obj -> obj -> Type
+
+  ið :: a --> (a::obj)
+
+class
+  OpOpNoOp obj
+  =>
+  OpRíki (obj :: Obj) where
+  type (<--) :: obj -> obj -> Type
+
+data Op a = Op a
+
+type family UnOp op where UnOp ('Op obj) = obj
+
+newtype Y :: Cat (Op a) where
+  Y :: (UnOp b --> UnOp a) -> Y a b
+
+instance Ríki Type where
+ type (-->) = (->)
+ ið x = x
+
+instance OpRíki (Op Type) where
+ type (<--) @(Op Type) = Y @Type
diff --git a/testsuite/tests/typecheck/should_fail/T15801.stderr b/testsuite/tests/typecheck/should_fail/T15801.stderr
new file mode 100644
index 0000000000..887c0f2a35
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15801.stderr
@@ -0,0 +1,6 @@
+
+T15801.hs:52:10: error:
+    • Couldn't match representation of type ‘UnOp op_a -> UnOp b’
+                               with that of ‘op_a --> b’
+        arising from the superclasses of an instance declaration
+    • In the instance declaration for ‘OpRíki (Op *)’
diff --git a/testsuite/tests/typecheck/should_fail/T15807.hs b/testsuite/tests/typecheck/should_fail/T15807.hs
new file mode 100644
index 0000000000..fa121d608e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15807.hs
@@ -0,0 +1,12 @@
+{-# Language RankNTypes       #-}
+{-# Language TypeApplications #-}
+{-# Language PolyKinds        #-}
+{-# Language GADTs            #-}
+
+module T15807 where
+import Data.Kind
+
+data
+  App :: forall (f :: k -> Type). k -> Type
+  where
+  MkApp :: f a -> App @f a
diff --git a/testsuite/tests/typecheck/should_fail/T15807.stderr b/testsuite/tests/typecheck/should_fail/T15807.stderr
new file mode 100644
index 0000000000..e24f5bb855
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15807.stderr
@@ -0,0 +1,16 @@
+
+T15807.hs:12:24: error:
+    • Expecting one more argument to ‘f’
+      Expected a type, but ‘f’ has kind ‘k0 -> *’
+    • In the first argument of ‘App’, namely ‘f’
+      In the type ‘App @f a’
+      In the definition of data constructor ‘MkApp’
+
+T15807.hs:12:26: error:
+    • Couldn't match kind ‘*’ with ‘k0 -> *’
+      When matching kinds
+        k0 :: *
+        f :: k0 -> *
+    • In the second argument of ‘App’, namely ‘a’
+      In the type ‘App @f a’
+      In the definition of data constructor ‘MkApp’
diff --git a/testsuite/tests/typecheck/should_fail/T15816.hs b/testsuite/tests/typecheck/should_fail/T15816.hs
new file mode 100644
index 0000000000..a9958ee38c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15816.hs
@@ -0,0 +1,8 @@
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies        #-}
+
+module T15816 where
+import Data.Kind
+
+data family U
+data instance U @Int
diff --git a/testsuite/tests/typecheck/should_fail/T15816.stderr b/testsuite/tests/typecheck/should_fail/T15816.stderr
new file mode 100644
index 0000000000..90bf2122d6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15816.stderr
@@ -0,0 +1,5 @@
+
+T15816.hs:8:1: error:
+    • Cannot apply function of kind ‘*’
+      to visible kind argument ‘Int’
+    • In the data instance declaration for ‘U’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index f0afa0d3a9..bac4d6b14e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -404,6 +404,8 @@ test('T11990b', normal, compile_fail, [''])
 test('T12035', [], multimod_compile_fail, ['T12035', '-v0'])
 test('T12035j', [extra_files(['T12035.hs', 'T12035a.hs', 'T12035.hs-boot']),
                  req_smp], multimod_compile_fail, ['T12035', '-j2 -v0'])
+test('T12045b', normal, compile_fail, [''])
+test('T12045c', normal, compile_fail, [''])
 test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
 test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
@@ -486,10 +488,16 @@ test('T15523', normal, compile_fail, ['-O'])
 test('T15527', normal, compile_fail, [''])
 test('T15552', normal, compile, [''])
 test('T15552a', normal, compile_fail, [''])
+test('T15592a', normal, compile_fail, [''])
 test('T15629', normal, compile_fail, [''])
 test('T15767', normal, compile_fail, [''])
 test('T15648', [extra_files(['T15648a.hs'])], multimod_compile_fail, ['T15648', '-v0 -fprint-equality-relations'])
 test('T15796', normal, compile_fail, [''])
+test('T15807', normal, compile_fail, [''])
 test('T15954', normal, compile_fail, [''])
 test('T15962', normal, compile_fail, [''])
 test('T16074', normal, compile_fail, [''])
+test('T15797', normal, compile_fail, [''])
+test('T15799', normal, compile_fail, [''])
+test('T15801', normal, compile_fail, [''])
+test('T15816', normal, compile_fail, [''])