[commit: ghc] master: Fix #13885 by freshening reified GADT constructors' universal tyvars (79b259a)
git at git.haskell.org
git at git.haskell.org
Tue Aug 22 14:56:32 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/79b259ae6a0a0c17568d7d03d82e378ad4c4001a/ghc
>---------------------------------------------------------------
commit 79b259ae6a0a0c17568d7d03d82e378ad4c4001a
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date: Tue Aug 22 09:28:56 2017 -0400
Fix #13885 by freshening reified GADT constructors' universal tyvars
Summary:
When reifying GADTs with Template Haskell, the universally quantified
type variables were being reused across both the data type head and the
constructors' type signatures. This had the annoying effect of causing sets
of differently scoped variables to have the same uniques. To avoid this, we
now freshen the universal tyvars before reifying the constructors so as to
ensure they have distinct uniques.
Test Plan: make test TEST=T13885
Reviewers: goldfire, austin, bgamari, simonpj
Reviewed By: simonpj
Subscribers: rwbarton, thomie
GHC Trac Issues: #13885
Differential Revision: https://phabricator.haskell.org/D3867
>---------------------------------------------------------------
79b259ae6a0a0c17568d7d03d82e378ad4c4001a
compiler/typecheck/TcSplice.hs | 77 ++++++++++++++++------
testsuite/tests/th/T13885.hs | 23 +++++++
.../tests/th/T13885.stdout | 0
testsuite/tests/th/all.T | 1 +
4 files changed, 82 insertions(+), 19 deletions(-)
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 8b5ed7d..029ae28 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1449,7 +1449,7 @@ reifyDataCon isGadtDataCon tys dc
(ex_tvs, theta, arg_tys)
= dataConInstSig dc tys
-- used for GADTs data constructors
- (g_univ_tvs, g_ex_tvs, g_eq_spec, g_theta, g_arg_tys, g_res_ty)
+ (g_univ_tvs, g_ex_tvs, g_eq_spec, g_theta', g_arg_tys', g_res_ty')
= dataConFullSig dc
(srcUnpks, srcStricts)
= mapAndUnzip reifySourceBang (dataConSrcBangs dc)
@@ -1459,7 +1459,14 @@ reifyDataCon isGadtDataCon tys dc
-- Universal tvs present in eq_spec need to be filtered out, as
-- they will not appear anywhere in the type.
eq_spec_tvs = mkVarSet (map eqSpecTyVar g_eq_spec)
- g_unsbst_univ_tvs = filterOut (`elemVarSet` eq_spec_tvs) g_univ_tvs
+
+ ; (univ_subst, g_unsbst_univ_tvs)
+ -- See Note [Freshen reified GADT constructors' universal tyvars]
+ <- freshenTyVarBndrs $
+ filterOut (`elemVarSet` eq_spec_tvs) g_univ_tvs
+ ; let g_theta = substTys univ_subst g_theta'
+ g_arg_tys = substTys univ_subst g_arg_tys'
+ g_res_ty = substTy univ_subst g_res_ty'
; r_arg_tys <- reifyTypes (if isGadtDataCon then g_arg_tys else arg_tys)
@@ -1497,23 +1504,55 @@ reifyDataCon isGadtDataCon tys dc
; ASSERT( arg_tys `equalLength` dcdBangs )
ret_con }
--- Note [Reifying GADT data constructors]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- At this point in the compilation pipeline we have no way of telling whether a
--- data type was declared as a H98 data type or as a GADT. We have to rely on
--- heuristics here. We look at dcEqSpec field of all data constructors in a
--- data type declaration. If at least one data constructor has non-empty
--- dcEqSpec this means that the data type must have been declared as a GADT.
--- Consider these declarations:
---
--- data T a where
--- MkT :: forall a. (a ~ Int) => T a
---
--- data T a where
--- MkT :: T Int
---
--- First declaration will be reified as a GADT. Second declaration will be
--- reified as a normal H98 data type declaration.
+{-
+Note [Reifying GADT data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At this point in the compilation pipeline we have no way of telling whether a
+data type was declared as a H98 data type or as a GADT. We have to rely on
+heuristics here. We look at dcEqSpec field of all data constructors in a
+data type declaration. If at least one data constructor has non-empty
+dcEqSpec this means that the data type must have been declared as a GADT.
+Consider these declarations:
+
+ data T1 a where
+ MkT1 :: T1 Int
+
+ data T2 a where
+ MkT2 :: forall a. (a ~ Int) => T2 a
+
+T1 will be reified as a GADT, as it has a non-empty EqSpec [(a, Int)] due to
+MkT1's return type. T2 will be reified as a normal H98 data type declaration
+since MkT2 uses an explicit type equality in its context instead of an implicit
+equality in its return type, and therefore has an empty EqSpec.
+
+Note [Freshen reified GADT constructors' universal tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose one were to reify this data type:
+
+ data a :~: b = (a ~ b) => Refl
+
+This will be reified as if it were a GADT definiton, so the reified definition
+will be closer to:
+
+ data a :~: b where
+ Refl :: forall a b. (a ~ b) => a :~: b
+
+We ought to be careful here about the uniques we give to the occurrences of `a`
+and `b` in this definition. That is because in the original DataCon, all uses
+of `a` and `b` have the same unique, since `a` and `b` are both universally
+quantified type variables--that is, they are used in both the (:~:) tycon as
+well as in the constructor type signature. But when we turn the DataCon
+definition into the reified one, the `a` and `b` in the constructor type
+signature becomes differently scoped than the `a` and `b` in `data a :~: b`.
+
+While it wouldn't technically be *wrong* per se to re-use the same uniques for
+`a` and `b` across these two different scopes, it's somewhat annoying for end
+users of Template Haskell, since they wouldn't be able to rely on the
+assumption that all TH names have globally distinct uniques (#13885). For this
+reason, we freshen the universally quantified tyvars that go into the reified
+GADT constructor type signature to give them distinct uniques from their
+counterparts in the tycon.
+-}
------------------------------
reifyClass :: Class -> TcM TH.Info
diff --git a/testsuite/tests/th/T13885.hs b/testsuite/tests/th/T13885.hs
new file mode 100644
index 0000000..0e29c88
--- /dev/null
+++ b/testsuite/tests/th/T13885.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module Main where
+
+import Data.Function (on)
+import Language.Haskell.TH.Syntax
+
+data a :~: b = a ~ b => Refl
+
+$(return [])
+
+main :: IO ()
+main = print
+ $(do TyConI (DataD _ _ tycon_tyvars _
+ [ForallC con_tyvars _ _] _) <- reify ''(:~:)
+
+ let tvbName :: TyVarBndr -> Name
+ tvbName (PlainTV n) = n
+ tvbName (KindedTV n _) = n
+
+ lift $ and $ zipWith ((/=) `on` tvbName) tycon_tyvars con_tyvars)
diff --git a/libraries/base/tests/IO/IOError002.stdout b/testsuite/tests/th/T13885.stdout
similarity index 100%
copy from libraries/base/tests/IO/IOError002.stdout
copy to testsuite/tests/th/T13885.stdout
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 5d61fa4..1e737ac 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -391,6 +391,7 @@ test('T13781', normal, compile, ['-v0'])
test('T13782', normal, compile, [''])
test('T13837', normal, compile_fail, ['-v0 -dsuppress-uniques'])
test('T13856', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('T13885', normal, compile_and_run, ['-v0'])
test('T13887', normal, compile_and_run, ['-v0'])
test('T13968', normal, compile_fail, ['-v0'])
test('T14060', normal, compile_and_run, ['-v0'])
More information about the ghc-commits
mailing list