Regression: TH splice requires TypeInType when it shouldn't

I discovered this when debugging #13018 (closed). This code:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

$([d| idProxy :: forall proxy (a :: k). proxy a -> proxy a
      idProxy x = x
   |])

Used to compile on GHC 7.10.3:

$ /opt/ghc/7.10.3/bin/ghci -ddump-splices Bug.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Bug.hs:(6,3)-(8,5): Splicing declarations
    [d| idProxy_avY ::
          forall proxy_aw0 (a_aw1 :: k_avZ).
          proxy_aw0 a_aw1 -> proxy_aw0 a_aw1
        idProxy_avY x_aw2 = x_aw2 |]
  ======>
    idProxy_a3yP ::
      forall proxy_a3yN (a_a3yO :: k_avZ).
      proxy_a3yN a_a3yO -> proxy_a3yN a_a3yO
    idProxy_a3yP x_a3yQ = x_a3yQ
Ok, modules loaded: Bug.

But on GHC 8.0.2 and HEAD, it's spuriously rejected:

$ /opt/ghc/8.0.2/bin/ghci -ddump-splices Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Bug.hs:(6,3)-(8,5): Splicing declarations
    [d| idProxy_a13B ::
          forall proxy_a13D (a_a13E :: k_a13C).
          proxy_a13D a_a13E -> proxy_a13D a_a13E
        idProxy_a13B x_a13F = x_a13F |]
  ======>
    idProxy_a3LN ::
      forall k_a3LK proxy_a3LL (a_a3LM :: k_a3LK).
      proxy_a3LL a_a3LM -> proxy_a3LL a_a3LM
    idProxy_a3LN x_a3LO = x_a3LO

Bug.hs:6:3: error:
    Type variable ‘k_a3LK’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘idProxy_a3LN’

Notice that in GHC 8.0.2, it's explicitly quantifying the k! This shouldn't happen, since in the source declaration it was implicit.

The culprit is rep_wc_ty_sig. It is always explicitly quantifying all type variables, both explicit and implicit.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture