Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,867
    • Issues 4,867
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16396
Closed
Open
Created Mar 06, 2019 by Richard Eisenberg@raeDeveloper

TH doesn't preserve `forall`

I think there are several bugs in the way TH currently deals with type variable quantification.

  • *Background**

GHC uses the "forall-or-nothing" rule. This means that, if there is a top-level forall in a type signature, that forall must bind all variables being brought into scope in that signature. Examples:

f1 :: a -> a
f1 x = x    -- OK, no forall

f2 :: forall . a -> a
f2 x = x    -- rejected

f3 :: forall a. a -> a
f3 x = x    -- OK, forall binds all variables

f4 :: forall a. a -> a
f4 x = helper x
  where helper :: a -> a        -- OK; this uses a already in scope
        helper _ = x

f5 :: forall a. a -> a
f5 x = helper x
  where helper :: forall . a -> a   -- OK; a is already in scope
        helper _ = x

f6 :: forall a. a -> a
f6 x = helper x
  where helper :: forall a. a -> a   -- this is a new variable `a`
        helper _ = x     -- rejected; the two `a`s are different

Upshot: the existence of forall matters.

  • *Strangeness 1**
foo1 :: $([t| a -> a |])
foo1 x = x

is rejected, because a is not in scope. This is incongruent with the treatment of f1. One could argue, though, that all type variables used in quotes should be in scope. I would disagree with such an argument (that's not what we do these days in terms), but it's not silly.

  • *Strangeness 2**
foo2 :: $([t| $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo2 x = x

is rejected because a is not in scope. This behavior seems just wrong.

  • *Strangeness 3**
foo3 :: $([t| forall . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo3 x = x

is rejected in the same way as foo2. While this should be rejected (it's f2), -ddump-splices says that the splice evaluates to a -> a; note: no forall. So it's rejected under false pretenses.

  • *Strangeness 4**
foo4 :: $([t| forall a . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo4 x = x

This one is accepted (as it should be), but it produces a warning!

Scratch.hs:51:21: warning: [-Wunused-foralls]
    Unused quantified type variable ‘a’
    In the type ‘forall a.
                 $(varT (mkName "a")) -> $(varT (mkName "a"))’
   |
51 | foo :: $([t| forall a . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
   |                  
Trac metadata
Trac field Value
Version 8.6.3
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking