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

27 Jun 2017

      #13885: Template Haskell doesn't freshen GADT type variables properly
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Template Haskell  |              Version:  8.0.1
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Actually, it's not just kind variables, and you don't need to necessarily
 import them from another package. Another way to trigger this problem is
 to use `ExistentialQuantification` instead of `GADTs`:

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

 import Language.Haskell.TH

 data a :~: b = a ~ b => Refl

 $(return [])

 main :: IO ()
 main = putStrLn $(reify ''(:~:) >>= stringE . pprint)
 }}}

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

 Now we are shadowing both the type variables `a_0` and `b_2`, as well as
 the kind variable `k_1`.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13885#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler