Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,251
    • Issues 4,251
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 394
    • Merge Requests 394
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #8031

Closed
Open
Opened Jul 02, 2013 by Richard Eisenberg@raeDeveloper

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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#8031