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

11 files changed, 70 insertions, 93 deletions

diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 13eb2089a7..1373fb0fcb 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -697,19 +697,18 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
                              ifGadtSyntax = gadt,
                              ifBinders = binders })
 
-  | gadt_style = vcat [ pp_roles
-                      , pp_nd <+> pp_lhs <+> pp_where
-                      , nest 2 (vcat pp_cons)
-                      , nest 2 $ ppShowIface ss pp_extra ]
-  | otherwise  = vcat [ pp_roles
-                      , hang (pp_nd <+> pp_lhs) 2 (add_bars pp_cons)
-                      , nest 2 $ ppShowIface ss pp_extra ]
+  | gadt      = vcat [ pp_roles
+                     , pp_nd <+> pp_lhs <+> pp_where
+                     , nest 2 (vcat pp_cons)
+                     , nest 2 $ ppShowIface ss pp_extra ]
+  | otherwise = vcat [ pp_roles
+                     , hang (pp_nd <+> pp_lhs) 2 (add_bars pp_cons)
+                     , nest 2 $ ppShowIface ss pp_extra ]
   where
     is_data_instance = isIfaceDataInstance parent
 
-    gadt_style = gadt || any (not . isVanillaIfaceConDecl) cons
     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_lhs = case parent of
@@ -732,7 +731,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     ok_con dc = showSub ss dc || any (showSub ss . flSelector) (ifConFields 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
 
     pp_nd = case condecls of
@@ -953,12 +952,6 @@ pprIfaceDeclHead context ss tc_occ bndrs m_res_kind
           <+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs)
         , 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
                 -> IfaceTopBndr
                 -> [IfaceTyConBinder]
@@ -969,23 +962,27 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
                  ifConExTvs = ex_tvs,
                  ifConEqSpec = eq_spec, ifConCtxt = ctxt, ifConArgTys = arg_tys,
                  ifConStricts = stricts, ifConFields = fields })
-  | gadt_style            = pp_prefix_con <+> dcolon <+> ppr_ty
-  | not (null fields)     = pp_prefix_con <+> pp_field_args
-  | is_infix
-  , [ty1, ty2] <- pp_args = sep [ ty1
-                                , pprInfixIfDeclBndr how_much (occName name)
-                                , ty2]
-
-  | otherwise             = pp_prefix_con <+> sep pp_args
+  | 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
+      | is_infix
+      , [ty1, ty2] <- pp_args
+      = sep [ ty1
+            , pprInfixIfDeclBndr how_much (occName name)
+            , ty2]
+      | otherwise = pp_prefix_con <+> sep pp_args
+
     how_much = ss_how_much ss
     tys_w_strs :: [(IfaceBang, IfaceType)]
     tys_w_strs = zip stricts arg_tys
     pp_prefix_con = pprPrefixIfDeclBndr how_much (occName name)
 
     (univ_tvs, pp_res_ty) = mk_user_con_res_ty eq_spec
-    ppr_ty = pprIfaceForAllPart (map tv_to_forall_bndr univ_tvs ++ ex_tvs)
-                                ctxt pp_tau
+    ppr_ex_quant = pprIfaceForAllPartMust ex_tvs ctxt
+    ppr_gadt_ty = pprIfaceForAllPart (map tv_to_forall_bndr univ_tvs ++ ex_tvs)
+                                     ctxt pp_tau
 
         -- A bit gruesome this, but we can't form the full con_tau, and ppr it,
         -- because we don't have a Name for the tycon, only an OccName
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index cde9e02d83..1f3ee6df07 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -34,8 +34,8 @@ module IfaceType (
         pprIfaceContext, pprIfaceContextArr,
         pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
         pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
-        pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType,
-        pprIfaceTyLit,
+        pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
+        pprIfaceSigmaType, pprIfaceTyLit,
         pprIfaceCoercion, pprParendIfaceCoercion,
         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
         pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
@@ -744,6 +744,11 @@ pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
 pprIfaceForAllPart 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 tvs sdoc
   = sep [ pprIfaceForAllCo tvs, sdoc ]
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 029ae28b7a..f0236b826a 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1430,8 +1430,7 @@ reifyTyCon tc
   = do  { cxt <- reifyCxt (tyConStupidTheta tc)
         ; let tvs      = tyConTyVars tc
               dataCons = tyConDataCons tc
-              -- see Note [Reifying GADT data constructors]
-              isGadt   = any (not . null . dataConEqSpec) dataCons
+              isGadt   = isGadtSyntaxTyCon tc
         ; cons <- mapM (reifyDataCon isGadt (mkTyVarTys tvs)) dataCons
         ; r_tvs <- reifyTyVars tvs (Just tc)
         ; let name = reifyName tc
@@ -1443,7 +1442,6 @@ reifyTyCon tc
         ; return (TH.TyConI decl) }
 
 reifyDataCon :: Bool -> [Type] -> DataCon -> TcM TH.Con
--- For GADTs etc, see Note [Reifying GADT data constructors]
 reifyDataCon isGadtDataCon tys dc
   = do { let -- used for H98 data constructors
              (ex_tvs, theta, arg_tys)
@@ -1505,34 +1503,9 @@ reifyDataCon isGadtDataCon tys dc
          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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-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:
+Suppose one were to reify this GADT:
 
   data a :~: b where
     Refl :: forall a b. (a ~ b) => a :~: b
@@ -1697,8 +1670,7 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
                  eta_expanded_tvs = mkTyVarTys fam_tvs `chkAppend` etad_tys
                  eta_expanded_lhs = lhs `chkAppend` etad_tys
                  dataCons         = tyConDataCons rep_tc
-                 -- see Note [Reifying GADT data constructors]
-                 isGadt   = any (not . null . dataConEqSpec) dataCons
+                 isGadt           = isGadtSyntaxTyCon rep_tc
            ; cons <- mapM (reifyDataCon isGadt eta_expanded_tvs) dataCons
            ; let types_only = filterOutInvisibleTypes fam_tc eta_expanded_lhs
            ; th_tys <- reifyTypes types_only
diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst
index 8f61ef86fe..96fbdd4886 100644
--- a/docs/users_guide/8.4.1-notes.rst
+++ b/docs/users_guide/8.4.1-notes.rst
@@ -124,6 +124,12 @@ Runtime system
 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
 ~~~~~~~~~~~~~~~
 
diff --git a/testsuite/tests/ghci/scripts/T7730.stdout b/testsuite/tests/ghci/scripts/T7730.stdout
index e96e909413..bf9c1d025b 100644
--- a/testsuite/tests/ghci/scripts/T7730.stdout
+++ b/testsuite/tests/ghci/scripts/T7730.stdout
@@ -3,6 +3,5 @@ data A (x :: k) (y :: k1)
   	-- Defined at <interactive>:2:1
 A :: k1 -> k2 -> *
 type role T phantom
-data T (a :: k) where
-  MkT :: forall k (a :: k) a1. a1 -> T a
+data T (a :: k) = forall a1. MkT a1
   	-- Defined at <interactive>:6:1
diff --git a/testsuite/tests/ghci/scripts/T7873.stdout b/testsuite/tests/ghci/scripts/T7873.stdout
index 2c79056da4..bcdebe71e1 100644
--- a/testsuite/tests/ghci/scripts/T7873.stdout
+++ b/testsuite/tests/ghci/scripts/T7873.stdout
@@ -1,5 +1,5 @@
-data D2 where
-  MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2
+data D2
+  = forall k. MkD2 (forall (p :: k -> *) (a :: k). p a -> Int)
   	-- Defined at <interactive>:3:1
 data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int)
   	-- Defined at <interactive>:4:1
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index d51b345d5c..1ae9bd54d0 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -4,19 +4,22 @@ type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
 type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol)
                                    (b :: GHC.Types.Symbol)
             :: Ordering
