[GHC] #14885: TH breaks the scoping of quoted default method implementations when spliced

3 Mar 2018

      #14885: TH breaks the scoping of quoted default method implementations when spliced
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Template       |           Version:  8.2.2
  Haskell                            |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{#!hs
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -ddump-splices #-}
 module Bug where

 class Foo1 a where
   bar1 :: forall b. a -> b -> b
   bar1 _ x = (x :: b)

 $([d| class Foo2 a where
         bar2 :: forall b. a -> b -> b
         bar2 _ x = (x :: b)
     |])
 }}}

 `Foo1` typechecks, so naturally you'd expect `Foo2` to typecheck as well.
 Prepare to be surprised:

 {{{
 $ /opt/ghc/8.2.2/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 Bug.hs:(10,3)-(13,6): Splicing declarations
     [d| class Foo2_aoA a_aoC where
           bar2_aoB :: forall b_aoD. a_aoC -> b_aoD -> b_aoD
           bar2_aoB _ x_aoE = (x_aoE :: b_aoD) |]
   ======>
     class Foo2_a3JQ a_a3JS where
       bar2_a3JR :: forall b_a3JT. a_a3JS -> b_a3JT -> b_a3JT
       bar2_a3JR _ x_a3JU = x_a3JU :: b_aoD

 Bug.hs:10:3: error:
     • Couldn't match expected type ‘b1’ with actual type ‘b’
       ‘b’ is a rigid type variable bound by
         the type signature for:
           bar2 :: forall b. a0 -> b -> b
         at Bug.hs:(10,3)-(13,6)
       ‘b1’ is a rigid type variable bound by
         an expression type signature:
           forall b1. b1
         at Bug.hs:(10,3)-(13,6)
     • In the expression: x_a3JU :: b
       In an equation for ‘bar2’: bar2 _ x_a3JU = x_a3JU :: b
     • Relevant bindings include
         x_a3JU :: b (bound at Bug.hs:10:3)
         bar2 :: a0 -> b -> b (bound at Bug.hs:10:3)
    |
 10 | $([d| class Foo2 a where
    |   ^^^^^^^^^^^^^^^^^^^^^^...
 }}}

 Notice how in the quoted `Foo2` declaration, the scoping is correct:
 `b_a0D` is used in both the type signature for `bar2_a0B` as well as in
 its default implementation. But after splicing, there are now two
 different `b`s: the one in the type signature (`b_a3JT`), and the one in
 the default implementation (`b_aoD`)! This causes the resulting type
 error.

 This is a regression that was introduced somewhere between 7.10.3 and
 8.0.1, since it works in 7.10.3:

 {{{
 $ /opt/ghc/7.10.3/bin/ghci Bug.hs
 GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Bug.hs:(10,3)-(13,6): Splicing declarations
     [d| class Foo2_awn a_awp where
           bar2_awo :: forall b_awq. a_awp -> b_awq -> b_awq
           bar2_awo _ x_awr = (x_awr :: b_awq) |]
   ======>
     class Foo2_a3zs a_a3zu where
       bar2_a3zt :: forall b_awq. a_a3zu -> b_awq -> b_awq
       bar2_a3zt _ x_a3zv = x_a3zv :: b_awq
 Ok, modules loaded: Bug.
 }}}

 But not in any version of GHC since 8.0.1.

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