[GHC] #13885: Template Haskell doesn't freshen GADT kind variables properly when imported from another package

[GHC]

#13885: Template Haskell doesn't freshen GADT kind variables properly when imported
from another package
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Template       |           Version:  8.0.1
  Haskell                            |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect result
  Unknown/Multiple                   |  at runtime
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 A simple way to illustrate this bug is with this code:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeOperators #-}
 module Foo where

 import qualified Data.Type.Equality as DTE ((:~:))
 import Language.Haskell.TH

 data a :~: b where
   Refl :: a :~: a

 $(return [])

 main :: IO ()
 main = do
   putStrLn "Imported\n-----"
   putStrLn $(reify ''(DTE.:~:) >>= stringE . pprint)
   putStrLn "-----\n\nLocally defined\n-----"
   putStrLn $(reify ''(:~:) >>= stringE . pprint)
   putStrLn "-----"
 }}}

 Here, I'm pretty-printing the reified Template Haskell information about
 two datatypes: one that is imported from another package (`base`), and
 another that is defined locally. Aside from their definition sites, they
 are otherwise identical. However, when reifying them with Template
 Haskell, there is another distinction one can observe:

 {{{
 $ /opt/ghc/8.2.1/bin/runghc Foo.hs
 Imported
 -----
 data Data.Type.Equality.:~: (a_0 :: k_1) (b_2 :: k_1) where
     Data.Type.Equality.Refl :: forall (k_1 :: *) (a_0 :: k_1) .
 Data.Type.Equality.:~: a_0
 a_0
 -----

 Locally defined
 -----
 data Foo.:~: (a_0 :: k_1) (b_2 :: k_1) where
     Foo.Refl :: forall (k_3 :: *) (a_4 :: k_3) . Foo.:~: a_4 a_4
 -----
 }}}

 The locally defined information looks fine, but the one imported from
 `base` is suspicious. Namely, the `k_1` variable is used both in the
 datatype head and in the quantified variables for the constructor! To
 confirm this, you can print out more verbose info with `show` instead of
 `pprint`:

 {{{
 Imported
 -----
 TyConI (DataD [] Data.Type.Equality.:~: [KindedTV a_6989586621679026781
 (VarT k_6989586621679026780),KindedTV b_6989586621679026782 (VarT
 k_6989586621679026780)] Nothing [ForallC [KindedTV k_6989586621679026780
 StarT,KindedTV a_6989586621679026781 (VarT k_6989586621679026780)] []
 (GadtC [Data.Type.Equality.Refl] [] (AppT (AppT (ConT
 Data.Type.Equality.:~:) (VarT a_6989586621679026781)) (VarT
 a_6989586621679026781)))] [])
 -----

 Locally defined
 -----
 TyConI (DataD [] Foo.:~: [KindedTV a_6989586621679016094 (VarT
 k_6989586621679016098),KindedTV b_6989586621679016095 (VarT
 k_6989586621679016098)] Nothing [ForallC [KindedTV k_6989586621679016108
 StarT,KindedTV a_6989586621679016096 (VarT k_6989586621679016108)] []
 (GadtC [Foo.Refl] [] (AppT (AppT (ConT Foo.:~:) (VarT
 a_6989586621679016096)) (VarT a_6989586621679016096)))] [])
 -----
 }}}

 Sure enough, the variable `k_6989586621679026780` is used in both places.
 I would expect this not to happen, since the two sets of variables are
 scoped differently, and in practice, I have to work around this by
 freshening the type variables for the constructor, which is annoying.

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