Overhaul -fprint-explicit-kinds to use VKA

This patch changes the behavior of `-fprint-explicit-kinds`
so that it displays kind argument using visible kind application.
In other words, the flag now:

1. Prints instantiations of specified variables with `@(...)`.
2. Prints instantiations of inferred variables with `@{...}`.

In addition, this patch removes the `Use -fprint-explicit-kinds to
see the kind arguments` error message that often arises when a type
mismatch occurs due to different kinds. Instead, whenever there is a
kind mismatch, we now enable the `-fprint-explicit-kinds` flag
locally to help cue to the programmer where the error lies.
(See `Note [Kind arguments in error messages]` in `TcErrors`.)
As a result, these funny `@{...}` things can now appear to the user
even without turning on the `-fprint-explicit-kinds` flag explicitly,
so I took the liberty of documenting them in the users' guide.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15871

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

12 files changed, 316 insertions, 185 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index 896303b55a..01cf47f039 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -740,6 +740,6 @@ rnIfaceForAllBndr :: Rename IfaceForAllBndr
 rnIfaceForAllBndr (Bndr tv vis) = Bndr <$> rnIfaceBndr tv <*> pure vis
 
 rnIfaceAppArgs :: Rename IfaceAppArgs
-rnIfaceAppArgs (IA_Invis t ts) = IA_Invis <$> rnIfaceType t <*> rnIfaceAppArgs ts
-rnIfaceAppArgs (IA_Vis t ts) = IA_Vis <$> rnIfaceType t <*> rnIfaceAppArgs ts
+rnIfaceAppArgs (IA_Arg t a ts) = IA_Arg <$> rnIfaceType t <*> pure a
+                                        <*> rnIfaceAppArgs ts
 rnIfaceAppArgs IA_Nil = pure IA_Nil
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs
index 5d84187cf0..bfa5e5fa7a 100644
--- a/compiler/basicTypes/Var.hs
+++ b/compiler/basicTypes/Var.hs
@@ -385,7 +385,7 @@ updateVarTypeM f id = do { ty' <- f (varType id)
 -- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
 data ArgFlag = Inferred | Specified | Required
   deriving (Eq, Ord, Data)
-  -- (<) on ArgFlag meant "is less visible than"
+  -- (<) on ArgFlag means "is less visible than"
 
 -- | Does this 'ArgFlag' classify an argument that is written in Haskell?
 isVisibleArgFlag :: ArgFlag -> Bool
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 7d1e697cdf..4d70b11973 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -954,9 +954,7 @@ pprIfaceTyConParent :: IfaceTyConParent -> SDoc
 pprIfaceTyConParent IfNoParent
   = Outputable.empty
 pprIfaceTyConParent (IfDataInstance _ tc tys)
-  = sdocWithDynFlags $ \dflags ->
-    let ftys = stripInvisArgs dflags tys
-    in pprIfaceTypeApp topPrec tc ftys
+  = pprIfaceTypeApp topPrec tc tys
 
 pprIfaceDeclHead :: IfaceContext -> ShowSub -> Name
                  -> [IfaceTyConBinder]   -- of the tycon, for invisible-suppression
@@ -1414,8 +1412,7 @@ freeNamesIfKind :: IfaceType -> NameSet
 freeNamesIfKind = freeNamesIfType
 
 freeNamesIfAppArgs :: IfaceAppArgs -> NameSet
-freeNamesIfAppArgs (IA_Vis   t ts) = freeNamesIfType t &&& freeNamesIfAppArgs ts
-freeNamesIfAppArgs (IA_Invis k ks) = freeNamesIfKind k &&& freeNamesIfAppArgs ks
+freeNamesIfAppArgs (IA_Arg t _ ts) = freeNamesIfType t &&& freeNamesIfAppArgs ts
 freeNamesIfAppArgs IA_Nil          = emptyNameSet
 
 freeNamesIfType :: IfaceType -> NameSet
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 4d6a3b3be3..e2ea655194 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -28,8 +28,8 @@ module IfaceType (
         -- Equality testing
         isIfaceLiftedTypeKind,
 
-        -- Conversion from IfaceAppArgs -> [IfaceType]
-        appArgsIfaceTypes,
+        -- Conversion from IfaceAppArgs to IfaceTypes/ArgFlags
+        appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
 
         -- Printing
         pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
@@ -158,21 +158,27 @@ data IfaceTyLit
 type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
 type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
 
--- See Note [Suppressing invisible arguments]
--- We use a new list type (rather than [(IfaceType,Bool)], because
--- it'll be more compact and faster to parse in interface
--- files. Rather than two bytes and two decisions (nil/cons, and
--- type/kind) there'll just be one.
+-- | Stores the arguments in a type application as a list.
+-- See @Note [Suppressing invisible arguments]@.
 data IfaceAppArgs
   = IA_Nil
-  | IA_Vis   IfaceType IfaceAppArgs   -- "Vis" means show when pretty-printing
-  | IA_Invis IfaceKind IfaceAppArgs   -- "Invis" means don't show when pretty-printing
-                                      --         except with -fprint-explicit-kinds
+  | IA_Arg IfaceType    -- The type argument
+
+           ArgFlag      -- The argument's visibility. We store this here so
+                        -- that we can:
+                        --
+                        -- 1. Avoid pretty-printing invisible (i.e., specified
+                        --    or inferred) arguments when
+                        --    -fprint-explicit-kinds isn't enabled, or
+                        -- 2. When -fprint-explicit-kinds *is*, enabled, print
+                        --    specified arguments in @(...) and inferred
+                        --    arguments in @{...}.
+
+           IfaceAppArgs -- The rest of the arguments
 
 instance Semi.Semigroup IfaceAppArgs where
-  IA_Nil <> xs           = xs
-  IA_Vis ty rest <> xs   = IA_Vis ty (rest Semi.<> xs)
-  IA_Invis ki rest <> xs = IA_Invis ki (rest Semi.<> xs)
+  IA_Nil <> xs              = xs
+  IA_Arg ty argf rest <> xs = IA_Arg ty argf (rest Semi.<> xs)
 
 instance Monoid IfaceAppArgs where
   mempty = IA_Nil
@@ -236,29 +242,29 @@ Here is how each equality predicate* is printed in homogeneous and
 heterogeneous contexts, depending on which combination of the
 -fprint-explicit-kinds and -fprint-equality-relations flags is used:
 
----------------------------------------------------------------------------------------
-|         Predicate             |        Neither flag        | -fprint-explicit-kinds |
-|-------------------------------|----------------------------|------------------------|
-| a ~ b         (homogeneous)   |        a ~ b               | (a :: *) ~  (b :: *)   |
-| a ~~ b,       homogeneously   |        a ~ b               | (a :: *) ~  (b :: *)   |
-| a ~~ b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
-| a ~# b,       homogeneously   |        a ~ b               | (a :: *) ~  (b :: *)   |
-| a ~# b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
-| Coercible a b (homogeneous)   |        Coercible a b       | Coercible * a b        |
-| a ~R# b,      homogeneously   |        Coercible a b       | Coercible * a b        |
-| a ~R# b,      heterogeneously |        a ~R# b             | (a :: *) ~R# (c :: k)  |
-|-------------------------------|----------------------------|------------------------|
-|         Predicate             | -fprint-equality-relations |      Both flags        |
-|-------------------------------|----------------------------|------------------------|
-| a ~ b         (homogeneous)   |        a ~  b              | (a :: *) ~  (b :: *)   |
-| a ~~ b,       homogeneously   |        a ~~ b              | (a :: *) ~~ (b :: *)   |
-| a ~~ b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
-| a ~# b,       homogeneously   |        a ~# b              | (a :: *) ~# (b :: *)   |
-| a ~# b,       heterogeneously |        a ~# c              | (a :: *) ~# (c :: k)   |
-| Coercible a b (homogeneous)   |        Coercible a b       | Coercible * a b        |
-| a ~R# b,      homogeneously   |        a ~R# b             | (a :: *) ~R# (b :: *)  |
-| a ~R# b,      heterogeneously |        a ~R# b             | (a :: *) ~R# (c :: k)  |
----------------------------------------------------------------------------------------
+--------------------------------------------------------------------------------------------
+|         Predicate             |        Neither flag        |    -fprint-explicit-kinds   |
+|-------------------------------|----------------------------|-----------------------------|
+| a ~ b         (homogeneous)   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| a ~# b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~# b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      homogeneously   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
+|-------------------------------|----------------------------|-----------------------------|
+|         Predicate             | -fprint-equality-relations |          Both flags         |
+|-------------------------------|----------------------------|-----------------------------|
+| a ~ b         (homogeneous)   |        a ~  b              | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       homogeneously   |        a ~~ b              | (a :: Type) ~~ (b :: Type)  |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| a ~# b,       homogeneously   |        a ~# b              | (a :: Type) ~# (b :: Type)  |
+| a ~# b,       heterogeneously |        a ~# c              | (a :: Type) ~# (c :: k)     |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      homogeneously   |        a ~R# b             | (a :: Type) ~R# (b :: Type) |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
+--------------------------------------------------------------------------------------------
 
 (* There is no heterogeneous, representational, lifted equality counterpart
 to (~~). There could be, but there seems to be no use for it.)
@@ -349,7 +355,8 @@ isIfaceLiftedTypeKind :: IfaceKind -> Bool
 isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
   = isLiftedTypeKindTyConName (ifaceTyConName tc)
 isIfaceLiftedTypeKind (IfaceTyConApp tc
-                       (IA_Vis (IfaceTyConApp ptr_rep_lifted IA_Nil) IA_Nil))
+                       (IA_Arg (IfaceTyConApp ptr_rep_lifted IA_Nil)
+                               Required IA_Nil))
   =  tc `ifaceTyConHasKey` tYPETyConKey
   && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
 isIfaceLiftedTypeKind _ = False
@@ -435,8 +442,7 @@ ifTypeIsVarFree ty = go ty
     go (IfaceCoercionTy {})    = False -- Safe
 
     go_args IA_Nil = True
-    go_args (IA_Vis   arg args) = go arg && go_args args
-    go_args (IA_Invis arg args) = go arg && go_args args
+    go_args (IA_Arg arg _ args) = go arg && go_args args
 
 {- Note [Substitution on IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -505,9 +511,8 @@ substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
   = go args
   where
-    go IA_Nil            = IA_Nil
-    go (IA_Vis ty tys)   = IA_Vis   (substIfaceType env ty) (go tys)
-    go (IA_Invis ty tys) = IA_Invis (substIfaceType env ty) (go tys)
+    go IA_Nil              = IA_Nil
+    go (IA_Arg ty arg tys) = IA_Arg (substIfaceType env ty) arg (go tys)
 
 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
 substIfaceTyVar env tv
@@ -530,25 +535,33 @@ stripInvisArgs dflags tys
     where
       suppress_invis c
         = case c of
-            IA_Nil        -> IA_Nil
-            IA_Invis _ ts -> suppress_invis ts
-            IA_Vis   t ts -> IA_Vis t $ suppress_invis ts
+            IA_Nil -> IA_Nil
+            IA_Arg t argf ts
+              |  isVisibleArgFlag argf
+              -> IA_Arg t argf $ suppress_invis ts
               -- Keep recursing through the remainder of the arguments, as it's
               -- possible that there are remaining invisible ones.
               -- See the "In type declarations" section of Note [VarBndrs,
               -- TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
+              |  otherwise
+              -> suppress_invis ts
 
 appArgsIfaceTypes :: IfaceAppArgs -> [IfaceType]
 appArgsIfaceTypes IA_Nil = []
-appArgsIfaceTypes (IA_Invis t ts) = t : appArgsIfaceTypes ts
-appArgsIfaceTypes (IA_Vis   t ts) = t : appArgsIfaceTypes ts
+appArgsIfaceTypes (IA_Arg t _ ts) = t : appArgsIfaceTypes ts
+
+appArgsIfaceTypesArgFlags :: IfaceAppArgs -> [(IfaceType, ArgFlag)]
+appArgsIfaceTypesArgFlags IA_Nil = []
+appArgsIfaceTypesArgFlags (IA_Arg t a ts)
+                                 = (t, a) : appArgsIfaceTypesArgFlags ts
 
 ifaceVisAppArgsLength :: IfaceAppArgs -> Int
 ifaceVisAppArgsLength = go 0
   where
-    go !n IA_Nil            = n
-    go n  (IA_Vis _ rest)   = go (n+1) rest
-    go n  (IA_Invis _ rest) = go n rest
+    go !n IA_Nil = n
+    go n  (IA_Arg _ argf rest)
+      | isVisibleArgFlag argf = go (n+1) rest
+      | otherwise             = go n rest
 
 {-
 Note [Suppressing invisible arguments]
@@ -609,6 +622,37 @@ By flattening the arguments like this, we obtain two benefits:
     is not a constant-time operation, so by flattening the arguments first, we
     decrease the number of times we have to call typeKind.
 
+Note [Pretty-printing invisible arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Suppressing invisible arguments] is all about how to avoid printing
+invisible arguments when the -fprint-explicit-kinds flag is disables. Well,
+what about when it's enabled? Then we can and should print invisible kind
+arguments, and this Note explains how we do it.
+
+As two running examples, consider the following code:
+
+  {-# LANGUAGE PolyKinds #-}
+  data T1 a
+  data T2 (a :: k)
+
+When displaying these types (with -fprint-explicit-kinds on), we could just
+do the following:
+
+  T1 k a
+  T2 k a
+
+That certainly gets the job done. But it lacks a crucial piece of information:
+is the `k` argument inferred or specified? To communicate this, we use visible
+kind application syntax to distinguish the two cases:
+
+  T1 @{k} a
+  T2 @k   a
+
+Here, @{k} indicates that `k` is an inferred argument, and @k indicates that
+`k` is a specified argument. (See
+Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep for
+a lengthier explanation on what "inferred" and "specified" mean.)
+
 ************************************************************************
 *                                                                      *
                 Pretty-printing
@@ -663,10 +707,19 @@ pprIfaceTvBndr use_parens (tv, ki)
                  | otherwise  = id
 
 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
-pprIfaceTyConBinders = sep . map (go . ifTyConBinderVar)
+pprIfaceTyConBinders = sep . map go
   where
-    go (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
-    go (IfaceTvBndr bndr) = pprIfaceTvBndr True bndr
+    go :: IfaceTyConBinder -> SDoc
+    go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr
+    go (Bndr (IfaceTvBndr bndr) vis) =
+      -- See Note [Pretty-printing invisible arguments]
+      case vis of
+        AnonTCB            -> ppr_bndr True
+        NamedTCB Required  -> ppr_bndr True
+        NamedTCB Specified -> char '@' <> ppr_bndr True
+        NamedTCB Inferred  -> char '@' <> braces (ppr_bndr False)
+      where
+        ppr_bndr use_parens = pprIfaceTvBndr use_parens bndr
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
@@ -735,9 +788,9 @@ ppr_ty ctxt_prec (IfaceAppTy t ts)
         sdocWithDynFlags $ \dflags ->
         pprIfacePrefixApp ctxt_prec
                           (ppr_ty funPrec t)
-                          (map (ppr_ty appPrec) (tys_wo_kinds dflags))
+                          (map (ppr_app_arg appPrec) (tys_wo_kinds dflags))
 
-    tys_wo_kinds dflags = appArgsIfaceTypes $ stripInvisArgs dflags ts
+    tys_wo_kinds dflags = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags ts
 
     -- Strip any casts from the head of the application
     ppr_app_ty_no_casts =
@@ -860,8 +913,8 @@ defaultRuntimeRepVars sty = go emptyFsEnv
 
     go_args :: FastStringEnv () -> IfaceAppArgs -> IfaceAppArgs
     go_args _ IA_Nil = IA_Nil
-    go_args subs (IA_Vis ty args)   = IA_Vis   (go subs ty) (go_args subs args)
-    go_args subs (IA_Invis ty args) = IA_Invis (go subs ty) (go_args subs args)
+    go_args subs (IA_Arg ty argf args)
+                     = IA_Arg (go subs ty) argf (go_args subs args)
 
     liftedRep :: IfaceTyCon
     liftedRep =
@@ -887,16 +940,24 @@ pprIfaceAppArgs  = ppr_app_args topPrec
 pprParendIfaceAppArgs = ppr_app_args appPrec
 
 ppr_app_args :: PprPrec -> IfaceAppArgs -> SDoc
-ppr_app_args ctx_prec args
- = let ppr_rest    = ppr_app_args ctx_prec
-       pprTys t ts = ppr_ty ctx_prec t <+> ppr_rest ts
-   in case args of
-        IA_Nil        -> empty
-        IA_Vis   t ts -> pprTys t ts
-        IA_Invis t ts -> sdocWithDynFlags $ \dflags ->
-                         if gopt Opt_PrintExplicitKinds dflags
-                            then pprTys t ts
-                            else ppr_rest ts
+ppr_app_args ctx_prec = go
+  where
+    go :: IfaceAppArgs -> SDoc
+    go IA_Nil             = empty
+    go (IA_Arg t argf ts) = ppr_app_arg ctx_prec (t, argf) <+> go ts
+
+-- See Note [Pretty-printing invisible arguments]
+ppr_app_arg :: PprPrec -> (IfaceType, ArgFlag) -> SDoc
+ppr_app_arg ctx_prec (t, argf) =
+  sdocWithDynFlags $ \dflags ->
+  let print_kinds = gopt Opt_PrintExplicitKinds dflags
+  in case argf of
+       Required  -> ppr_ty ctx_prec t
+       Specified |  print_kinds
+                 -> char '@' <> ppr_ty appPrec t
+       Inferred  |  print_kinds
+                 -> char '@' <> braces (ppr_ty topPrec t)
+       _         -> empty
 
 -------------------
 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
@@ -1074,7 +1135,8 @@ pprIfaceTyList ctxt_prec ty1 ty2
      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
     gather (IfaceTyConApp tc tys)
       | tc `ifaceTyConHasKey` consDataConKey
-      , (IA_Invis _ (IA_Vis ty1 (IA_Vis ty2 IA_Nil))) <- tys
+      , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
+      , isInvisibleArgFlag argf
       , (args, tl) <- gather ty2
       = (ty1:args, tl)
       | tc `ifaceTyConHasKey` nilDataConKey
@@ -1094,7 +1156,8 @@ pprTyTcApp' :: PprPrec -> IfaceTyCon -> IfaceAppArgs
             -> DynFlags -> PprStyle -> SDoc
 pprTyTcApp' ctxt_prec tc tys dflags style
   | ifaceTyConName tc `hasKey` ipClassKey
-  , IA_Vis (IfaceLitTy (IfaceStrTyLit n)) (IA_Vis ty IA_Nil) <- tys
+  , IA_Arg (IfaceLitTy (IfaceStrTyLit n))
+           Required (IA_Arg ty Required IA_Nil) <- tys
   = maybeParen ctxt_prec funPrec
     $ char '?' <> ftext n <> text "::" <> ppr_ty topPrec ty
 
@@ -1108,11 +1171,12 @@ pprTyTcApp' ctxt_prec tc tys dflags style
 
   | tc `ifaceTyConHasKey` consDataConKey
   , not (gopt Opt_PrintExplicitKinds dflags)
-  , IA_Invis _ (IA_Vis ty1 (IA_Vis ty2 IA_Nil)) <- tys
+  , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
+  , isInvisibleArgFlag argf
   = pprIfaceTyList ctxt_prec ty1 ty2
 
   | tc `ifaceTyConHasKey` tYPETyConKey
-  , IA_Vis (IfaceTyConApp rep IA_Nil) IA_Nil <- tys
+  , IA_Arg (IfaceTyConApp rep IA_Nil) Required IA_Nil <- tys
   , rep `ifaceTyConHasKey` liftedRepDataConKey
   = kindType
 
@@ -1126,10 +1190,10 @@ pprTyTcApp' ctxt_prec tc tys dflags style
          -> doc
 
        | otherwise
-         -> ppr_iface_tc_app ppr_ty ctxt_prec tc tys_wo_kinds
+         -> ppr_iface_tc_app ppr_app_arg ctxt_prec tc tys_wo_kinds
   where
     info = ifaceTyConInfo tc
-    tys_wo_kinds = appArgsIfaceTypes $ stripInvisArgs dflags tys
+    tys_wo_kinds = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags tys
 
 -- | Pretty-print a type-level equality.
 -- Returns (Just doc) if the argument is a /saturated/ application
@@ -1436,22 +1500,18 @@ instance Binary IfaceTyLit where
 instance Binary IfaceAppArgs where
   put_ bh tk =
     case tk of
-      IA_Vis   t ts -> putByte bh 0 >> put_ bh t >> put_ bh ts
-      IA_Invis t ts -> putByte bh 1 >> put_ bh t >> put_ bh ts
-      IA_Nil        -> putByte bh 2
+      IA_Arg t a ts -> putByte bh 0 >> put_ bh t >> put_ bh a >> put_ bh ts
+      IA_Nil        -> putByte bh 1
 
   get bh =
     do c <- getByte bh
        case c of
          0 -> do
            t  <- get bh
+           a  <- get bh
            ts <- get bh
-           return $! IA_Vis t ts
-         1 -> do
-           t  <- get bh
-           ts <- get bh
-           return $! IA_Invis t ts
-         2 -> return IA_Nil
+           return $! IA_Arg t a ts
+         1 -> return IA_Nil
          _ -> panic ("get IfaceAppArgs " ++ show c)
 
 -------------------
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index a3d11e8891..7c8a939965 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -305,14 +305,13 @@ toIfaceAppArgsX fr kind ty_args
       | Just ty' <- coreView ty
       = go env ty' ts
     go env (ForAllTy (Bndr tv vis) res) (t:ts)
-      | isVisibleArgFlag vis = IA_Vis   t' ts'
-      | otherwise            = IA_Invis t' ts'
+      = IA_Arg t' vis ts'
       where
         t'  = toIfaceTypeX fr t
         ts' = go (extendTCvSubst env tv t) res ts
 
     go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
-      = IA_Vis (toIfaceTypeX fr t) (go env res ts)
+      = IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
 
     go env ty ts@(t1:ts1)
       | not (isEmptyTCvSubst env)
@@ -326,7 +325,7 @@ toIfaceAppArgsX fr kind ty_args
         -- carry on as if it were FunTy.  Without the test for
         -- isEmptyTCvSubst we'd get an infinite loop (Trac #15473)
         WARN( True, ppr kind $$ ppr ty_args )
-        IA_Vis (toIfaceTypeX fr t1) (go env ty ts1)
+        IA_Arg (toIfaceTypeX fr t1) Required (go env ty ts1)
 
 tidyToIfaceType :: TidyEnv -> Type -> IfaceType
 tidyToIfaceType env ty = toIfaceType (tidyType env ty)
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 4944598aeb..100919eb16 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -894,8 +894,9 @@ conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
 unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
                        -> (SDoc, SrcSpan)
 unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
-  = errorBuilder (injectivityErrorHerald True $$ msg)
-                 [tyfamEqn]
+  = let (doc, loc) = errorBuilder (injectivityErrorHerald True $$ msg)
+                                  [tyfamEqn]
+    in (pprWithExplicitKindsWhen has_kinds doc, loc)
     where
       tvs = invis_vars `unionVarSet` vis_vars
       has_types = not $ isEmptyVarSet vis_vars
@@ -909,9 +910,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
                (True, False)  -> text "Type"
                (False, True)  -> text "Kind"
                (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
-      print_kinds_info = ppWhen has_kinds ppSuggestExplicitKinds
-      msg = doc $$ print_kinds_info $$
-            text "In the type family equation:"
+      msg = doc $$ text "In the type family equation:"
 
 -- | Build error message for equation that has a type family call at the top
 -- level of RHS
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index 768c78d28f..94525e8294 100644
--- a/compiler/typecheck/FunDeps.hs
+++ b/compiler/typecheck/FunDeps.hs
@@ -394,7 +394,9 @@ checkInstCoverage be_liberal clas theta inst_taus
 
          undet_set = fold undetermined_tvs
 
-         msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
+         msg = pprWithExplicitKindsWhen
+                 (isEmptyVarSet $ pSnd undetermined_tvs) $
+               vcat [ -- text "ls_tvs" <+> ppr ls_tvs
                       -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
                       -- , text "theta" <+> ppr theta
                       -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
@@ -414,8 +416,6 @@ checkInstCoverage be_liberal clas theta inst_taus
                             <+> pprQuotedList rs ]
                     , text "Un-determined variable" <> pluralVarSet undet_set <> colon
                             <+> pprVarSet undet_set (pprWithCommas ppr)
-                    , ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
-                      ppSuggestExplicitKinds
                     , ppWhen (not be_liberal &&
                               and (isEmptyVarSet <$> liberal_undet_tvs)) $
                       text "Using UndecidableInstances might help" ]
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index c692b7b905..5496f16ce1 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1762,9 +1762,8 @@ mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
 --        (b) warning about injectivity if both sides are the same
 --            type function application   F a ~ F b
 --            See Note [Non-injective type functions]
---        (c) warning about -fprint-explicit-kinds if that might be helpful
 mkEqInfoMsg ct ty1 ty2
-  = tyfun_msg $$ ambig_msg $$ invis_msg
+  = tyfun_msg $$ ambig_msg
   where
     mb_fun1 = isTyFun_maybe ty1
     mb_fun2 = isTyFun_maybe ty2
@@ -1773,19 +1772,6 @@ mkEqInfoMsg ct ty1 ty2
               = snd (mkAmbigMsg False ct)
               | otherwise = empty
 
-    -- better to check the exp/act types in the CtOrigin than the actual
-    -- mismatched types for suggestion about -fprint-explicit-kinds
-    (act_ty, exp_ty) = case ctOrigin ct of
-      TypeEqOrigin { uo_actual = act
-                   , uo_expected = exp } -> (act, exp)
-      _                                  -> (ty1, ty2)
-
-    invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
-              , not vis
-              = ppSuggestExplicitKinds
-              | otherwise
-              = empty
-
     tyfun_msg | Just tc1 <- mb_fun1
               , Just tc2 <- mb_fun2
               , tc1 == tc2
@@ -1940,6 +1926,7 @@ misMatchMsg ct oriented ty1 ty2
   | otherwise  -- So now we have Nothing or (Just IsSwapped)
                -- For some reason we treat Nothing like IsSwapped
   = addArising orig $
+    pprWithExplicitKindsWhenMismatch ty1 ty2 (ctOrigin ct) $
     sep [ text herald1 <+> quotes (ppr ty1)
         , nest padding $
           text herald2 <+> quotes (ppr ty2)
@@ -1974,13 +1961,37 @@ misMatchMsg ct oriented ty1 ty2
       = addArising orig $
         text "Couldn't match a lifted type with an unlifted type"
 
+-- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a
+-- type mismatch occurs to due invisible kind arguments.
+--
+-- This function first checks to see if the 'CtOrigin' argument is a
+-- 'TypeEqOrigin', and if so, uses the expected/actual types from that to
+-- check for a kind mismatch (as these types typically have more surrounding
+-- types and are likelier to be able to glean information about whether a
+-- mismatch occurred in an invisible argument position or not). If the
+-- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types
+-- themselves.
+pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
+                                 -> SDoc -> SDoc
+pprWithExplicitKindsWhenMismatch ty1 ty2 ct =
+  pprWithExplicitKindsWhen mismatch
+  where
+    (act_ty, exp_ty) = case ct of
+      TypeEqOrigin { uo_actual = act
+                   , uo_expected = exp } -> (act, exp)
+      _                                  -> (ty1, ty2)
+    mismatch | Just vis <- tcEqTypeVis act_ty exp_ty
+             = not vis
+             | otherwise
+             = False
+
 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
                     -> (Bool, Maybe SwapFlag, SDoc)
 -- NotSwapped means (actual, expected), IsSwapped is the reverse
 -- First return val is whether or not to print a herald above this msg
-mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
-                                          , uo_expected = exp
-                                          , uo_thing = maybe_thing })
+mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
+                                             , uo_expected = exp
+                                             , uo_thing = maybe_thing })
                     m_level printExpanded
   | KindLevel <- level, occurs_check_error       = (True, Nothing, empty)
   | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
@@ -2014,7 +2025,8 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
         -> msg5 th
 
       _ | not (act `pickyEqType` exp)
-        -> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
+        -> pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
+           vcat [ text "Expected" <+> sort <> colon <+> ppr exp
                 , text "  Actual" <+> sort <> colon <+> ppr act
                 , if printExpanded then expandedTys else empty ]
 
@@ -2036,7 +2048,8 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
                        maybe_thing
                , quotes (pprWithTYPE act) ]
 
-    msg5 th = hang (text "Expected" <+> kind_desc <> comma)
+    msg5 th = pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
+              hang (text "Expected" <+> kind_desc <> comma)
                  2 (text "but" <+> quotes th <+> text "has kind" <+>
                     quotes (ppr act))
       where
@@ -2819,15 +2832,26 @@ Re-flattening is pretty easy, because we don't need to keep track of
 evidence.  We don't re-use the code in TcCanonical because that's in
 the TcS monad, and we are in TcM here.
 
-Note [Suggest -fprint-explicit-kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Kind arguments in error messages]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It can be terribly confusing to get an error message like (Trac #9171)
+
     Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
                 with actual type ‘GetParam Base (GetParam Base Int)’
+
 The reason may be that the kinds don't match up.  Typically you'll get
 more useful information, but not when it's as a result of ambiguity.
-This test suggests -fprint-explicit-kinds when all the ambiguous type
-variables are kind variables.
+
+To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
+whenever any error message arises due to a kind mismatch. This means that
+the above error message would instead be displayed as:
+
+    Couldn't match expected type
+                  ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
+                with actual type
+                  ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
+
+Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
 -}
 
 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
@@ -2847,10 +2871,8 @@ mkAmbigMsg prepend_msg ct
         | not (null ambig_tvs)
         = pp_ambig (text "type") ambig_tvs
 
-        | otherwise  -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
-                     -- See Note [Suggest -fprint-explicit-kinds]
-        = vcat [ pp_ambig (text "kind") ambig_kvs
-               , ppSuggestExplicitKinds ]
+        | otherwise
+        = pp_ambig (text "kind") ambig_kvs
 
     pp_ambig what tkvs
       | prepend_msg -- "Ambiguous type variable 't0'"
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 2ddb4c4604..d454f4cd32 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -100,7 +100,7 @@ module TcType (
   isImprovementPred,
 
   -- * Finding type instances
-  tcTyFamInsts, isTyFamFree,
+  tcTyFamInsts, tcTyFamInstsAndVis, tcTyConAppTyFamInstsAndVis, isTyFamFree,
 
   -- * Finding "exact" (non-dead) type variables
   exactTyCoVarsOfType, exactTyCoVarsOfTypes,
@@ -858,20 +858,85 @@ promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
 -- we don't need to take <big type> into account when asking if
 -- the calls on the RHS are smaller than the LHS
 tcTyFamInsts :: Type -> [(TyCon, [Type])]
-tcTyFamInsts ty
-  | Just exp_ty <- tcView ty    = tcTyFamInsts exp_ty
-tcTyFamInsts (TyVarTy _)        = []
-tcTyFamInsts (TyConApp tc tys)
-  | isTypeFamilyTyCon tc        = [(tc, take (tyConArity tc) tys)]
-  | otherwise                   = concat (map tcTyFamInsts tys)
-tcTyFamInsts (LitTy {})         = []
-tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderType bndr)
-                                  ++ tcTyFamInsts ty
-tcTyFamInsts (FunTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
-tcTyFamInsts (AppTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
-tcTyFamInsts (CastTy ty _)      = tcTyFamInsts ty
-tcTyFamInsts (CoercionTy _)     = []  -- don't count tyfams in coercions,
-                                      -- as they never get normalized, anyway
+tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis
+
+-- | Like 'tcTyFamInsts', except that the output records whether the
+-- type family and its arguments occur as an /invisible/ argument in
+-- some type application. This information is useful because it helps GHC know
+-- when to turn on @-fprint-explicit-kinds@ during error reporting so that
+-- users can actually see the type family being mentioned.
+--
+-- As an example, consider:
+--
+-- @
+-- class C a
+-- data T (a :: k)
+-- type family F a :: k
+-- instance C (T @(F Int) (F Bool))
+-- @
+--
+-- There are two occurrences of the type family `F` in that `C` instance, so
+-- @'tcTyFamInstsAndVis' (C (T \@(F Int) (F Bool)))@ will return:
+--
+-- @
+-- [ ('True',  F, [Int])
+-- , ('False', F, [Bool]) ]
+-- @
+--
+-- @F Int@ is paired with 'True' since it appears as an /invisible/ argument
+-- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a
+-- /visible/ argument to @C@.
+--
+-- See also @Note [Kind arguments in error messages]@ in "TcErrors".
+tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])]
+tcTyFamInstsAndVis = tcTyFamInstsAndVisX False
+
+tcTyFamInstsAndVisX
+  :: Bool -- ^ Is this an invisible argument to some type application?
+  -> Type -> [(Bool, TyCon, [Type])]
+tcTyFamInstsAndVisX = go
+  where
+    go is_invis_arg ty
+      | Just exp_ty <- tcView ty       = go is_invis_arg exp_ty
+    go _ (TyVarTy _)                   = []
+    go is_invis_arg (TyConApp tc tys)
+      | isTypeFamilyTyCon tc
+      = [(is_invis_arg, tc, take (tyConArity tc) tys)]
+      | otherwise
+      = tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys
+    go _            (LitTy {})         = []
+    go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr)
+                                         ++ go is_invis_arg ty
+    go is_invis_arg (FunTy ty1 ty2)    = go is_invis_arg ty1
+                                         ++ go is_invis_arg ty2
+    go is_invis_arg ty@(AppTy _ _)     =
+      let (ty_head, ty_args) = splitAppTys ty
+          ty_arg_flags       = appTyArgFlags ty_head ty_args
+      in go is_invis_arg ty_head
+         ++ concat (zipWith (\flag -> go (isInvisibleArgFlag flag))
+                            ty_arg_flags ty_args)
+    go is_invis_arg (CastTy ty _)      = go is_invis_arg ty
+    go _            (CoercionTy _)     = [] -- don't count tyfams in coercions,
+                                            -- as they never get normalized,
+                                            -- anyway
+
+-- | In an application of a 'TyCon' to some arguments, find the outermost
+-- occurrences of type family applications within the arguments. This function
+-- will not consider the 'TyCon' itself when checking for type family
+-- applications.
+--
+-- See 'tcTyFamInstsAndVis' for more details on how this works (as this
+-- function is called inside of 'tcTyFamInstsAndVis').
+tcTyConAppTyFamInstsAndVis :: TyCon -> [Type] -> [(Bool, TyCon, [Type])]
+tcTyConAppTyFamInstsAndVis = tcTyConAppTyFamInstsAndVisX False
+
+tcTyConAppTyFamInstsAndVisX
+  :: Bool -- ^ Is this an invisible argument to some type application?
+  -> TyCon -> [Type] -> [(Bool, TyCon, [Type])]
+tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys =
+  let (invis_tys, vis_tys) = partitionInvisibleTypes tc tys
+  in concat $ map (tcTyFamInstsAndVisX True)         invis_tys
+           ++ map (tcTyFamInstsAndVisX is_invis_arg) vis_tys
 
 isTyFamFree :: Type -> Bool
 -- ^ Check that a type does not contain any type family applications.
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index f9aad513b7..1c0ce678e5 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1788,7 +1788,7 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
 
        -- And now kind args
        ; checkTcM (all check_arg kind_shapes)
-                  (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
+                  (tidy_env2, pprWithExplicitKindsWhen True pp_wrong_at_arg)
 
        ; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
                                                 , ppr arg_shapes
@@ -2001,41 +2001,27 @@ checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pat
 -- | Checks for occurrences of type families in class instances and type/data
 -- family instances.
 checkValidTypePats :: TyCon -> [Type] -> TcM ()
-checkValidTypePats tc pat_ty_args =
-  traverse_ (check_valid_type_pat False) invis_ty_args *>
-  traverse_ (check_valid_type_pat True)  vis_ty_args
+checkValidTypePats tc pat_ty_args = do
+  -- Check that each of pat_ty_args is a monotype.
+  -- One could imagine generalising to allow
+  --      instance C (forall a. a->a)
+  -- but we don't know what all the consequences might be.
+  traverse_ checkValidMonoType pat_ty_args
+
+  -- Ensure that no type family instances occur a type pattern
+  case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
+    [] -> pure ()
+    ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
+      ty_fam_inst_illegal_err tf_is_invis_arg (mkTyConApp tf_tc tf_args)
   where
-    (invis_ty_args, vis_ty_args) = partitionInvisibleTypes tc pat_ty_args
     inst_ty = mkTyConApp tc pat_ty_args
 
-    check_valid_type_pat
-      :: Bool -- True if this is an /visible/ argument to the TyCon.
-      -> Type -> TcM ()
-    -- Used for type patterns in class instances,
-    -- and in type/data family instances
-    check_valid_type_pat vis_arg pat_ty
-      = do { -- Check that pat_ty is a monotype
-             checkValidMonoType pat_ty
-                 -- One could imagine generalising to allow
-                 --      instance C (forall a. a->a)
-                 -- but we don't know what all the consequences might be
-
-              -- Ensure that no type family instances occur a type pattern
-           ; case tcTyFamInsts pat_ty of
-               [] -> pure ()
-               ((tf_tc, tf_args):_) ->
-                 failWithTc $
-                 ty_fam_inst_illegal_err vis_arg (mkTyConApp tf_tc tf_args) }
-
     ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
-    ty_fam_inst_illegal_err vis_arg ty
-      = sdocWithDynFlags $ \dflags ->
+    ty_fam_inst_illegal_err invis_arg ty
+      = pprWithExplicitKindsWhen invis_arg $
         hang (text "Illegal type synonym family application"
-                <+> quotes (ppr ty) <+> text "in instance" <>
-             colon) 2 $
-          vcat [ ppr inst_ty
-               , ppUnless (vis_arg || gopt Opt_PrintExplicitKinds dflags) $
-                 text "Use -fprint-explicit-kinds to see the kind arguments" ]
+                <+> quotes (ppr ty) <+> text "in instance" <> colon)
+           2 (ppr inst_ty)
 
 -- Error messages
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 5f70206a1a..37457e9f22 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -69,7 +69,7 @@ module TyCoRep (
         pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprTyLit,
         PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
-        pprDataCons, ppSuggestExplicitKinds,
+        pprDataCons, pprWithExplicitKindsWhen,
 
         pprCo, pprParendCo,
 
@@ -3356,13 +3356,14 @@ pprTypeApp tc tys
     -- TODO: toIfaceTcArgs seems rather wasteful here
 
 ------------------
-ppSuggestExplicitKinds :: SDoc
--- Print a helpful suggstion about -fprint-explicit-kinds,
--- if it is not already on
-ppSuggestExplicitKinds
-  = sdocWithDynFlags $ \ dflags ->
-    ppUnless (gopt Opt_PrintExplicitKinds dflags) $
-    text "Use -fprint-explicit-kinds to see the kind arguments"
+-- | Display all kind information (with @-fprint-explicit-kinds@) when the
+-- provided 'Bool' argument is 'True'.
+-- See @Note [Kind arguments in error messages]@ in "TcErrors".
+pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
+pprWithExplicitKindsWhen b
+  = updSDocDynFlags $ \dflags ->
+      if b then gopt_set dflags Opt_PrintExplicitKinds
+           else dflags
 
 {-
 %************************************************************************
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 6df6d944ed..26461ee43a 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -204,7 +204,7 @@ module Type (
         pprType, pprParendType, pprPrecType,
         pprTypeApp, pprTyThingCategory, pprShortTyThing,
         pprTCvBndr, pprTCvBndrs, pprForAll, pprUserForAll,
-        pprSigmaType, ppSuggestExplicitKinds,
+        pprSigmaType, pprWithExplicitKindsWhen,
         pprTheta, pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprSourceTyCon,
         PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
@@ -1617,6 +1617,8 @@ appTyArgFlags ty = fun_kind_arg_flags (typeKind ty)
 fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag]
 fun_kind_arg_flags = go emptyTCvSubst
   where
+    go subst ki arg_tys
+      | Just ki' <- coreView ki = go subst ki' arg_tys
     go _ _ [] = []
     go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys)
       = argf : go subst' res_ki arg_tys