Fix #13963.

This commit fixes several things:

1. RuntimeRep arg suppression was overeager for *visibly*-quantified
RuntimeReps, which should remain.

2. The choice of whether to used a Named TyConBinder or an anonymous
was sometimes wrong. Now, we do an extra little pass right before
constructing the tycon to fix these.

3. TyCons that normally cannot appear unsaturated can appear unsaturated
in :kind. But this fact was not propagated into the type checker.
It now is.

6 files changed, 73 insertions, 10 deletions

diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index dcd3ad3f9d..3475366e31 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -681,11 +681,13 @@ defaultRuntimeRepVars = go emptyFsEnv
     go :: FastStringEnv () -> IfaceType -> IfaceType
     go subs (IfaceForAllTy bndr ty)
       | isRuntimeRep var_kind
+      , isInvisibleArgFlag (binderArgFlag bndr) -- don't default *visible* quantification
+                                                -- or we get the mess in #13963
       = let subs' = extendFsEnv subs var ()
         in go subs' ty
       | otherwise
       = IfaceForAllTy (TvBndr (var, go subs var_kind) (binderArgFlag bndr))
-        (go subs ty)
+                      (go subs ty)
       where
         var :: IfLclName
         (var, var_kind) = binderVar bndr
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index fdde6f1ca2..4fd561e65c 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -30,7 +30,7 @@ module TcHsType (
         kcHsTyVarBndrs,
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
-        tcLHsType, tcCheckLHsType,
+        tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
         tcHsContext, tcLHsPredType, tcInferApps,
         solveEqualities, -- useful re-export
 
@@ -88,7 +88,7 @@ import PrelNames hiding ( wildCardName )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Maybes
-import Data.List ( partition, zipWith4 )
+import Data.List ( partition, zipWith4, mapAccumR )
 import Control.Monad
 
 {-
@@ -333,6 +333,13 @@ tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
 -- Called from outside: set the context
 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
 
+-- Like tcLHsType, but use it in a context where type synonyms and type families
+-- do not need to be saturated, like in a GHCi :kind call
+tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
+tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
+  where
+    mode = allowUnsaturated typeLevelMode
+
 ---------------------------
 -- | Should we generalise the kind of this type signature?
 -- We *should* generalise if the type is closed
@@ -392,15 +399,21 @@ concern things that the renamer can't handle.
 -- differentiates only between types and kinds, but this will likely
 -- grow, at least to include the distinction between patterns and
 -- not-patterns.
-newtype TcTyMode
-  = TcTyMode { mode_level :: TypeOrKind  -- True <=> type, False <=> kind
+data TcTyMode
+  = TcTyMode { mode_level :: TypeOrKind
+             , mode_unsat :: Bool        -- True <=> allow unsaturated type families
              }
+ -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
+ -- in GHCi :kind calls
 
 typeLevelMode :: TcTyMode
-typeLevelMode = TcTyMode { mode_level = TypeLevel }
+typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_unsat = False }
 
 kindLevelMode :: TcTyMode
-kindLevelMode = TcTyMode { mode_level = KindLevel }
+kindLevelMode = TcTyMode { mode_level = KindLevel, mode_unsat = False }
+
+allowUnsaturated :: TcTyMode -> TcTyMode
+allowUnsaturated mode = mode { mode_unsat = True }
 
 -- switch to kind level
 kindLevel :: TcTyMode -> TcTyMode
@@ -1041,7 +1054,8 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                   -> TcTyCon   -- a non-loopy version of the tycon
                   -> TcM (TcType, TcKind)
     handle_tyfams tc tc_tc
-      | mightBeUnsaturatedTyCon tc_tc
+      | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
+                                         -- This is where mode_unsat is used
       = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
            ; return (ty, tc_kind) }
 
@@ -1835,8 +1849,8 @@ tcTyClTyVars tycon_name thing_inside
 
        ; let scoped_tvs = tcTyConScopedTyVars tycon
                -- these are all zonked:
-             binders    = tyConBinders tycon
              res_kind   = tyConResKind tycon
+             binders    = correct_binders (tyConBinders tycon) res_kind
 
           -- See Note [Free-floating kind vars]
        ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
@@ -1849,6 +1863,39 @@ tcTyClTyVars tycon_name thing_inside
        ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
        ; tcExtendTyVarEnv scoped_tvs $
          thing_inside binders res_kind }
+  where
+    -- Given some TyConBinders and a TyCon's result kind, make sure that the
+    -- correct any wrong Named/Anon choices. For example, consider
+    --   type Syn k = forall (a :: k). Proxy a
+    -- At first, it looks like k should be named -- after all, it appears on the RHS.
+    -- However, the correct kind for Syn is (* -> *).
+    -- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
+    -- kind *.) See also #13963.
+    correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
+    correct_binders binders kind
+      = binders'
+      where
+        (_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
+
+        go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
+        go fvs binder
+          | isNamedTyConBinder binder
+          , not (tv `elemVarSet` fvs)
+          = (new_fvs, mkAnonTyConBinder tv)
+
+          | not (isNamedTyConBinder binder)
+          , tv `elemVarSet` fvs
+          = (new_fvs, mkNamedTyConBinder Required tv)
+             -- always Required, because it was anonymous (i.e. visible) previously
+
+          | otherwise
+          = (new_fvs, binder)
+
+          where
+            tv      = binderVar binder
+            new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
+
+
 
 -----------------------------------
 tcDataKindSig :: Bool  -- ^ Do we require the result to be *?
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index e53a661d17..a0bd2a837c 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2255,7 +2255,7 @@ tcRnType hsc_env normalise rdr_type
        ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
        ; (ty, kind) <- solveEqualities $
                        tcWildCardBinders wcs  $ \ _ ->
-                       tcLHsType rn_type
+                       tcLHsTypeUnsaturated rn_type
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
        ; kvs <- kindGeneralize kind
diff --git a/testsuite/tests/ghci/scripts/T13963.script b/testsuite/tests/ghci/scripts/T13963.script
new file mode 100644
index 0000000000..630e5cd70c
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T13963.script
@@ -0,0 +1,9 @@
+:set -XTypeInType -XRankNTypes
+import GHC.Exts (TYPE, RuntimeRep(LiftedRep))
+type Pair (a :: TYPE rep) (b :: TYPE rep') rep'' = forall (r :: TYPE rep''). (a -> b -> r)
+:kind Pair
+:kind Pair Int
+:kind Pair Int Float
+:kind Pair Int Float LiftedRep
+
+
diff --git a/testsuite/tests/ghci/scripts/T13963.stdout b/testsuite/tests/ghci/scripts/T13963.stdout
new file mode 100644
index 0000000000..9e31d8bebc
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T13963.stdout
@@ -0,0 +1,4 @@
+Pair :: TYPE rep -> TYPE rep' -> RuntimeRep -> *
+Pair Int :: * -> RuntimeRep -> *
+Pair Int Float :: RuntimeRep -> *
+Pair Int Float LiftedRep :: *
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index fd3744e190..6d1d0f1172 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -258,3 +258,4 @@ test('T13591', expect_broken(13591), ghci_script, ['T13591.script'])
 test('T13699', normal, ghci_script, ['T13699.script'])
 test('T13988', normal, ghci_script, ['T13988.script'])
 test('T13407', normal, ghci_script, ['T13407.script'])
+test('T13963', normal, ghci_script, ['T13963.script'])