"Quantification by level numbers would fail" for an ill-kinded signature

Summary

With assertions enabled, this program causes a warning about level numbers:

{-# LANGUAGE RankNTypes, PolyKinds #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module T where

import Data.Proxy

t :: Proxy (z :: forall k. a)
t = t

The warning and the kind error are as follows:

WARNING: file compiler/typecheck/TcMType.hs, line 1472
  Quantification by level numbers would fail
    Outer level = 0
    dep_tkvs = {k_a1f6[tau:0], k_a1f7[tau:0], a_a1eI[sk:1],
                k_a1f4[tau:1]}
    co_vars = co_a1f3 :: k_a1eK[tau:1]
                         ~# (forall (k :: k_a1eX[tau:1]). a_a1eI[sk:1])
    co_tvs = {a_a1eI[sk:1], k_a1eK[tau:1], k_a1eX[tau:1], co_a1f3}
    dep_kvs = [k_a1f4[tau:1]]
    dep_kvs2 = [a_a1eI[sk:1], k_a1f4[tau:1]]
    nondep_tvs = []
    nondep_tvs2 = []
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1237:29 in ghc:Outputable
        warnPprTrace, called at compiler/typecheck/TcMType.hs:1472:11 in ghc:TcMType

Bug.hs:7:13: error:
    • Expected kind ‘forall (k :: k1). a’, but ‘z’ has kind ‘k0’
    • In the first argument of ‘Proxy’, namely ‘(z :: forall k. a)’
      In the type signature: t :: Proxy (z :: forall k. a)
  |
7 | t :: Proxy (z :: forall k. a)
  |    

Steps to reproduce

1. Compile GHC with assertions enabled (hadrian/build.sh -j --flavour=Devel2).
2. Load the aforementioned program in GHCi (_build/stage1/bin/ghc --interactive)

Expected behavior

No warning.

Environment

• GHC version used: HEAD