Template Haskell doesn't freshen GADT type variables properly
A simple way to illustrate this bug is with this code:
{-# 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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Template Haskell |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |