#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