Template Haskell gets confused with kind variables introduced in separate foralls

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.

Trac metadata

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