[GHC] #16396: TH doesn't preserve `forall`

5 Mar 2019

      #16396: TH doesn't preserve `forall`
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Template       |           Version:  8.6.3
  Haskell                            |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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:

 {{{#!hs
 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**

 {{{#!hs
 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**

 {{{#!hs
 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**

 {{{#!hs
 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**

 {{{#!hs
 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"))
 |])
    |
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16396
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler