Be pickier about unsaturated synonyms in :kind

Summary:
We currently permit any and all uses of unsaturated type
synonyms and type families in GHCi's `:kind` command, which allows
strange interactions like this one:

```
> :set -XTypeFamilies -XPolyKinds
> type family Id (a :: k)
> type instance Id a = a
> type Foo x = Maybe
> :kind! Id Foo
```

This is probably a stretch too far, so this patch moves to disallow
unsaturated synonyms that aren't at the top level (we still want to
allow `:kind Id`, for instance). We do this by augmenting `GhciCtxt`
with an additional `Bool` field to indicate if we are at the
outermost level of the type being passed to `:kind` or not. See
`Note [Unsaturated type synonyms in GHCi]` in `TcValidity` for the
full story.

Test Plan: make test TEST=T16013

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: simonpj, goldfire, rwbarton, carter

GHC Trac Issues: #16013

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

7 files changed, 71 insertions, 11 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 7f4e379fef..006a97bd55 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1852,7 +1852,7 @@ expectedKindInCtxt :: UserTypeCtxt -> ContextKind
 -- splice), or only certain kinds (like in type signatures).
 expectedKindInCtxt (TySynCtxt _)   = AnyKind
 expectedKindInCtxt ThBrackCtxt     = AnyKind
-expectedKindInCtxt GhciCtxt        = AnyKind
+expectedKindInCtxt (GhciCtxt {})   = AnyKind
 -- The types in a 'default' decl can have varying kinds
 -- See Note [Extended defaults]" in TcEnv
 expectedKindInCtxt DefaultDeclCtxt     = AnyKind
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 54948e00e2..fae0c19394 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2415,7 +2415,7 @@ tcRnType hsc_env normalise rdr_type
        ; ty  <- zonkTcTypeToType ty
 
        -- Do validity checking on type
