Print for-alls more often (Trac #9018)

We now display the foralls of a type if any of the type variables
is polykinded.  This put kind polymorphism "in your face" a bit more
often, but eliminates a lot of head scratching.

The user manual reflects the new behaviour.

12 files changed, 74 insertions, 35 deletions

diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs
index 1fd5d0cbcf..01932f6553 100644
--- a/compiler/main/PprTyThing.hs
+++ b/compiler/main/PprTyThing.hs
@@ -156,19 +156,16 @@ pprId ident
 pprTypeForUser :: Type -> SDoc
 -- We do two things here.
 -- a) We tidy the type, regardless
--- b) If Opt_PrintExplicitForAlls is True, we discard the foralls
--- 	but we do so `deeply'
+-- b) Swizzle the foralls to the top, so that without
+--    -fprint-explicit-foralls we'll suppress all the foralls
 -- Prime example: a class op might have type
 --	forall a. C a => forall b. Ord b => stuff
 -- Then we want to display
 --	(C a, Ord b) => stuff
 pprTypeForUser ty
-  = sdocWithDynFlags $ \ dflags ->
-    if gopt Opt_PrintExplicitForalls dflags
-    then ppr tidy_ty
-    else ppr (mkPhiTy ctxt ty')
+  = pprSigmaType (mkSigmaTy tvs ctxt tau)
   where
-    (_, ctxt, ty') = tcSplitSigmaTy tidy_ty
+    (tvs, ctxt, tau) = tcSplitSigmaTy tidy_ty
     (_, tidy_ty)   = tidyOpenType emptyTidyEnv ty
      -- Often the types/kinds we print in ghci are fully generalised
      -- and have no free variables, but it turns out that we sometimes
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 0355dab9c7..4b86fa02fc 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -1741,11 +1741,14 @@ pprSkolInfo ArrowSkol       = ptext (sLit "the arrow form")
 pprSkolInfo (PatSkol cl mc) = case cl of
     RealDataCon dc -> sep [ ptext (sLit "a pattern with constructor")
                           , nest 2 $ ppr dc <+> dcolon
-                            <+> ppr (dataConUserType dc) <> comma
+                            <+> pprType (dataConUserType dc) <> comma
+                            -- pprType prints forall's regardless of -fprint-explict-foralls
+                            -- which is what we want here, since we might be saying
+                            -- type variable 't' is bound by ...
                           , ptext (sLit "in") <+> pprMatchContext mc ]
     PatSynCon ps -> sep [ ptext (sLit "a pattern with pattern synonym")
                         , nest 2 $ ppr ps <+> dcolon
-                          <+> ppr (varType (patSynId ps)) <> comma
+                          <+> pprType (varType (patSynId ps)) <> comma
                         , ptext (sLit "in") <+> pprMatchContext mc ]
 pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of")
                                   , vcat [ ppr name <+> dcolon <+> ppr ty
diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index bea67b4e3b..5787d87f0f 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -603,6 +603,8 @@ ppr_type p fun_ty@(FunTy ty1 ty2)
 ppr_forall_type :: Prec -> Type -> SDoc
 ppr_forall_type p ty
   = maybeParen p FunPrec $ ppr_sigma_type True ty
+    -- True <=> we always print the foralls on *nested* quantifiers
+    -- Opt_PrintExplicitForalls only affects top-level quantifiers
 
 ppr_tvar :: TyVar -> SDoc
 ppr_tvar tv  -- Note [Infix type variables]
@@ -618,24 +620,22 @@ ppr_tylit _ tl =
 ppr_sigma_type :: Bool -> Type -> SDoc
 -- Bool <=> Show the foralls
 ppr_sigma_type show_foralls ty
-  = sdocWithDynFlags $ \ dflags -> 
-    let filtered_tvs | gopt Opt_PrintExplicitKinds dflags 
-                     = tvs
-                     | otherwise
-                     = filterOut isKindVar tvs
-    in sep [ ppWhen show_foralls (pprForAll filtered_tvs)
-           , pprThetaArrowTy ctxt
-           , pprType tau ]
+  = sep [ ppWhen (show_foralls || any tv_has_kind_var tvs)
+                 (pprForAll tvs)
+                -- See Note [When to print foralls]
+        , pprThetaArrowTy ctxt
+        , pprType tau ]
   where
     (tvs,  rho) = split1 [] ty
     (ctxt, tau) = split2 [] rho
 
     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
-    split1 tvs ty          = (reverse tvs, ty)
+    split1 tvs ty               = (reverse tvs, ty)
  
     split2 ps (ty1 `FunTy` ty2) | isPredTy ty1 = split2 (ty1:ps) ty2
     split2 ps ty                               = (reverse ps, ty)
 
+    tv_has_kind_var tv = not (isEmptyVarSet (tyVarsOfType (tyVarKind tv)))
 
 pprSigmaType :: Type -> SDoc
 pprSigmaType ty = sdocWithDynFlags $ \dflags ->
@@ -656,6 +656,24 @@ pprTvBndr tv
 	       kind = tyVarKind tv
 \end{code}
 
+Note [When to print foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Mostly we want to print top-level foralls when (and only when) the user specifies
+-fprint-explicit-foralls.  But when kind polymorphism is at work, that suppresses
+too much information; see Trac #9018.
+
+So I'm trying out this rule: print explicit foralls if
+  a) User specifies -fprint-explicit-foralls, or
+  b) Any of the quantified type variables has a kind 
+     that mentions a kind variable
+
+This catches common situations, such as a type siguature
+     f :: m a
+which means
+      f :: forall k. forall (m :: k->*) (a :: k). m a
+We really want to see both the "forall k" and the kind signatures
+on m and a.  The latter comes from pprTvBndr.
+
 Note [Infix type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 With TypeOperators you can say
diff --git a/docs/users_guide/using.xml b/docs/users_guide/using.xml
index 8d8211eb5a..9d145f6369 100644
--- a/docs/users_guide/using.xml
+++ b/docs/users_guide/using.xml
@@ -899,20 +899,37 @@ ghci> :set -fprint-explicit-foralls
 ghci> :t f
 f :: forall a. a -> a
 </screen>
-         Using <option>-fprint-explicit-kinds</option> makes GHC print kind-foralls and kind applications
+However, regardless of the flag setting, the quantifiers are printed under these circumstances:
+<itemizedlist>
+<listitem><para>For nested <literal>foralls</literal>, e.g.
+<screen>
+ghci> :t GHC.ST.runST
+GHC.ST.runST :: (forall s. GHC.ST.ST s a) -> a
+</screen>
+</para></listitem>
+<listitem><para>If any of the quantified type variables has a kind
+that mentions a kind variable, e.g.
+<screen>
+ghci> :i Data.Coerce.coerce
+coerce ::
+  forall (k :: BOX) (a :: k) (b :: k). Coercible a b => a -> b
+     -- Defined in GHC.Prim
+</screen>
+</para></listitem>
+</itemizedlist>
+          </para>
+          <para>
+         Using <option>-fprint-explicit-kinds</option> makes GHC print kind arguments
          in types, which are normally suppressed.  This can be important when you are using kind polymorphism.
          For example:
 <screen>
 ghci> :set -XPolyKinds
 ghci> data T a = MkT
 ghci> :t MkT
-MkT :: T b
+MkT :: forall (k :: BOX) (a :: k). T a
 ghci> :set -fprint-explicit-foralls
 ghci> :t MkT
-MkT :: forall (b::k). T b
-ghci> :set -fprint-explicit-kinds
-ghci> :t MkT
-MkT :: forall (k::BOX) (b:k). T b
+MkT :: forall (k :: BOX) (a :: k). T k a
 </screen>
          </para>
         </listitem>
diff --git a/testsuite/tests/ghci/scripts/T7873.stdout b/testsuite/tests/ghci/scripts/T7873.stdout
index 0167fb2eba..6f9f55a8af 100644
--- a/testsuite/tests/ghci/scripts/T7873.stdout
+++ b/testsuite/tests/ghci/scripts/T7873.stdout
@@ -1,5 +1,6 @@
 data D1 where
-  MkD1 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D1
+  MkD1 :: (forall (k :: BOX) (p :: k -> *) (a :: k).
+           p a -> Int) -> D1
   	-- Defined at <interactive>:3:1
 data D2 where
   MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2
diff --git a/testsuite/tests/ghci/scripts/ghci059.stdout b/testsuite/tests/ghci/scripts/ghci059.stdout
index 6b2c8f886e..ffc893f363 100644
--- a/testsuite/tests/ghci/scripts/ghci059.stdout
+++ b/testsuite/tests/ghci/scripts/ghci059.stdout
@@ -1,4 +1,6 @@
 type role Coercible representational representational
 class Coercible (a :: k) (b :: k)
   	-- Defined in ‘GHC.Types’
-coerce :: Coercible a b => a -> b 	-- Defined in ‘GHC.Prim’
+coerce ::
+  forall (k :: BOX) (a :: k) (b :: k). Coercible a b => a -> b
+  	-- Defined in ‘GHC.Prim’
diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr
index 9652643802..b081ed69b4 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr
@@ -3,7 +3,7 @@ T7786.hs:86:22:
     Couldn't match type ‘xxx’ with ‘'Empty’
     Inaccessible code in
       a pattern with constructor
-        Nil :: Sing 'Empty,
+        Nil :: forall (k :: BOX). Sing 'Empty,
       in a pattern binding in
            'do' block
     In the pattern: Nil
diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr
index 7e1a7ab88f..0c34249223 100644
--- a/testsuite/tests/polykinds/T7230.stderr
+++ b/testsuite/tests/polykinds/T7230.stderr
@@ -7,13 +7,13 @@ T7230.hs:48:32:
       at T7230.hs:47:10-68
     or from (xs ~ (x : xs1))
       bound by a pattern with constructor
-                 SCons :: forall (x :: k) (xs :: [k]).
+                 SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
                           Sing x -> Sing xs -> Sing (x : xs),
                in an equation for ‘crash’
       at T7230.hs:48:8-27
     or from (xs1 ~ (x1 : xs2))
       bound by a pattern with constructor
-                 SCons :: forall (x :: k) (xs :: [k]).
+                 SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
                           Sing x -> Sing xs -> Sing (x : xs),
                in an equation for ‘crash’
       at T7230.hs:48:17-26
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index b126621ce1..509dcc4b90 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -4,7 +4,7 @@ T7438.hs:6:14:
       ‘t’ is untouchable
         inside the constraints (t2 ~ t3)
         bound by a pattern with constructor
-                   Nil :: forall (a :: k). Thrist a a,
+                   Nil :: forall (k :: BOX) (a :: k). Thrist a a,
                  in an equation for ‘go’
         at T7438.hs:6:4-6
       ‘t’ is a rigid type variable bound by
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 4638fd8c4d..ad0d15e69c 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -6,7 +6,8 @@ T8566.hs:31:9:
       bound by the instance declaration at T8566.hs:29:10-67
     or from ('AA t (a : as) ~ 'AA t1 as1)
       bound by a pattern with constructor
-                 A :: forall (r :: [*]) (t :: k) (as :: [U *]). I ('AA t as) r,
+                 A :: forall (r :: [*]) (k :: BOX) (t :: k) (as :: [U *]).
+                      I ('AA t as) r,
                in an equation for ‘c’
       at T8566.hs:31:5
     The type variable ‘fs0’ is ambiguous
diff --git a/testsuite/tests/roles/should_compile/Roles1.stderr b/testsuite/tests/roles/should_compile/Roles1.stderr
index cd027f13f2..de4ecf36e2 100644
--- a/testsuite/tests/roles/should_compile/Roles1.stderr
+++ b/testsuite/tests/roles/should_compile/Roles1.stderr
@@ -14,7 +14,7 @@ TYPE CONSTRUCTORS
     RecFlag NonRecursive, Promotable
     = K2 :: forall a. a -> T2 a Stricts: _
     FamilyInstance: none
-  T3 :: k -> *
+  T3 :: forall (k :: BOX). k -> *
   data T3 (k::BOX) (a::k)
     No C type associated
     Roles: [nominal, phantom]
@@ -35,14 +35,14 @@ TYPE CONSTRUCTORS
     RecFlag NonRecursive, Promotable
     = K5 :: forall a. a -> T5 a Stricts: _
     FamilyInstance: none
-  T6 :: k -> *
+  T6 :: forall (k :: BOX). k -> *
   data T6 (k::BOX) (a::k)
     No C type associated
     Roles: [nominal, phantom]
     RecFlag NonRecursive, Not promotable
     = K6 :: forall (k::BOX) (a::k). T6 k a
     FamilyInstance: none
-  T7 :: k -> * -> *
+  T7 :: forall (k :: BOX). k -> * -> *
   data T7 (k::BOX) (a::k) b
     No C type associated
     Roles: [nominal, phantom, representational]
diff --git a/testsuite/tests/th/TH_Roles2.stderr b/testsuite/tests/th/TH_Roles2.stderr
index bd44d12c6b..334d09dfd2 100644
--- a/testsuite/tests/th/TH_Roles2.stderr
+++ b/testsuite/tests/th/TH_Roles2.stderr
@@ -1,6 +1,6 @@
 TYPE SIGNATURES
 TYPE CONSTRUCTORS
-  T :: k -> *
+  T :: forall (k :: BOX). k -> *
   data T (k::BOX) (a::k)
     No C type associated
     Roles: [nominal, representational]