diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 95646b0057be8be66e6dfe628392de93a5e3e66d..d47fd2168bbd1243b9f9f24a66a5720acbd03966 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1253,6 +1253,12 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
 
 --------- Promoted lists and tuples
 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
+  -- The '[] case is handled in tc_infer_hs_type.
+  -- See Note [Future-proofing the type checker].
+  | null tys
+  = tc_infer_hs_type_ek mode rn_ty exp_kind
+
+  | otherwise
   = do { tks <- mapM (tc_infer_lhs_type mode) tys
        ; (taus', kind) <- unifyKinds tys tks
        ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
diff --git a/testsuite/tests/ghci/scripts/T15898.stderr b/testsuite/tests/ghci/scripts/T15898.stderr
index 4fd99bbccc0d60011f4cdbe5c5c422e834a4754a..97b98bc882a3d6116026addf29cf1c377bffa4cb 100644
--- a/testsuite/tests/ghci/scripts/T15898.stderr
+++ b/testsuite/tests/ghci/scripts/T15898.stderr
@@ -18,7 +18,7 @@
       In an equation for ‘it’: it = undefined :: [(), ()]
 
 <interactive>:6:14: error: [GHC-83865]
-    • Expected a type, but ‘'( '[], '[])’ has kind ‘([k0], [k1])’
+    • Expected a type, but ‘'( '[], '[])’ has kind ‘([a0], [a1])’
     • In an expression type signature: '( '[], '[])
       In the expression: undefined :: '( '[], '[])
       In an equation for ‘it’: it = undefined :: '( '[], '[])
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 36398cc89a00316dee01e8bf32f22274a0232ccf..ea1cd3f6df0669c0437e242cb364939a3b7a473e 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -41,18 +41,18 @@
 
 <interactive>:55:41: error: [GHC-05175]
     Type family equation violates the family's injectivity annotation.
-    Type/kind variable ‘k1’
+    Type/kind variable ‘a1’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
+      PolyKindVarsF @{[a1]} @[a2] ('[] @a1) = '[] @a2
         -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error: [GHC-05175]
     Type family equation violates the family's injectivity annotation.
-    Type/kind variable ‘k1’
+    Type/kind variable ‘a1’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
+      PolyKindVars @[a1] @[a2] ('[] @a1) = '[] @a2
         -- Defined at <interactive>:60:15
 
 <interactive>:64:15: error: [GHC-05175]
diff --git a/testsuite/tests/ghci/scripts/T7939.stdout b/testsuite/tests/ghci/scripts/T7939.stdout
index 6f0ab38948762477c091bc2bb45e7f68a31d9be9..83445adc242ea998f15bcc1617b50bc531c6dda1 100644
--- a/testsuite/tests/ghci/scripts/T7939.stdout
+++ b/testsuite/tests/ghci/scripts/T7939.stdout
@@ -19,12 +19,12 @@ type family H a where
     H False = True
   	-- Defined at T7939.hs:15:1
 H :: Bool -> Bool
-type J :: forall {k}. [k] -> Bool
-type family J a where
+type J :: forall {a}. [a] -> Bool
+type family J a1 where
     J '[] = False
-  forall k (h :: k) (t :: [k]). J (h : t) = True
+  forall a (h :: a) (t :: [a]). J (h : t) = True
   	-- Defined at T7939.hs:18:1
-J :: [k] -> Bool
+J :: [a] -> Bool
 type K :: forall {a}. [a] -> Maybe a
 type family K a1 where
     K '[] = Nothing
diff --git a/testsuite/tests/typecheck/should_compile/T23543.hs b/testsuite/tests/typecheck/should_compile/T23543.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1689d023287e34362942babb0e8b883f605fcab5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T23543.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T23543 where
+
+type N :: forall a. Maybe a
+type N = ('Nothing :: forall a. Maybe a)
+
+type L :: forall a. [a]
+type L = ('[] :: forall a. [a])
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 505a2f44adb057d6b52f5a00171459dcbc2fc45e..013f44971a4b77ab82f5d3cea9e89ecccc3d2058 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -875,6 +875,7 @@ test('T23171', normal, compile, [''])
 test('T23192', normal, compile, [''])
 test('T23199', normal, compile, [''])
 test('T23156', normal, compile, [''])
+test('T23543', normal, compile, [''])
 test('T22560a', normal, compile, [''])
 test('T22560b', normal, compile, [''])
 test('T22560c', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 0c352199e1f1c6b821e2d00aec56b748f9dbd9f7..27afca2b94d98642062f94b06c800bd76fb63795 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -52,18 +52,18 @@ T6018fail.hs:53:15: error: [GHC-05175]
 
 T6018fail.hs:61:10: error: [GHC-05175]
     Type family equation violates the family's injectivity annotation.
-    Type/kind variable ‘k1’
+    Type/kind variable ‘a1’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
+      PolyKindVarsF @{[a1]} @[a2] ('[] @a1) = '[] @a2
         -- Defined at T6018fail.hs:61:10
 
 T6018fail.hs:64:15: error: [GHC-05175]
     Type family equation violates the family's injectivity annotation.
-    Type/kind variable ‘k1’
+    Type/kind variable ‘a1’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
+      PolyKindVars @[a1] @[a2] ('[] @a1) = '[] @a2
         -- Defined at T6018fail.hs:64:15
 
 T6018fail.hs:68:15: error: [GHC-05175]