-       ; checkValidType GhciCtxt ty
+       ; checkValidType (GhciCtxt True) ty
 
        ; ty' <- if normalise
                 then do { fam_envs <- tcGetFamInstEnvs
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 90d4408126..b2c9b3291f 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -606,7 +606,11 @@ data UserTypeCtxt
   | GenSigCtxt          -- Higher-rank or impredicative situations
                         -- e.g. (f e) where f has a higher-rank type
                         -- We might want to elaborate this
-  | GhciCtxt            -- GHCi command :kind <type>
+  | GhciCtxt Bool       -- GHCi command :kind <type>
+                        -- The Bool indicates if we are checking the outermost
+                        -- type application.
+                        -- See Note [Unsaturated type synonyms in GHCi] in
+                        -- TcValidity.
 
   | ClassSCCtxt Name    -- Superclasses of a class
   | SigmaCtxt           -- Theta part of a normal for-all type
@@ -650,7 +654,7 @@ pprUserTypeCtxt (InstDeclCtxt False) = text "an instance declaration"
 pprUserTypeCtxt (InstDeclCtxt True)  = text "a stand-alone deriving instance declaration"
 pprUserTypeCtxt SpecInstCtxt      = text "a SPECIALISE instance pragma"
 pprUserTypeCtxt GenSigCtxt        = text "a type expected by the context"
-pprUserTypeCtxt GhciCtxt          = text "a type in a GHCi command"
+pprUserTypeCtxt (GhciCtxt {})     = text "a type in a GHCi command"
 pprUserTypeCtxt (ClassSCCtxt c)   = text "the super-classes of class" <+> quotes (ppr c)
 pprUserTypeCtxt SigmaCtxt         = text "the context of a polymorphic type"
 pprUserTypeCtxt (DataTyCtxt tc)   = text "the context of the data type declaration for" <+> quotes (ppr tc)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 867e202218..64f5bc779c 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -228,7 +228,7 @@ checkAmbiguity ctxt ty
 wantAmbiguityCheck :: UserTypeCtxt -> Bool
 wantAmbiguityCheck ctxt
   = case ctxt of  -- See Note [When we don't check for ambiguity]
-      GhciCtxt     -> False
+      GhciCtxt {}  -> False
       TySynCtxt {} -> False
       TypeAppCtxt  -> False
       _            -> True
@@ -357,7 +357,7 @@ checkValidType ctxt ty
                  ForSigCtxt _   -> rank1
                  SpecInstCtxt   -> rank1
                  ThBrackCtxt    -> rank1
-                 GhciCtxt       -> ArbitraryRank
+                 GhciCtxt {}    -> ArbitraryRank
 
                  TyVarBndrKindCtxt _ -> rank0
                  DataKindCtxt _      -> rank1
@@ -547,16 +547,63 @@ check_syn_tc_app env ctxt rank ty tc tys
                          in addErrCtxt err_ctxt $ check_type env ctxt rank ty'
              Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
 
-  | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in
-                      -- GHCi :kind commands; see Trac #7586
+  | GhciCtxt True <- ctxt  -- Accept outermost under-saturated type synonym or
+                           -- type family constructors in GHCi :kind commands.
+                           -- See Note [Unsaturated type synonyms in GHCi]
   = mapM_ check_arg tys
 
   | otherwise
   = failWithTc (tyConArityErr tc tys)
   where
     tc_arity  = tyConArity tc
-    check_arg | isTypeFamilyTyCon tc = check_arg_type  env ctxt rank
-              | otherwise            = check_type      env ctxt synArgMonoType
+    check_arg
+      | isTypeFamilyTyCon tc = check_arg_type  env arg_ctxt rank
+      | otherwise            = check_type      env arg_ctxt synArgMonoType
+    arg_ctxt
+      | GhciCtxt _ <- ctxt = GhciCtxt False
+          -- When checking an argument, set the field of GhciCtxt to False to
+          -- indicate that we are no longer in an outermost position (and thus
+          -- unsaturated synonyms are no longer allowed).
+          -- See Note [Unsaturated type synonyms in GHCi]
+      | otherwise          = ctxt
+
+{-
+Note [Unsaturated type synonyms in GHCi]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking, GHC disallows unsaturated uses of type synonyms or type
+families. For instance, if one defines `type Const a b = a`, then GHC will not
+permit using `Const` unless it is applied to (at least) two arguments. There is
+an exception to this rule, however: GHCi's :kind command. For instance, it
+is quite common to look up the kind of a type constructor like so:
+
+  λ> :kind Const
+  Const :: j -> k -> j
+  λ> :kind Const Int
+  Const Int :: k -> Type
+
+Strictly speaking, the two uses of `Const` above are unsaturated, but this
+is an extremely benign (and useful) example of unsaturation, so we allow it
+here as a special case.
+
+That being said, we do not allow unsaturation carte blanche in GHCi. Otherwise,
+this GHCi interaction would be possible:
+
+  λ> newtype Fix f = MkFix (f (Fix f))
+  λ> type Id a = a
+  λ> :kind Fix Id
+  Fix Id :: Type
+
+This is rather dodgy, so we move to disallow this. We only permit unsaturated
+synonyms in GHCi if they are *top-level*—that is, if the synonym is the
+outermost type being applied. This allows `Const` and `Const Int` in the
+first example, but not `Fix Id` in the second example, as `Id` is not the
+outermost type being applied (`Fix` is).
+
+We track this outermost property in the GhciCtxt constructor of UserTypeCtxt.
+A field of True in GhciCtxt indicates that we're in an outermost position. Any
+time we invoke `check_arg` to check the validity of an argument, we switch the
+field to False.
+-}
 
 ----------------------------------------
 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
@@ -1007,7 +1054,7 @@ okIPCtxt GenSigCtxt             = True
 okIPCtxt (ConArgCtxt {})        = True
 okIPCtxt (ForSigCtxt {})        = True  -- ??
 okIPCtxt ThBrackCtxt            = True
-okIPCtxt GhciCtxt               = True
+okIPCtxt (GhciCtxt {})          = True
 okIPCtxt SigmaCtxt              = True
 okIPCtxt (DataTyCtxt {})        = True
 okIPCtxt (PatSynCtxt {})        = True
diff --git a/testsuite/tests/ghci/should_fail/T16013.script b/testsuite/tests/ghci/should_fail/T16013.script
new file mode 100644
index 0000000000..287de60656
--- /dev/null
+++ b/testsuite/tests/ghci/should_fail/T16013.script
@@ -0,0 +1,5 @@
+:set -XTypeFamilies -XPolyKinds
+type family Id (a :: k)
+type instance Id a = a
+type Foo x = Maybe
+:kind! Id Foo
diff --git a/testsuite/tests/ghci/should_fail/T16013.stderr b/testsuite/tests/ghci/should_fail/T16013.stderr
new file mode 100644
index 0000000000..ec60359829
--- /dev/null
+++ b/testsuite/tests/ghci/should_fail/T16013.stderr
@@ -0,0 +1,3 @@
+
+<interactive>:1:1: error:
+    The type synonym ‘Foo’ should have 1 argument, but has been given none
diff --git a/testsuite/tests/ghci/should_fail/all.T b/testsuite/tests/ghci/should_fail/all.T
index 01e5c36579..5e0a18c5b8 100644
--- a/testsuite/tests/ghci/should_fail/all.T
+++ b/testsuite/tests/ghci/should_fail/all.T
@@ -2,3 +2,4 @@ test('T10549', [], ghci_script, ['T10549.script'])
 test('T10549a', [], ghci_script, ['T10549a.script'])
 test('T14608', [], ghci_script, ['T14608.script'])
 test('T15055', normalise_version('ghc'), ghci_script, ['T15055.script'])
+test('T16013', [], ghci_script, ['T16013.script'])