[GHC] #13123: Regression: TH splice requires TypeInType when it shouldn't

[GHC]

#13123: Regression: TH splice requires TypeInType when it shouldn't
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Template       |           Version:  8.0.1
  Haskell                            |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I discovered this when debugging #13018. This code:

 {{{#!hs
 {-# 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
 [http://git.haskell.org/ghc.git/blob/13a85211040f67977d2a2371f4087d1d2ebf4de4:/compiler/deSugar/DsMeta.hs#l735
 rep_wc_ty_sig]. It is always explicitly quantifying all type variables,
 both explicit and implicit.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13123>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler