Print explicit foralls in type family eqns when appropriate

Summary:
When `-fprint-explicit-foralls` is enabled, type family
equations are either printed without an explict `forall` entirely,
or with a bizarre square bracket syntax (in the case of closed type
families). I find neither satisfying, so in this patch, I introduce
support for printing explicit `forall`s in open type-family, closed
type-family, and data-family equations when appropriate. (By "when
appropriate", I refer to the conditions laid out in
`Note [When to print foralls]` in `IfaceType`.)

One tricky point in the implementation is that I had to pick a
visibility for each type variable in a `CoAxiom`/`FamInst` in order
to be able to pass it to `pprUserIfaceForAll` //et al.// Because
the type variables in a type family instance equation can't be
instantiated by the programmer anyway, the choice only really matters
for pretty-printing purposes, so I simply went with good ol'
trustworthy `Specified`. (This design choice is documented in
`Note [Printing foralls in type family instances]` in `IfaceType`.)

Test Plan: make test TEST=T15827

Reviewers: goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, carter

GHC Trac Issues: #15827

Differential Revision: https://phabricator.haskell.org/D5282

13 files changed, 138 insertions, 52 deletions

diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 4d70b11973..2e63fbc22f 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -64,12 +64,11 @@ import SrcLoc
 import Fingerprint
 import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
-import Var( VarBndr(..) )
+import Var( VarBndr(..), binderVar )
 import TyCon ( Role (..), Injectivity(..) )
 import Util( dropList, filterByList )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
 import Lexeme (isLexSym)
-import DynFlags
 
 import Control.Monad
 import System.IO.Unsafe
@@ -558,7 +557,6 @@ pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
 -- be a branch for an imported TyCon, so it would be an ExtName
 -- So it's easier to take an SDoc here
 pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
-                                 , ifaxbCoVars = cvs
                                  , ifaxbLHS = pat_tys
                                  , ifaxbRHS = rhs
                                  , ifaxbIncomps = incomps })
@@ -566,16 +564,8 @@ pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
     $+$
     nest 2 maybe_incomps
   where
-    ppr_binders = sdocWithDynFlags $ \dflags ->
-                  ppWhen (gopt Opt_PrintExplicitForalls dflags) ppr_binders'
-
-    ppr_binders'
-      | null tvs && null cvs = empty
-      | null cvs
-      = brackets (pprWithCommas (pprIfaceTvBndr True) tvs)
-      | otherwise
-      = brackets (pprWithCommas (pprIfaceTvBndr True) tvs <> semi <+>
-                  pprWithCommas pprIfaceIdBndr cvs)
+    -- See Note [Printing foralls in type family instances] in IfaceType
+    ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
     pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
     maybe_incomps = ppUnless (null incomps) $ parens $
                     text "incompatible indices:" <+> ppr incomps
@@ -718,6 +708,12 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
                      , nest 2 $ ppShowIface ss pp_extra ]
   where
     is_data_instance = isIfaceDataInstance parent
+    -- See Note [Printing foralls in type family instances] in IfaceType
+    pp_data_inst_forall :: SDoc
+    pp_data_inst_forall = pprUserIfaceForAll forall_bndrs
+
+    forall_bndrs :: [IfaceForAllBndr]
+    forall_bndrs = [Bndr (binderVar tc_bndr) Specified | tc_bndr <- binders]
 
     cons       = visibleIfConDecls condecls
     pp_where   = ppWhen (gadt && not (null cons)) $ text "where"
@@ -728,7 +724,9 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
 
     pp_lhs = case parent of
                IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing
-               _          -> text "instance" <+> pprIfaceTyConParent parent
+               IfDataInstance{}
+                          -> text "instance" <+> pp_data_inst_forall
+                                             <+> pprIfaceTyConParent parent
 
     pp_roles
       | is_data_instance = empty
@@ -821,11 +819,16 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon
   = text "data family" <+> pprIfaceDeclHead [] ss tycon binders Nothing
 
   | otherwise
-  = hang (text "type family" <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind))
+  = hang (text "type family"
+            <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind)
+            <+> ppShowRhs ss (pp_where rhs))
        2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
     $$
     nest 2 (ppShowRhs ss (pp_branches rhs))
   where
