Fix #16287 by checking for more unsaturated synonym arguments

Trac #16287 shows that we were checking for unsaturated type synonym
arguments (in `:kind`) when the argument was to a type synonym, but
_not_ when the argument was to some other form of type constructor,
such as a data type. The solution is to use the machinery that
rejects unsaturated type synonym arguments (previously confined to
`check_syn_tc_app`) to `check_arg_type`, which checks these other
forms of arguments. While I was in town, I cleaned up
`check_syn_tc_app` a bit to only invoke `check_arg_type` so as to
minimize the number of different code paths that that function could
go down.

4 files changed, 46 insertions, 24 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index ca58877bcb..218f539c68 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -599,13 +599,13 @@ check_type _ (TyVarTy _) = return ()
 
 check_type ve (AppTy ty1 ty2)
   = do  { check_type ve ty1
-        ; check_arg_type ve ty2 }
+        ; check_arg_type False ve ty2 }
 
 check_type ve ty@(TyConApp tc tys)
   | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
   = check_syn_tc_app ve ty tc tys
   | isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys
-  | otherwise              = mapM_ (check_arg_type ve) tys
+  | otherwise              = mapM_ (check_arg_type False ve) tys
 
 check_type _ (LitTy {}) = return ()
 
@@ -693,14 +693,8 @@ check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
     tc_arity  = tyConArity tc
 
     check_arg :: ExpandMode -> KindOrType -> TcM ()
-    check_arg expand
-      | isTypeFamilyTyCon tc
-      = check_arg_type ve'
-      | otherwise
-      = check_type (ve'{ve_rank = synArgMonoType})
-      where
-        ve' :: ValidityEnv
-        ve' = ve{ve_ctxt = arg_ctxt, ve_expand = expand}
+    check_arg expand =
+      check_arg_type (isTypeSynonymTyCon tc) (ve{ve_expand = expand})
 
     check_args_only, check_expansion_only :: ExpandMode -> TcM ()
     check_args_only expand = mapM_ (check_arg expand) tys
@@ -713,15 +707,6 @@ check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
                         check_type (ve{ve_expand = expand}) ty'
          Nothing  -> pprPanic "check_syn_tc_app" (ppr ty)
 
-    arg_ctxt :: UserTypeCtxt
-    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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -774,7 +759,9 @@ check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys
         ; mapM_ (check_type (ve{ve_rank = rank'})) tys }
 
 ----------------------------------------
-check_arg_type :: ValidityEnv -> KindOrType -> TcM ()
+check_arg_type
+  :: Bool -- ^ Is this the argument to a type synonym?
+  -> ValidityEnv -> KindOrType -> TcM ()
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
@@ -793,11 +780,14 @@ check_arg_type :: ValidityEnv -> KindOrType -> TcM ()
 --     But not in user code.
 -- Anyway, they are dealt with by a special case in check_tau_type
 
-check_arg_type _ (CoercionTy {}) = return ()
+check_arg_type _ _ (CoercionTy {}) = return ()
 
-check_arg_type (ve@ValidityEnv{ve_rank = rank}) ty
+check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
   = do  { impred <- xoptM LangExt.ImpredicativeTypes
         ; let rank' = case rank of          -- Predictive => must be monotype
+                        -- Rank-n arguments to type synonyms are OK, provided
+                        -- that LiberalTypeSynonyms is enabled.
+                        _ | type_syn       -> synArgMonoType
                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
                         _other | impred    -> ArbitraryRank
                                | otherwise -> tyConArgMonoType
@@ -805,8 +795,17 @@ check_arg_type (ve@ValidityEnv{ve_rank = rank}) ty
                         -- so that we don't suggest -XImpredicativeTypes in
                         --    (Ord (forall a.a)) => a -> a
                         -- and so that if it Must be a monotype, we check that it is!
-
-        ; check_type (ve{ve_rank = rank'}) ty }
+              ctxt' :: UserTypeCtxt
+              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
+
+        ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
 
 ----------------------------------------
 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
diff --git a/testsuite/tests/ghci/should_fail/T16287.script b/testsuite/tests/ghci/should_fail/T16287.script
new file mode 100644
index 0000000000..9976832cca
--- /dev/null
+++ b/testsuite/tests/ghci/should_fail/T16287.script
@@ -0,0 +1,10 @@
+:set -XPolyKinds -XRankNTypes -XTypeFamilies
+import Data.Kind
+type F1 a = a
+type family F2 :: k
+data T1 :: (Type -> Type) -> Type
+data T2 :: (forall k. k) -> Type
+:kind T1 F1
+:kind T2 F2
+:kind Maybe (T1 F1)
+:kind Maybe (T2 F2)
diff --git a/testsuite/tests/ghci/should_fail/T16287.stderr b/testsuite/tests/ghci/should_fail/T16287.stderr
new file mode 100644
index 0000000000..13f0852144
--- /dev/null
+++ b/testsuite/tests/ghci/should_fail/T16287.stderr
@@ -0,0 +1,12 @@
+
+<interactive>:1:1: error:
+    The type synonym ‘F1’ should have 1 argument, but has been given none
+
+<interactive>:1:1: error:
+    The type family ‘F2’ should have no arguments, but has been given none
+
+<interactive>:1:1: error:
+    The type synonym ‘F1’ should have 1 argument, but has been given none
+
+<interactive>:1:1: error:
+    The type family ‘F2’ should have no arguments, but has been given none
diff --git a/testsuite/tests/ghci/should_fail/all.T b/testsuite/tests/ghci/should_fail/all.T
index 5e0a18c5b8..da01a98e3e 100644
--- a/testsuite/tests/ghci/should_fail/all.T
+++ b/testsuite/tests/ghci/should_fail/all.T
@@ -3,3 +3,4 @@ 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'])
+test('T16287', [], ghci_script, ['T16287.script'])