Commit 341d3a78 authored by Ryan Scott's avatar Ryan Scott

Incorporate changes from #11721 into Template Haskell

Summary:
#11721 changed the order of type variables in GADT
constructor type signatures, but these changes weren't reflected in
Template Haskell reification of GADTs. Let's do that.

Along the way, I:

* noticed that the `T13885` test was claiming to test TH reification
  of GADTs, but the reified data type wasn't actually a GADT! Since
  this patch touches that part of the codebase, I decided to fix
  this.
* incorporated some feedback from @simonpj in
  https://phabricator.haskell.org/D3687#113566. (These changes alone
  don't account for any different in behavior.)

Test Plan: make test TEST=T11721_TH

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: goldfire, bgamari, simonpj

Subscribers: rwbarton, thomie, simonpj

GHC Trac Issues: #11721

Differential Revision: https://phabricator.haskell.org/D4070
parent f6bca0c5
......@@ -278,19 +278,20 @@ data DataCon
-- Running example:
--
-- *** As declared by the user
-- data T a where
-- MkT :: forall y x. (x~y,Ord x) => x -> y -> T (x,y)
-- data T a b c where
-- MkT :: forall c y x b. (x~y,Ord x) => x -> y -> T (x,y) b c
-- *** As represented internally
-- data T a where
-- MkT :: forall a. forall x y. (a~(x,y),x~y,Ord x) => x -> y -> T a
-- data T a b c where
-- MkT :: forall a b c. forall x y. (a~(x,y),x~y,Ord x)
-- => x -> y -> T a b c
--
-- The next six fields express the type of the constructor, in pieces
-- e.g.
--
-- dcUnivTyVars = [a]
-- dcUnivTyVars = [a,b,c]
-- dcExTyVars = [x,y]
-- dcUserTyVarBinders = [y,x]
-- dcUserTyVarBinders = [c,y,x,b]
-- dcEqSpec = [a~(x,y)]
-- dcOtherTheta = [x~y, Ord x]
-- dcOrigArgTys = [x,y]
......@@ -332,7 +333,7 @@ data DataCon
-- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
-- Reason: less confusing, and easier to generate IfaceSyn
-- The type vars in the order the user wrote them [y,x]
-- The type vars in the order the user wrote them [c,y,x,b]
-- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the
-- set of dcExTyVars unioned with the set of dcUnivTyVars
-- whose tyvars do not appear in dcEqSpec
......@@ -920,16 +921,16 @@ mkDataCon name declared_infix prom_info
tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
rep_arg_tys = dataConRepArgTys con
mk_rep_for_all_tys =
rep_ty =
case rep of
-- If the DataCon has no wrapper, then the worker's type *is* the
-- user-facing type, so we can simply use user_tvbs.
NoDataConRep -> mkForAllTys user_tvbs'
-- user-facing type, so we can simply use dataConUserType.
NoDataConRep -> dataConUserType con
-- If the DataCon has a wrapper, then the worker's type is never seen
-- by the user. The visibilities we pick do not matter here.
DCR{} -> mkInvForAllTys univ_tvs . mkInvForAllTys ex_tvs
rep_ty = mk_rep_for_all_tys $ mkFunTys rep_arg_tys $
mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
DCR{} -> mkInvForAllTys univ_tvs $ mkInvForAllTys ex_tvs $
mkFunTys rep_arg_tys $
mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
-- See Note [Promoted data constructors] in TyCon
prom_tv_bndrs = [ mkNamedTyConBinder vis tv
......
......@@ -13,7 +13,6 @@ import {-# SOURCE #-} TyCoRep ( Type, ThetaType )
data DataCon
data DataConRep
data EqSpec
filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
dataConName :: DataCon -> Name
dataConTyCon :: DataCon -> TyCon
......
......@@ -102,7 +102,7 @@ import ErrUtils
import Util
import Unique
import VarSet
import Data.List ( find )
import Data.List ( find, mapAccumL )
import Data.Maybe
import FastString
import BasicTypes hiding( SuccessFlag(..) )
......@@ -1466,7 +1466,8 @@ 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_user_tvs' = dataConUserTyVars dc
(g_univ_tvs, _, g_eq_spec, g_theta', g_arg_tys', g_res_ty')
= dataConFullSig dc
(srcUnpks, srcStricts)
= mapAndUnzip reifySourceBang (dataConSrcBangs dc)
......@@ -1477,13 +1478,15 @@ reifyDataCon isGadtDataCon tys dc
-- they will not appear anywhere in the type.
eq_spec_tvs = mkVarSet (map eqSpecTyVar g_eq_spec)
; (univ_subst, g_unsbst_univ_tvs)
; (univ_subst, _)
-- 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'
; let (tvb_subst, g_user_tvs)
= mapAccumL substTyVarBndr univ_subst g_user_tvs'
g_theta = substTys tvb_subst g_theta'
g_arg_tys = substTys tvb_subst g_arg_tys'
g_res_ty = substTy tvb_subst g_res_ty'
; r_arg_tys <- reifyTypes (if isGadtDataCon then g_arg_tys else arg_tys)
......@@ -1510,9 +1513,8 @@ reifyDataCon isGadtDataCon tys dc
| otherwise ->
return $ TH.NormalC name (dcdBangs `zip` r_arg_tys)
; let (ex_tvs', theta') | isGadtDataCon = ( g_unsbst_univ_tvs ++ g_ex_tvs
, g_theta )
| otherwise = ( ex_tvs, theta )
; let (ex_tvs', theta') | isGadtDataCon = (g_user_tvs, g_theta)
| otherwise = (ex_tvs, theta)
ret_con | null ex_tvs' && null theta' = return main_con
| otherwise = do
{ cxt <- reifyCxt theta'
......
......@@ -197,6 +197,16 @@ Template Haskell
such as ``data T1 a = (a ~ Int) => MkT1`` being reified as a GADT and
``data T2 a where MkT2 :: Show a => T2 a`` *not* being reified as a GADT.
In addition, reified GADT constructors now more accurately track the order in
which users write type variables. Before, if you reified ``MkT`` as below: ::
data T a where
MkT :: forall b a. b -> T a
Then the reified type signature of ``MkT`` would have been headed by
``ForallC [PlainTV a, PlainTV b]``. Now, reifying ``MkT`` will give a type
headed by ``ForallC [PlainTV b, PlainTV a]``, as one would expect.
``ghc`` library
~~~~~~~~~~~~~~~
......
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module T11721_TH where
import Language.Haskell.TH
data T a where
MkT :: forall b a. b -> T a
$(return [])
main :: IO ()
main = print
$(do let rightOrder :: [TyVarBndr] -> Bool
rightOrder [KindedTV b _, KindedTV a _]
= nameBase b == "b" && nameBase a == "a"
rightOrder _ = False
TyConI (DataD _ _ _ _
[ForallC con_tvbs1 _ _] _) <- reify ''T
DataConI _ (ForallT con_tvbs2 _ _) _ <- reify 'MkT
if rightOrder con_tvbs1 && rightOrder con_tvbs2
then [| () |]
else fail "T11721_TH failed")
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
......@@ -7,7 +7,8 @@ module Main where
import Data.Function (on)
import Language.Haskell.TH.Syntax
data a :~: b = a ~ b => Refl
data a :~: b where
Refl :: a ~ b => a :~: b
$(return [])
......
......@@ -350,6 +350,7 @@ test('T9022', normal, compile_and_run, ['-v0'])
test('T11145', normal, compile_fail, ['-v0 -dsuppress-uniques'])
test('T11463', normal, compile_and_run, ['-v0 -dsuppress-uniques'])
test('T11680', normal, compile_fail, ['-v0'])
test('T11721_TH', normal, compile, ['-v0'])
test('T11809', normal, compile, ['-v0'])
test('T11797', normal, compile, ['-v0 -dsuppress-uniques'])
test('T11941', normal, compile_fail, ['-v0'])
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment