Fix #14238 by always pretty-printing visible tyvars

Summary:
Before, GHC would never print visible tyvars in the absence
of `-fprint-explicit-foralls`, which led to `:kind` displaying
incorrect kinds in GHCi. The fix is simple—simply check beforehand
if any of the type variable binders are required when deciding when
to pretty-print them.

Test Plan: make test TEST=T14238

Reviewers: simonpj, goldfire, bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14238

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

5 files changed, 43 insertions, 2 deletions

diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 4523093ef6..f6493f0a24 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -860,11 +860,46 @@ pprIfaceSigmaType show_forall ty
 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprUserIfaceForAll tvs
    = sdocWithDynFlags $ \dflags ->
-     ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
+     -- See Note [When to print foralls]
+     ppWhen (any tv_has_kind_var tvs
+             || any tv_is_required tvs
+             || gopt Opt_PrintExplicitForalls dflags) $
      pprIfaceForAll tvs
    where
      tv_has_kind_var (TvBndr (_,kind) _) = not (ifTypeIsVarFree kind)
+     tv_is_required = isVisibleArgFlag . binderArgFlag
 
+{-
+Note [When to print foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We opt to explicitly pretty-print `forall`s if any of the following
+criteria are met:
+
+1. -fprint-explicit-foralls is on.
+
+2. A bound type variable has a polymorphic kind. E.g.,
+
+     forall k (a::k). Proxy a -> Proxy a
+
+   Since a's kind mentions a variable k, we print the foralls.
+
+3. A bound type variable is a visible argument (#14238).
+   Suppose we are printing the kind of:
+
+     T :: forall k -> k -> Type
+
+   The "forall k ->" notation means that this kind argument is required.
+   That is, it must be supplied at uses of T. E.g.,
+
+     f :: T (Type->Type)  Monad -> Int
+
+   So we print an explicit "T :: forall k -> k -> Type",
+   because omitting it and printing "T :: k -> Type" would be
+   utterly misleading.
+
+   See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]
+   in TyCoRep.
+-}
 
 -------------------
 
diff --git a/testsuite/tests/dependent/ghci/T14238.script b/testsuite/tests/dependent/ghci/T14238.script
new file mode 100644
index 0000000000..7c27123e00
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.script
@@ -0,0 +1,4 @@
+:set -XTypeInType
+:m + Data.Kind
+data Foo (k :: Type) :: k -> Type
+:kind Foo
diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout
new file mode 100644
index 0000000000..fddbc0de54
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.stdout
@@ -0,0 +1 @@
+Foo :: forall k -> k -> *
diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T
index 956272fa55..bd819c28bc 100644
--- a/testsuite/tests/dependent/ghci/all.T
+++ b/testsuite/tests/dependent/ghci/all.T
@@ -2,3 +2,4 @@ test('T11549',
      [ expect_broken( 11787 ),
        expect_broken( 11786 ) ],
      ghci_script, ['T11549.script'])
+test('T14238', normal, ghci_script, ['T14238.script'])
diff --git a/testsuite/tests/ghci/scripts/T11252.stdout b/testsuite/tests/ghci/scripts/T11252.stdout
index f6d45ddf32..eddba4530e 100644
--- a/testsuite/tests/ghci/scripts/T11252.stdout
+++ b/testsuite/tests/ghci/scripts/T11252.stdout
@@ -1 +1 @@
-Proxy1 :: k -> *
+Proxy1 :: forall k -> k -> *