+    pp_where (IfaceClosedSynFamilyTyCon {}) = text "where"
+    pp_where _                              = empty
+
     pp_inj Nothing    _   = empty
     pp_inj (Just res) inj
        | Injective injectivity <- inj = hsep [ equals, ppr res
@@ -848,13 +851,12 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon
       = ppShowIface ss (text "built-in")
 
     pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs)))
-      = hang (text "where")
-           2 (vcat (map (pprAxBranch
-                           (pprPrefixIfDeclBndr
-                             (ss_how_much ss)
-                             (occName tycon))
-                        ) brs)
-              $$ ppShowIface ss (text "axiom" <+> ppr ax))
+      = vcat (map (pprAxBranch
+                     (pprPrefixIfDeclBndr
+                       (ss_how_much ss)
+                       (occName tycon))
+                  ) brs)
+        $$ ppShowIface ss (text "axiom" <+> ppr ax)
     pp_branches _ = Outputable.empty
 
 pprIfaceDecl _ (IfacePatSyn { ifName = name,
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index e2ea655194..25000737a6 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -21,6 +21,7 @@ module IfaceType (
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
         IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
+        mkIfaceForAllTvBndr,
 
         ifForAllBndrVar, ifForAllBndrName,
         ifTyConBinderVar, ifTyConBinderName,
@@ -158,6 +159,10 @@ data IfaceTyLit
 type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
 type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
 
+-- | Make an 'IfaceForAllBndr' from an 'IfaceTvBndr'.
+mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr
+mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis
+
 -- | Stores the arguments in a type application as a list.
 -- See @Note [Suppressing invisible arguments]@.
 data IfaceAppArgs
@@ -1091,6 +1096,54 @@ criteria are met:
 
 N.B. Until now (Aug 2018) we didn't check anything for coercion variables.
 
+Note [Printing foralls in type family instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use the same criteria as in Note [When to print foralls] to determine
+whether a type family instance should be pretty-printed with an explicit
+`forall`. Example:
+
+  type family Foo (a :: k) :: k where
+    Foo Maybe       = []
+    Foo (a :: Type) = Int
+    Foo a           = a
+
+Without -fprint-explicit-foralls enabled, this will be pretty-printed as:
+
+type family Foo (a :: k) :: k where
+  Foo Maybe = []
+  Foo a = Int
+  forall k (a :: k). Foo a = a
+
+Note that only the third equation has an explicit forall, since it has a type
+variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then
+the second equation would be preceded with `forall a.`.)
+
+There is one tricky point in the implementation: what visibility
+do we give the type variables in a type family instance? Type family instances
+only store type *variables*, not type variable *binders*, and only the latter
+has visibility information. We opt to default the visibility of each of these
+type variables to Specified because users can't ever instantiate these
+variables manually, so the choice of visibility is only relevant to
+pretty-printing. (This is why the `k` in `forall k (a :: k). ...` above is
+printed the way it is, even though it wasn't written explicitly in the
+original source code.)
+
+We adopt the same strategy for data family instances. Example:
+
+  data family DF (a :: k)
+  data instance DF '[a, b] = DFList
+
+That data family instance is pretty-printed as:
+
+  data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList
+
+This is despite that the representation tycon for this data instance (call it
+$DF:List) actually has different visibilities for its binders.
+However, the visibilities of these binders are utterly irrelevant to the
+programmer, who cares only about the specificity of variables in `DF`'s type,
+not $DF:List's type. Therefore, we opt to pretty-print all variables in data
+family instances as Specified.
+
 Note [Printing promoted type constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this GHCi session (Trac #14343)
diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs
index b0a72cf499..b1ed2b2059 100644
--- a/compiler/main/PprTyThing.hs
+++ b/compiler/main/PprTyThing.hs
@@ -21,7 +21,7 @@ module PprTyThing (
 
 import GhcPrelude
 
-import Type    ( TyThing(..) )
+import Type    ( ArgFlag(..), TyThing(..), mkTyVarBinders, pprUserForAll )
 import IfaceSyn ( ShowSub(..), ShowHowMuch(..), AltPpr(..)
   , showToHeader, pprIfaceDecl )
 import CoAxiom ( coAxiomTyCon )
@@ -117,9 +117,13 @@ pprFamInst (FamInst { fi_flavor = DataFamilyInst rep_tc })
   = pprTyThingInContextLoc (ATyCon rep_tc)
 
 pprFamInst (FamInst { fi_flavor = SynFamilyInst, fi_axiom = axiom
-                    , fi_tys = lhs_tys, fi_rhs = rhs })
+                    , fi_tvs = tvs, fi_tys = lhs_tys, fi_rhs = rhs })
   = showWithLoc (pprDefinedAt (getName axiom)) $
-    hang (text "type instance" <+> pprTypeApp (coAxiomTyCon axiom) lhs_tys)
+    hang (text "type instance"
+            <+> pprUserForAll (mkTyVarBinders Specified tvs)
+                -- See Note [Printing foralls in type family instances]
+                -- in IfaceType
+            <+> pprTypeApp (coAxiomTyCon axiom) lhs_tys)
        2 (equals <+> ppr rhs)
 
 ----------------------------
diff --git a/testsuite/tests/ghci/scripts/T13420.stdout b/testsuite/tests/ghci/scripts/T13420.stdout
index e6b81adc41..c6dbaf2755 100644
--- a/testsuite/tests/ghci/scripts/T13420.stdout
+++ b/testsuite/tests/ghci/scripts/T13420.stdout
@@ -1,6 +1,5 @@
-type family F a :: *
-  where
-      F [Int] = Bool
-      F [a] = Double
-      F (a b) = Char
+type family F a :: * where
+    F [Int] = Bool
+    F [a] = Double
+    F (a b) = Char
   	-- Defined at T13420.hs:4:1
diff --git a/testsuite/tests/ghci/scripts/T15341.stdout b/testsuite/tests/ghci/scripts/T15341.stdout
index 0633ae5b39..e2555f9ac9 100644
--- a/testsuite/tests/ghci/scripts/T15341.stdout
+++ b/testsuite/tests/ghci/scripts/T15341.stdout
@@ -1,6 +1,6 @@
-type family Foo (a :: k) :: k
-  where Foo a = a
+type family Foo (a :: k) :: k where
+  forall k (a :: k). Foo a = a
   	-- Defined at T15341.hs:5:1
-type family Foo @k (a :: k) :: k
-  where Foo @k a = a
+type family Foo @k (a :: k) :: k where
+  forall k (a :: k). Foo @k a = a
   	-- Defined at T15341.hs:5:1
diff --git a/testsuite/tests/ghci/scripts/T15827.hs b/testsuite/tests/ghci/scripts/T15827.hs
new file mode 100644
index 0000000000..ba67534e62
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15827.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15827 where
+
+import Data.Kind
+import Data.Proxy
+
+type family F1 (a :: k)
+type instance forall k (a :: k). F1 a = Proxy a
+
+type family F2 (a :: k) :: Type where
+  forall k (a :: k). F2 a = Proxy a
+
+data family D (a :: k)
+data instance forall k (a :: k). D a = MkD (Proxy a)
diff --git a/testsuite/tests/ghci/scripts/T15827.script b/testsuite/tests/ghci/scripts/T15827.script
new file mode 100644
index 0000000000..a05fcd8a2d
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15827.script
@@ -0,0 +1,4 @@
+:load T15827
+:info F1
+:info F2
+:info D
diff --git a/testsuite/tests/ghci/scripts/T15827.stdout b/testsuite/tests/ghci/scripts/T15827.stdout
new file mode 100644
index 0000000000..50df504e58
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15827.stdout
@@ -0,0 +1,9 @@
+type family F1 (a :: k) :: * 	-- Defined at T15827.hs:9:1
+type instance forall k (a :: k). F1 a = Proxy a
+  	-- Defined at T15827.hs:10:34
+type family F2 (a :: k) :: * where
+  forall k (a :: k). F2 a = Proxy a
+  	-- Defined at T15827.hs:12:1
+data family D (a :: k) 	-- Defined at T15827.hs:15:1
+data instance forall k (a :: k). D a = MkD (Proxy a)
+  	-- Defined at T15827.hs:16:34
diff --git a/testsuite/tests/ghci/scripts/T4175.stdout b/testsuite/tests/ghci/scripts/T4175.stdout
index e95d9c76af..de4e28c46f 100644
--- a/testsuite/tests/ghci/scripts/T4175.stdout
+++ b/testsuite/tests/ghci/scripts/T4175.stdout
@@ -11,10 +11,9 @@ class C a where
   	-- Defined at T4175.hs:16:5
 type instance D () () = Bool 	-- Defined at T4175.hs:22:10
 type instance D Int () = String 	-- Defined at T4175.hs:19:10
-type family E a :: *
-  where
-      E () = Bool
-      E Int = String
+type family E a :: * where
+    E () = Bool
+    E Int = String
   	-- Defined at T4175.hs:24:1
 data () = () 	-- Defined in ‘GHC.Tuple’
 instance [safe] C () -- Defined at T4175.hs:21:10
diff --git a/testsuite/tests/ghci/scripts/T7939.stdout b/testsuite/tests/ghci/scripts/T7939.stdout
index 82a8658906..4c2a602f4f 100644
--- a/testsuite/tests/ghci/scripts/T7939.stdout
+++ b/testsuite/tests/ghci/scripts/T7939.stdout
@@ -5,23 +5,21 @@ Bar :: k -> * -> *
 type family F a :: * 	-- Defined at T7939.hs:8:1
 type instance F Int = Bool 	-- Defined at T7939.hs:9:15
 F :: * -> *
-type family G a :: *
-  where G Int = Bool
+type family G a :: * where
+    G Int = Bool
   	-- Defined at T7939.hs:11:1
 G :: * -> *
-type family H (a :: Bool) :: Bool
-  where H 'False = 'True
+type family H (a :: Bool) :: Bool where
+    H 'False = 'True
   	-- Defined at T7939.hs:14:1
 H :: Bool -> Bool
-type family J (a :: [k]) :: Bool
-  where
-      J '[] = 'False
-      J (h : t) = 'True
+type family J (a :: [k]) :: Bool where
+    J '[] = 'False
+  forall k (h :: k) (t :: [k]). J (h : t) = 'True
   	-- Defined at T7939.hs:17:1
 J :: [k] -> Bool
-type family K (a1 :: [a]) :: Maybe a
-  where
-      K '[] = 'Nothing
-      K (h : t) = 'Just h
+type family K (a1 :: [a]) :: Maybe a where
+    K '[] = 'Nothing
+  forall a (h :: a) (t :: [a]). K (h : t) = 'Just h
   	-- Defined at T7939.hs:21:1
 K :: [a] -> Maybe a
diff --git a/testsuite/tests/ghci/scripts/T8674.stdout b/testsuite/tests/ghci/scripts/T8674.stdout
index 45d4f0af0e..d938f95692 100644
--- a/testsuite/tests/ghci/scripts/T8674.stdout
+++ b/testsuite/tests/ghci/scripts/T8674.stdout
@@ -1,3 +1,4 @@
 data family Sing (a :: k) 	-- Defined at T8674.hs:4:1
 data instance Sing Bool = SBool 	-- Defined at T8674.hs:6:15
-data instance Sing a = SNil 	-- Defined at T8674.hs:5:15
+data instance forall k (a :: [k]). Sing a = SNil
+  	-- Defined at T8674.hs:5:15
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index 5e520fb0a2..a30879c316 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -21,7 +21,7 @@ data GHC.TypeLits.SomeSymbol
     GHC.TypeLits.KnownSymbol n =>
     GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
 type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
-            :: b
+            :: b where
 GHC.TypeLits.natVal ::
   GHC.TypeNats.KnownNat n => proxy n -> Integer
 GHC.TypeLits.natVal' ::
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 493daa4412..82197072c7 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -288,4 +288,5 @@ test('T15568', normal, ghci_script, ['T15568.script'])
 test('T15325', normal, ghci_script, ['T15325.script'])
 test('T15591', normal, ghci_script, ['T15591.script'])
 test('T15743b', normal, ghci_script, ['T15743b.script'])
+test('T15827', normal, ghci_script, ['T15827.script'])
 test('T15898', normal, ghci_script, ['T15898.script'])