-data GHC.TypeLits.ErrorMessage where
-  GHC.TypeLits.Text :: GHC.Types.Symbol -> GHC.TypeLits.ErrorMessage
-  GHC.TypeLits.ShowType :: t -> GHC.TypeLits.ErrorMessage
-  (GHC.TypeLits.:<>:) :: GHC.TypeLits.ErrorMessage
-                         -> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage
-  (GHC.TypeLits.:$$:) :: GHC.TypeLits.ErrorMessage
-                         -> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage
+data GHC.TypeLits.ErrorMessage
+  = GHC.TypeLits.Text GHC.Types.Symbol
+  | forall t. GHC.TypeLits.ShowType t
+  | GHC.TypeLits.ErrorMessage
+    GHC.TypeLits.:<>:
+    GHC.TypeLits.ErrorMessage
+  | GHC.TypeLits.ErrorMessage
+    GHC.TypeLits.:$$:
+    GHC.TypeLits.ErrorMessage
 class GHC.TypeLits.KnownSymbol (n :: GHC.Types.Symbol) where
   GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n
   {-# MINIMAL symbolSing #-}
-data GHC.TypeLits.SomeSymbol where
-  GHC.TypeLits.SomeSymbol :: GHC.TypeLits.KnownSymbol n =>
-                             (Data.Proxy.Proxy n) -> GHC.TypeLits.SomeSymbol
+data GHC.TypeLits.SomeSymbol
+  = forall (n :: GHC.Types.Symbol).
+    GHC.TypeLits.KnownSymbol n =>
+    GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
 type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
             :: b
 GHC.TypeLits.natVal ::
@@ -54,9 +57,10 @@ class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where
   GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
   {-# MINIMAL natSing #-}
 data GHC.Types.Nat
-data GHC.TypeNats.SomeNat where
-  GHC.TypeNats.SomeNat :: GHC.TypeNats.KnownNat n =>
-                          (Data.Proxy.Proxy n) -> GHC.TypeNats.SomeNat
+data GHC.TypeNats.SomeNat
+  = forall (n :: GHC.Types.Nat).
+    GHC.TypeNats.KnownNat n =>
+    GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
 data GHC.Types.Symbol
 type family (GHC.TypeNats.^) (a :: GHC.Types.Nat)
                              (b :: GHC.Types.Nat)
diff --git a/testsuite/tests/ghci/scripts/ghci030.stdout b/testsuite/tests/ghci/scripts/ghci030.stdout
index 9344bc39bd..49ce606456 100644
--- a/testsuite/tests/ghci/scripts/ghci030.stdout
+++ b/testsuite/tests/ghci/scripts/ghci030.stdout
@@ -1,6 +1,2 @@
-data D where
-  C :: (Int -> a) -> Char -> D
-  	-- Defined at ghci030.hs:8:1
-data D where
-  C :: (Int -> a) -> Char -> D
-  	-- Defined at ghci030.hs:8:10
+data D = forall a. C (Int -> a) Char 	-- Defined at ghci030.hs:8:1
+data D = forall a. C (Int -> a) Char 	-- Defined at ghci030.hs:8:10
diff --git a/testsuite/tests/rename/should_fail/rnfail055.stderr b/testsuite/tests/rename/should_fail/rnfail055.stderr
index 7fc5d80bad..b9ba174519 100644
--- a/testsuite/tests/rename/should_fail/rnfail055.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail055.stderr
@@ -71,10 +71,8 @@ RnFail055.hs-boot:25:1: error:
     Type constructor ‘T7’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role T7 phantom
-                 data T7 a where
-                   T7 :: a1 -> T7 a
-    Boot file:   data T7 a where
-                   T7 :: a -> T7 a
+                 data T7 a = forall a1. T7 a1
+    Boot file:   data T7 a = forall b. T7 a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
     The constructors do not match: The types for ‘T7’ differ
diff --git a/testsuite/tests/th/T4188.stderr b/testsuite/tests/th/T4188.stderr
index 2e4155fd8b..38a22cf172 100644
--- a/testsuite/tests/th/T4188.stderr
+++ b/testsuite/tests/th/T4188.stderr
@@ -1,8 +1,9 @@
-data T4188.T1 (a_0 :: *) = forall (b_1 :: *) . T4188.MkT1 a_0 b_1
-data T4188.T2 (a_0 :: *)
-    = forall (b_1 :: *) . (T4188.C a_0, T4188.C b_1) => T4188.MkT2 a_0
-                                                                   b_1
+data T4188.T1 (a_0 :: *) where
+    T4188.MkT1 :: forall (a_1 :: *) (b_2 :: *) . a_1 ->
+                                                 b_2 -> T4188.T1 a_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
     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)
-
diff --git a/testsuite/tests/typecheck/should_fail/T3468.stderr b/testsuite/tests/typecheck/should_fail/T3468.stderr
index 1f8bdcb11b..0a0fec223b 100644
--- a/testsuite/tests/typecheck/should_fail/T3468.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3468.stderr
@@ -3,7 +3,6 @@ T3468.hs-boot:3:1: error:
     Type constructor ‘Tool’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role Tool phantom
-                 data Tool d where
-                   F :: a -> Tool d
+                 data Tool d = forall a r. F a
     Boot file:   data Tool
     The types have different kinds