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

#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
participants (1)
-
GHC