"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
- Compile GHC with assertions enabled (
hadrian/build.sh -j --flavour=Devel2
). - Load the aforementioned program in GHCi (
_build/stage1/bin/ghc --interactive
)
Expected behavior
No warning.
Environment
- GHC version used: HEAD