[GHC] #8031: Template Haskell gets confused with kind variables introduced in separate foralls

[GHC]

#8031: Template Haskell gets confused with kind variables introduced in separate
foralls
-----------------------------+----------------------------------------------
Reporter:  goldfire          |          Owner:                           
    Type:  bug               |         Status:  new                      
Priority:  normal            |      Component:  Compiler                 
 Version:  7.7               |       Keywords:  TemplateHaskell PolyKinds
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple         
 Failure:  None/Unknown      |      Blockedby:                           
Blocking:                    |        Related:                           
-----------------------------+----------------------------------------------
 The following file compiles without complaint:

 {{{
 {-# LANGUAGE TemplateHaskell, RankNTypes, PolyKinds, DataKinds,
 TypeOperators,
              GADTs #-}

 module S2 where

 import Language.Haskell.TH

 data Proxy a = Proxy

 data SList :: [k] -> * where
   SCons :: Proxy h -> Proxy t -> SList (h ': t)

 dec :: Q [Dec]
 dec = [d| foo :: forall (a :: k). Proxy a -> forall (b :: [k]). Proxy b ->
 SList (a ': b)
           foo a b = SCons a b |]

 foo' :: forall (a :: k). Proxy a -> forall (b :: [k]). Proxy b -> SList (a
 ': b)
 foo' a b = SCons a b
 }}}

 Note that `foo` and `foo'` are identical, just at different compilation
 stages. However, the following module does not compile:

 {{{
 {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, RankNTypes #-}

 module S3 where

 import S2

 $(dec)
 }}}

 The error is
 {{{
 S3.hs:7:3:
     Couldn't match kind ‛k’ with ‛k1’
       ‛k’ is a rigid type variable bound by
           the type signature for
             foo :: Proxy k a0
                    -> forall (k1 :: BOX) (b0 :: [k1]).
                       Proxy [k1] b0 -> SList k1 ((':) k1 a0 b0)
           at S3.hs:7:3
       ‛k1’ is a rigid type variable bound by
            the type signature for
              foo :: Proxy k a0 -> Proxy [k1] b -> SList k1 ((':) k1 a0 b)
            at S3.hs:7:3
     Expected type: SList k1 ((':) k1 a0 b)
       Actual type: SList k ((':) k a0 b)
     Relevant bindings include
       foo :: Proxy k a0
              -> forall (k1 :: BOX) (b0 :: [k1]).
                 Proxy [k1] b0 -> SList k1 ((':) k1 a0 b0)
         (bound at S3.hs:7:3)
       a_aTCB :: Proxy k a0 (bound at S3.hs:7:3)
       b_aTCC :: Proxy [k1] b (bound at S3.hs:7:3)
     In the expression: SCons a_aTCB b_aTCC
     In an equation for ‛foo’: foo a_aTCB b_aTCC = SCons a_aTCB b_aTCC
 }}}

 If I change the nested `forall`s in the definition of `foo` to be just one
 top-level `forall`, the problem goes away.

 This may seem terribly esoteric, but it's easier to generate nested
 `forall`s than to float them all to the top-level after processing a type.
 I received an email requesting that I get the `singletons` library to
 compile with HEAD, and this seems to be why it doesn't.

 This is a regression error: the code compiles fine with 7.6.3 but not with
 HEAD.

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