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 foralls 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 foralls 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.