Quantification by level numbers would fail
Witness:
rae:11:43:10 ~/ghc/ghc-head/testsuite/tests> ~/ghc/ghc-head/inplace/bin/ghc-stage2 --interactive -fprint-explicit-foralls -fprint-explicit-kinds -XTypeApplications -XDataKinds
GHCi, version 8.9.0.20190531: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /Users/rae/.ghc/ghci.conf
Prelude> import Data.Proxy
Prelude Data.Proxy> :kind! 'Proxy @_
WARNING: file compiler/typecheck/TcMType.hs, line 1470
Quantification by level numbers would fail
Outer level = 0
dep_tkvs = {k_a1Ef[tau:0], __a1Eh[tau:0]}
co_vars =
co_tvs = {}
dep_kvs = [k_a1Ef[tau:0], __a1Eh[tau:0]]
dep_kvs2 = []
nondep_tvs = []
nondep_tvs2 = []
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1231:29 in ghc:Outputable
warnPprTrace, called at compiler/typecheck/TcMType.hs:1470:11 in ghc:TcMType
'Proxy @_ :: forall {k} {_ :: k}. Proxy @{k} _
= 'Proxy @{k} @_
Prelude Data.Proxy>
The problem is that tcRnType
(the worker for GHCi's :kind
) does not bump the level before doing its work. Will fix in ongoing work (!951 (closed)).