Opened 7 months ago

#16396 new bug

TH doesn't preserve `forall`

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 8.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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")) |])
   |                  

Change History (0)

Note: See TracTickets for help on using tickets.