Incorporate changes from #11721 into Template Haskell
authorRyan Scott <ryan.gl.scott@gmail.com>
Sat, 7 Oct 2017 20:58:56 +0000 (16:58 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Sat, 7 Oct 2017 20:58:56 +0000 (16:58 -0400)
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

compiler/basicTypes/DataCon.hs
compiler/basicTypes/DataCon.hs-boot
compiler/typecheck/TcSplice.hs
docs/users_guide/8.4.1-notes.rst
testsuite/tests/th/T11721_TH.hs [new file with mode: 0644]
testsuite/tests/th/T13885.hs
testsuite/tests/th/all.T

index 82298f7..a6d0593 100644 (file)
@@ -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
index a223c4f..841f8c9 100644 (file)
@@ -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
index a010227..04adbc3 100644 (file)
@@ -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'
index dc76260..f59d266 100644 (file)
@@ -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
 ~~~~~~~~~~~~~~~
 
diff --git a/testsuite/tests/th/T11721_TH.hs b/testsuite/tests/th/T11721_TH.hs
new file mode 100644 (file)
index 0000000..979ff15
--- /dev/null
@@ -0,0 +1,26 @@
+{-# 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")
index 0e29c88..cdcc37f 100644 (file)
@@ -1,4 +1,4 @@
-{-# 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 [])
 
index aa973f7..0ad178e 100644 (file)
@@ -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'])