Commit 8e4229ab authored by Ryan Scott's avatar Ryan Scott
Browse files

Fix #14167 by using isGadtSyntaxTyCon in more places

Summary:
Two places in GHC effectively attempt to //guess// whether a data type
was declared using GADT syntax:

1. When reifying a data type in Template Haskell
2. When pretty-printing a data type (e.g., via `:info` in GHCi)

But there's no need for heuristics here, since we have a 100% accurate way to
determine whether a data type was declared using GADT syntax: the
`isGadtSyntaxTyCon` function! By simply using that as the metric, we obtain
far more accurate TH reification and pretty-printing results.

This is technically a breaking change, since Template Haskell reification will
now reify some data type constructors as `(Rec)GadtC` that it didn't before,
and some data type constructors that were previously reified as `(Rec)GadtC`
will no longer be reified as such. But it's a very understandable breaking
change, since the previous behavior was simply incorrect.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #14167

Differential Revision: https://phabricator.haskell.org/D3901
parent 5dd6b13c
...@@ -697,7 +697,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, ...@@ -697,7 +697,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
ifGadtSyntax = gadt, ifGadtSyntax = gadt,
ifBinders = binders }) ifBinders = binders })
| gadt_style = vcat [ pp_roles | gadt = vcat [ pp_roles
, pp_nd <+> pp_lhs <+> pp_where , pp_nd <+> pp_lhs <+> pp_where
, nest 2 (vcat pp_cons) , nest 2 (vcat pp_cons)
, nest 2 $ ppShowIface ss pp_extra ] , nest 2 $ ppShowIface ss pp_extra ]
...@@ -707,9 +707,8 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, ...@@ -707,9 +707,8 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
where where
is_data_instance = isIfaceDataInstance parent is_data_instance = isIfaceDataInstance parent
gadt_style = gadt || any (not . isVanillaIfaceConDecl) cons
cons = visibleIfConDecls condecls cons = visibleIfConDecls condecls
pp_where = ppWhen (gadt_style && not (null cons)) $ text "where" pp_where = ppWhen (gadt && not (null cons)) $ text "where"
pp_cons = ppr_trim (map show_con cons) :: [SDoc] pp_cons = ppr_trim (map show_con cons) :: [SDoc]
pp_lhs = case parent of pp_lhs = case parent of
...@@ -732,7 +731,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, ...@@ -732,7 +731,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
ok_con dc = showSub ss dc || any (showSub ss . flSelector) (ifConFields dc) ok_con dc = showSub ss dc || any (showSub ss . flSelector) (ifConFields dc)
show_con dc show_con dc
| ok_con dc = Just $ pprIfaceConDecl ss gadt_style tycon binders parent dc | ok_con dc = Just $ pprIfaceConDecl ss gadt tycon binders parent dc
| otherwise = Nothing | otherwise = Nothing
pp_nd = case condecls of pp_nd = case condecls of
...@@ -953,12 +952,6 @@ pprIfaceDeclHead context ss tc_occ bndrs m_res_kind ...@@ -953,12 +952,6 @@ pprIfaceDeclHead context ss tc_occ bndrs m_res_kind
<+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs) <+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs)
, maybe empty (\res_kind -> dcolon <+> pprIfaceType res_kind) m_res_kind ] , maybe empty (\res_kind -> dcolon <+> pprIfaceType res_kind) m_res_kind ]
isVanillaIfaceConDecl :: IfaceConDecl -> Bool
isVanillaIfaceConDecl (IfCon { ifConExTvs = ex_tvs
, ifConEqSpec = eq_spec
, ifConCtxt = ctxt })
= (null ex_tvs) && (null eq_spec) && (null ctxt)
pprIfaceConDecl :: ShowSub -> Bool pprIfaceConDecl :: ShowSub -> Bool
-> IfaceTopBndr -> IfaceTopBndr
-> [IfaceTyConBinder] -> [IfaceTyConBinder]
...@@ -969,22 +962,26 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent ...@@ -969,22 +962,26 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
ifConExTvs = ex_tvs, ifConExTvs = ex_tvs,
ifConEqSpec = eq_spec, ifConCtxt = ctxt, ifConArgTys = arg_tys, ifConEqSpec = eq_spec, ifConCtxt = ctxt, ifConArgTys = arg_tys,
ifConStricts = stricts, ifConFields = fields }) ifConStricts = stricts, ifConFields = fields })
| gadt_style = pp_prefix_con <+> dcolon <+> ppr_ty | gadt_style = pp_prefix_con <+> dcolon <+> ppr_gadt_ty
| otherwise = ppr_ex_quant pp_h98_con
where
pp_h98_con
| not (null fields) = pp_prefix_con <+> pp_field_args | not (null fields) = pp_prefix_con <+> pp_field_args
| is_infix | is_infix
, [ty1, ty2] <- pp_args = sep [ ty1 , [ty1, ty2] <- pp_args
= sep [ ty1
, pprInfixIfDeclBndr how_much (occName name) , pprInfixIfDeclBndr how_much (occName name)
, ty2] , ty2]
| otherwise = pp_prefix_con <+> sep pp_args | otherwise = pp_prefix_con <+> sep pp_args
where
how_much = ss_how_much ss how_much = ss_how_much ss
tys_w_strs :: [(IfaceBang, IfaceType)] tys_w_strs :: [(IfaceBang, IfaceType)]
tys_w_strs = zip stricts arg_tys tys_w_strs = zip stricts arg_tys
pp_prefix_con = pprPrefixIfDeclBndr how_much (occName name) pp_prefix_con = pprPrefixIfDeclBndr how_much (occName name)
(univ_tvs, pp_res_ty) = mk_user_con_res_ty eq_spec (univ_tvs, pp_res_ty) = mk_user_con_res_ty eq_spec
ppr_ty = pprIfaceForAllPart (map tv_to_forall_bndr univ_tvs ++ ex_tvs) ppr_ex_quant = pprIfaceForAllPartMust ex_tvs ctxt
ppr_gadt_ty = pprIfaceForAllPart (map tv_to_forall_bndr univ_tvs ++ ex_tvs)
ctxt pp_tau ctxt pp_tau
-- A bit gruesome this, but we can't form the full con_tau, and ppr it, -- A bit gruesome this, but we can't form the full con_tau, and ppr it,
......
...@@ -34,8 +34,8 @@ module IfaceType ( ...@@ -34,8 +34,8 @@ module IfaceType (
pprIfaceContext, pprIfaceContextArr, pprIfaceContext, pprIfaceContextArr,
pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders, pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs, pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType, pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
pprIfaceTyLit, pprIfaceSigmaType, pprIfaceTyLit,
pprIfaceCoercion, pprParendIfaceCoercion, pprIfaceCoercion, pprParendIfaceCoercion,
splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll, splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp, pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
...@@ -744,6 +744,11 @@ pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc ...@@ -744,6 +744,11 @@ pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPart tvs ctxt sdoc pprIfaceForAllPart tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc = ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc
-- | Like 'pprIfaceForAllPart', but always uses an explicit @forall@.
pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPartMust tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
pprIfaceForAllCoPart tvs sdoc pprIfaceForAllCoPart tvs sdoc
= sep [ pprIfaceForAllCo tvs, sdoc ] = sep [ pprIfaceForAllCo tvs, sdoc ]
......
...@@ -1430,8 +1430,7 @@ reifyTyCon tc ...@@ -1430,8 +1430,7 @@ reifyTyCon tc
= do { cxt <- reifyCxt (tyConStupidTheta tc) = do { cxt <- reifyCxt (tyConStupidTheta tc)
; let tvs = tyConTyVars tc ; let tvs = tyConTyVars tc
dataCons = tyConDataCons tc dataCons = tyConDataCons tc
-- see Note [Reifying GADT data constructors] isGadt = isGadtSyntaxTyCon tc
isGadt = any (not . null . dataConEqSpec) dataCons
; cons <- mapM (reifyDataCon isGadt (mkTyVarTys tvs)) dataCons ; cons <- mapM (reifyDataCon isGadt (mkTyVarTys tvs)) dataCons
; r_tvs <- reifyTyVars tvs (Just tc) ; r_tvs <- reifyTyVars tvs (Just tc)
; let name = reifyName tc ; let name = reifyName tc
...@@ -1443,7 +1442,6 @@ reifyTyCon tc ...@@ -1443,7 +1442,6 @@ reifyTyCon tc
; return (TH.TyConI decl) } ; return (TH.TyConI decl) }
reifyDataCon :: Bool -> [Type] -> DataCon -> TcM TH.Con reifyDataCon :: Bool -> [Type] -> DataCon -> TcM TH.Con
-- For GADTs etc, see Note [Reifying GADT data constructors]
reifyDataCon isGadtDataCon tys dc reifyDataCon isGadtDataCon tys dc
= do { let -- used for H98 data constructors = do { let -- used for H98 data constructors
(ex_tvs, theta, arg_tys) (ex_tvs, theta, arg_tys)
...@@ -1505,34 +1503,9 @@ reifyDataCon isGadtDataCon tys dc ...@@ -1505,34 +1503,9 @@ reifyDataCon isGadtDataCon tys dc
ret_con } 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 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] Note [Freshen reified GADT constructors' universal tyvars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose one were to reify this data type: Suppose one were to reify this GADT:
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 data a :~: b where
Refl :: forall a b. (a ~ b) => a :~: b Refl :: forall a b. (a ~ b) => a :~: b
...@@ -1697,8 +1670,7 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor ...@@ -1697,8 +1670,7 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
eta_expanded_tvs = mkTyVarTys fam_tvs `chkAppend` etad_tys eta_expanded_tvs = mkTyVarTys fam_tvs `chkAppend` etad_tys
eta_expanded_lhs = lhs `chkAppend` etad_tys eta_expanded_lhs = lhs `chkAppend` etad_tys
dataCons = tyConDataCons rep_tc dataCons = tyConDataCons rep_tc
-- see Note [Reifying GADT data constructors] isGadt = isGadtSyntaxTyCon rep_tc
isGadt = any (not . null . dataConEqSpec) dataCons
; cons <- mapM (reifyDataCon isGadt eta_expanded_tvs) dataCons ; cons <- mapM (reifyDataCon isGadt eta_expanded_tvs) dataCons
; let types_only = filterOutInvisibleTypes fam_tc eta_expanded_lhs ; let types_only = filterOutInvisibleTypes fam_tc eta_expanded_lhs
; th_tys <- reifyTypes types_only ; th_tys <- reifyTypes types_only
......
...@@ -124,6 +124,12 @@ Runtime system ...@@ -124,6 +124,12 @@ Runtime system
Template Haskell Template Haskell
~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~
- Template Haskell now reifies data types with GADT syntax accurately.
Previously, TH used heuristics to determine whether a data type
should be reified using GADT syntax, which could lead to incorrect results,
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.
``ghc`` library ``ghc`` library
~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~
......
...@@ -3,6 +3,5 @@ data A (x :: k) (y :: k1) ...@@ -3,6 +3,5 @@ data A (x :: k) (y :: k1)
-- Defined at <interactive>:2:1 -- Defined at <interactive>:2:1
A :: k1 -> k2 -> * A :: k1 -> k2 -> *
type role T phantom type role T phantom
data T (a :: k) where data T (a :: k) = forall a1. MkT a1
MkT :: forall k (a :: k) a1. a1 -> T a
-- Defined at <interactive>:6:1 -- Defined at <interactive>:6:1
data D2 where data D2
MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2 = forall k. MkD2 (forall (p :: k -> *) (a :: k). p a -> Int)
-- Defined at <interactive>:3:1 -- Defined at <interactive>:3:1
data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int) data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int)
-- Defined at <interactive>:4:1 -- Defined at <interactive>:4:1
...@@ -4,19 +4,22 @@ type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol) ...@@ -4,19 +4,22 @@ type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol) type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol)
(b :: GHC.Types.Symbol) (b :: GHC.Types.Symbol)
:: Ordering :: Ordering
data GHC.TypeLits.ErrorMessage where data GHC.TypeLits.ErrorMessage
GHC.TypeLits.Text :: GHC.Types.Symbol -> GHC.TypeLits.ErrorMessage = GHC.TypeLits.Text GHC.Types.Symbol
GHC.TypeLits.ShowType :: t -> GHC.TypeLits.ErrorMessage | forall t. GHC.TypeLits.ShowType t
(GHC.TypeLits.:<>:) :: GHC.TypeLits.ErrorMessage | GHC.TypeLits.ErrorMessage
-> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage GHC.TypeLits.:<>:
(GHC.TypeLits.:$$:) :: GHC.TypeLits.ErrorMessage GHC.TypeLits.ErrorMessage
-> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage | GHC.TypeLits.ErrorMessage
GHC.TypeLits.:$$:
GHC.TypeLits.ErrorMessage
class GHC.TypeLits.KnownSymbol (n :: GHC.Types.Symbol) where class GHC.TypeLits.KnownSymbol (n :: GHC.Types.Symbol) where
GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n
{-# MINIMAL symbolSing #-} {-# MINIMAL symbolSing #-}
data GHC.TypeLits.SomeSymbol where data GHC.TypeLits.SomeSymbol
GHC.TypeLits.SomeSymbol :: GHC.TypeLits.KnownSymbol n => = forall (n :: GHC.Types.Symbol).
(Data.Proxy.Proxy n) -> GHC.TypeLits.SomeSymbol GHC.TypeLits.KnownSymbol n =>
GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage) type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
:: b :: b
GHC.TypeLits.natVal :: GHC.TypeLits.natVal ::
...@@ -54,9 +57,10 @@ class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where ...@@ -54,9 +57,10 @@ class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where
GHC.TypeNats.natSing :: GHC.TypeNats.SNat n GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
{-# MINIMAL natSing #-} {-# MINIMAL natSing #-}
data GHC.Types.Nat data GHC.Types.Nat
data GHC.TypeNats.SomeNat where data GHC.TypeNats.SomeNat
GHC.TypeNats.SomeNat :: GHC.TypeNats.KnownNat n => = forall (n :: GHC.Types.Nat).
(Data.Proxy.Proxy n) -> GHC.TypeNats.SomeNat GHC.TypeNats.KnownNat n =>
GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
data GHC.Types.Symbol data GHC.Types.Symbol
type family (GHC.TypeNats.^) (a :: GHC.Types.Nat) type family (GHC.TypeNats.^) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat) (b :: GHC.Types.Nat)
......
data D where data D = forall a. C (Int -> a) Char -- Defined at ghci030.hs:8:1
C :: (Int -> a) -> Char -> D data D = forall a. C (Int -> a) Char -- Defined at ghci030.hs:8:10
-- Defined at ghci030.hs:8:1
data D where
C :: (Int -> a) -> Char -> D
-- Defined at ghci030.hs:8:10
...@@ -71,10 +71,8 @@ RnFail055.hs-boot:25:1: error: ...@@ -71,10 +71,8 @@ RnFail055.hs-boot:25:1: error:
Type constructor ‘T7’ has conflicting definitions in the module Type constructor ‘T7’ has conflicting definitions in the module
and its hs-boot file and its hs-boot file
Main module: type role T7 phantom Main module: type role T7 phantom
data T7 a where data T7 a = forall a1. T7 a1
T7 :: a1 -> T7 a Boot file: data T7 a = forall b. T7 a
Boot file: data T7 a where
T7 :: a -> T7 a
The roles do not match. The roles do not match.
Roles on abstract types default to ‘representational’ in boot files. Roles on abstract types default to ‘representational’ in boot files.
The constructors do not match: The types for ‘T7’ differ The constructors do not match: The types for ‘T7’ differ
......
data T4188.T1 (a_0 :: *) = forall (b_1 :: *) . T4188.MkT1 a_0 b_1 data T4188.T1 (a_0 :: *) where
data T4188.T2 (a_0 :: *) T4188.MkT1 :: forall (a_1 :: *) (b_2 :: *) . a_1 ->
= forall (b_1 :: *) . (T4188.C a_0, T4188.C b_1) => T4188.MkT2 a_0 b_2 -> T4188.T1 a_1
b_1 data T4188.T2 (a_0 :: *) where
T4188.MkT2 :: forall (a_1 :: *) (b_2 :: *) . (T4188.C a_1,
T4188.C b_2) => a_1 -> b_2 -> T4188.T2 a_1
data T4188.T3 (x_0 :: *) where data T4188.T3 (x_0 :: *) where
T4188.MkT3 :: forall (x_1 :: *) (y_2 :: *) . (T4188.C x_1, T4188.MkT3 :: forall (x_1 :: *) (y_2 :: *) . (T4188.C x_1,
T4188.C y_2) => x_1 -> y_2 -> T4188.T3 (x_1, y_2) T4188.C y_2) => x_1 -> y_2 -> T4188.T3 (x_1, y_2)
...@@ -3,7 +3,6 @@ T3468.hs-boot:3:1: error: ...@@ -3,7 +3,6 @@ T3468.hs-boot:3:1: error:
Type constructor ‘Tool’ has conflicting definitions in the module Type constructor ‘Tool’ has conflicting definitions in the module
and its hs-boot file and its hs-boot file
Main module: type role Tool phantom Main module: type role Tool phantom
data Tool d where data Tool d = forall a r. F a
F :: a -> Tool d
Boot file: data Tool Boot file: data Tool
The types have different kinds The types have different kinds
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