Control validity-checking of type synonym applications more carefully

Trac #16059 shows that when validity checking applications of type
synonyms, GHC sometimes wasn't checking the expanded type enough.
We must be careful, however, since checking both the expanded type as
well as the arguments to the type synonym can lead to exponential
blowup (see https://ghc.haskell.org/trac/ghc/ticket/16059#comment:4).
Nor can we omit checking either the expanded type or the argument for
correctness reasons.

The solution here is to introduce a new `ExpandMode` data type that
is plumbed through all of the type-validity-checking functions in
`TcValidity`. `ExpandMode` dictates whether we only check the
expanded type (`Expand`), only check the arguments (`NoExpand), or
both (`Both`). Importantly, if we check `Both` in the function for
validity checking type synonym applications, then we switch to
`NoExpand` when checking the arguments so as to avoid exponential
blowup. See `Note [Correctness and performance of type synonym validity
checking]` for the full story.

14 files changed, 271 insertions, 70 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 64f5bc779c..83291d825c 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -368,12 +368,13 @@ checkValidType ctxt ty
                                           -- Can't happen; not used for *user* sigs
 
        ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
+       ; expand <- initialExpandMode
 
        -- Check the internal validity of the type itself
        -- Fail if bad things happen, else we misleading
        -- (and more complicated) errors in checkAmbiguity
        ; checkNoErrs $
-         do { check_type env ctxt rank ty
+         do { check_type env ctxt rank expand ty
             ; checkUserTypeError ty
             ; traceTc "done ct" (ppr ty) }
 
@@ -388,7 +389,8 @@ checkValidMonoType :: Type -> TcM ()
 -- Assumes argument is fully zonked
 checkValidMonoType ty
   = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
-       ; check_type env SigmaCtxt MustBeMonoType ty }
+       ; expand <- initialExpandMode
+       ; check_type env SigmaCtxt MustBeMonoType expand ty }
 
 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
 checkTySynRhs ctxt ty
@@ -397,7 +399,8 @@ checkTySynRhs ctxt ty
        ; if ck
          then  when (tcIsConstraintKind actual_kind)
                     (do { dflags <- getDynFlags
-                        ; check_pred_ty emptyTidyEnv dflags ctxt ty })
+                        ; expand <- initialExpandMode
+                        ; check_pred_ty emptyTidyEnv dflags ctxt expand ty })
          else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
 
   | otherwise
@@ -450,35 +453,143 @@ constraintsAllowed (TySynKindCtxt {})     = False
 constraintsAllowed (TyFamResKindCtxt {})  = False
 constraintsAllowed _ = True
 
+{-
+Note [Correctness and performance of type synonym validity checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the type A arg1 arg2, where A is a type synonym. How should we check
+this type for validity? We have three distinct choices, corresponding to the
+three constructors of ExpandMode:
+
+1. Expand the application of A, and check the resulting type (`Expand`).
+2. Don't expand the application of A. Only check the arguments (`NoExpand`).
+3. Check the arguments *and* check the expanded type (`Both`).
+
+It's tempting to think that we could always just pick choice (3), but this
+results in serious performance issues when checking a type like in the
+signature for `f` below:
+
+  type S = ...
+  f :: S (S (S (S (S (S ....(S Int)...))))
+
+When checking the type of `f`, we'll check the outer `S` application with and
+without expansion, and in *each* of those checks, we'll check the next `S`
+application with and without expansion... the result is exponential blowup! So
+clearly we don't want to use `Both` 100% of the time.
+
+On the other hand, neither is it correct to use exclusively `Expand` or
+exclusively `NoExpand` 100% of the time:
+
+* If one always expands, then one can miss erroneous programs like the one in
+  the `tcfail129` test case:
+
+    type Foo a = String -> Maybe a
+    type Bar m = m Int
+    blah = undefined :: Bar Foo
+
+  If we expand `Bar Foo` immediately, we'll miss the fact that the `Foo` type
+  synonyms is unsaturated.
+* If one never expands and only checks the arguments, then one can miss
+  erroneous programs like the one in Trac #16059:
+
+    type Foo b = Eq b => b
+    f :: forall b (a :: Foo b). Int
+
+  The kind of `a` contains a constraint, which is illegal, but this will only
+  be caught if `Foo b` is expanded.
+
+Therefore, it's impossible to have these validity checks be simultaneously
+correct and performant if one sticks exclusively to a single `ExpandMode`. In
+that case, the solution is to vary the `ExpandMode`s! In more detail:
+
+1. When we start validity checking, we start with `Expand` if
+   LiberalTypeSynonyms is enabled (see Note [Liberal type synonyms] for why we
+   do this), and we start with `Both` otherwise. The `initialExpandMode`
+   function is responsible for this.
+2. When expanding an application of a type synonym (in `check_syn_tc_app`), we
+   determine which things to check based on the current `ExpandMode` argument.
+   Importantly, if the current mode is `Both`, then we check the arguments in
+   `NoExpand` mode and check the expanded type in `Both` mode.
+
+   Switching to `NoExpand` when checking the arguments is vital to avoid
+   exponential blowup. One consequence of this choice is that if you have
+   the following type synonym in one module (with RankNTypes enabled):
+
+     {-# LANGUAGE RankNTypes #-}
+     module A where
+     type A = forall a. a
+
+   And you define the following in a separate module *without* RankNTypes
+   enabled:
+
+     module B where
+
+     import A
+
+     type Const a b = a
+     f :: Const Int A -> Int
+
+   Then `f` will be accepted, even though `A` (which is technically a rank-n
+   type) appears in its type. We view this as an acceptable compromise, since
+   `A` never appears in the type of `f` post-expansion. If `A` _did_ appear in
+   a type post-expansion, such as in the following variant:
+
+     g :: Const A A -> Int
+
+   Then that would be rejected unless RankNTypes were enabled.
+-}
+
+-- | When validity-checking an application of a type synonym, should we
+-- check the arguments, check the expanded type, or both?
+-- See Note [Correctness and performance of type synonym validity checking]
+data ExpandMode
+  = Expand   -- ^ Only check the expanded type.
+  | NoExpand -- ^ Only check the arguments.
+  | Both     -- ^ Check both the arguments and the expanded type.
+
+instance Outputable ExpandMode where
+  ppr e = text $ case e of
+                   Expand   -> "Expand"
+                   NoExpand -> "NoExpand"
+                   Both     -> "Both"
+
+-- | If @LiberalTypeSynonyms@ is enabled, we start in 'Expand' mode for the
+-- reasons explained in @Note [Liberal type synonyms]@. Otherwise, we start
+-- in 'Both' mode.
+initialExpandMode :: TcM ExpandMode
+initialExpandMode = do
+  liberal_flag <- xoptM LangExt.LiberalTypeSynonyms
+  pure $ if liberal_flag then Expand else Both
+
 ----------------------------------------
-check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
+check_type :: TidyEnv -> UserTypeCtxt -> Rank -> ExpandMode -> Type -> TcM ()
 -- The args say what the *type context* requires, independent
 -- of *flag* settings.  You test the flag settings at usage sites.
 --
 -- Rank is allowed rank for function args
 -- Rank 0 means no for-alls anywhere
 
-check_type _ _ _ (TyVarTy _) = return ()
+check_type _ _ _ _ (TyVarTy _) = return ()
 
-check_type env ctxt rank (AppTy ty1 ty2)
-  = do  { check_type env ctxt rank ty1
-        ; check_arg_type env ctxt rank ty2 }
+check_type env ctxt rank expand (AppTy ty1 ty2)
+  = do  { check_type env ctxt rank expand ty1
+        ; check_arg_type env ctxt rank expand ty2 }
 
-check_type env ctxt rank ty@(TyConApp tc tys)
+check_type env ctxt rank expand ty@(TyConApp tc tys)
   | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-  = check_syn_tc_app env ctxt rank ty tc tys
-  | isUnboxedTupleTyCon tc = check_ubx_tuple  env ctxt      ty    tys
-  | otherwise              = mapM_ (check_arg_type env ctxt rank) tys
+  = check_syn_tc_app env ctxt rank expand ty tc tys
+  | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt expand ty tys
+  | otherwise              = mapM_ (check_arg_type env ctxt rank expand) tys
 
-check_type _ _ _ (LitTy {}) = return ()
+check_type _ _ _ _ (LitTy {}) = return ()
 
-check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
+check_type env ctxt rank expand (CastTy ty _) =
+  check_type env ctxt rank expand ty
 
 -- Check for rank-n types, such as (forall x. x -> x) or (Show x => x).
 --
 -- Critically, this case must come *after* the case for TyConApp.
 -- See Note [Liberal type synonyms].
-check_type env ctxt rank ty
+check_type env ctxt rank expand ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
@@ -490,11 +601,12 @@ check_type env ctxt rank ty
                 -- Reject forall (a :: Eq b => b). blah
                 -- In a kind signature we don't allow constraints
 
-        ; check_valid_theta env' SigmaCtxt theta
+        ; check_valid_theta env' SigmaCtxt expand theta
                 -- Allow     type T = ?x::Int => Int -> Int
                 -- but not   type T = ?x::Int
 
-        ; check_type env' ctxt rank tau      -- Allow foralls to right of arrow
+        ; check_type env' ctxt rank expand tau
+                -- Allow foralls to right of arrow
 
         ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
                    (forAllEscapeErr env' ty tau_kind)
@@ -511,21 +623,21 @@ check_type env ctxt rank ty
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
 
-check_type env ctxt rank (FunTy arg_ty res_ty)
-  = do  { check_type env ctxt arg_rank arg_ty
-        ; check_type env ctxt res_rank res_ty }
+check_type env ctxt rank expand (FunTy arg_ty res_ty)
+  = do  { check_type env ctxt arg_rank expand arg_ty
+        ; check_type env ctxt res_rank expand res_ty }
   where
     (arg_rank, res_rank) = funArgResRank rank
 
-check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
+check_type _ _ _ _ ty = pprPanic "check_type" (ppr ty)
 
 ----------------------------------------
-check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
-                 -> TyCon -> [KindOrType] -> TcM ()
+check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> ExpandMode
+                 -> KindOrType -> TyCon -> [KindOrType] -> TcM ()
 -- Used for type synonyms and type synonym families,
 -- which must be saturated,
 -- but not data families, which need not be saturated
-check_syn_tc_app env ctxt rank ty tc tys
+check_syn_tc_app env ctxt rank expand ty tc tys
   | tys `lengthAtLeast` tc_arity   -- Saturated
        -- Check that the synonym has enough args
        -- This applies equally to open and closed synonyms
@@ -533,32 +645,44 @@ check_syn_tc_app env ctxt rank ty tc tys
        --      data Tree a b = ...
        --      type Foo a = Tree [a]
        --      f :: Foo a b -> ...
-  = do  { -- See Note [Liberal type synonyms]
-        ; liberal <- xoptM LangExt.LiberalTypeSynonyms
-        ; if not liberal || isTypeFamilyTyCon tc then
-                -- For H98 and synonym families, do check the type args
-                mapM_ check_arg tys
-
-          else  -- In the liberal case (only for closed syns), expand then check
-          case tcView ty of
-             Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
-                             err_ctxt = text "In the expansion of type synonym"
-                                        <+> quotes (ppr syn_tc)
-                         in addErrCtxt err_ctxt $ check_type env ctxt rank ty'
-             Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
+  = case expand of
+      _ |  isTypeFamilyTyCon tc
+        -> check_args_only expand
+      -- See Note [Correctness and performance of type synonym validity
+      --           checking]
+      Expand   -> check_expansion_only expand
+      NoExpand -> check_args_only expand
+      Both     -> check_args_only NoExpand *> check_expansion_only Both
 
   | 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
+  = check_args_only expand
 
   | otherwise
   = failWithTc (tyConArityErr tc tys)
   where
     tc_arity  = tyConArity tc
+
+    check_arg :: ExpandMode -> KindOrType -> TcM ()
     check_arg
-      | isTypeFamilyTyCon tc = check_arg_type  env arg_ctxt rank
-      | otherwise            = check_type      env arg_ctxt synArgMonoType
+      | isTypeFamilyTyCon tc
+      = check_arg_type  env arg_ctxt rank
+      | otherwise
+      = check_type      env arg_ctxt synArgMonoType
+
+    check_args_only, check_expansion_only :: ExpandMode -> TcM ()
+    check_args_only expand = mapM_ (check_arg expand) tys
+    check_expansion_only expand =
+      case tcView ty of
+         Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
+                         err_ctxt = text "In the expansion of type synonym"
+                                    <+> quotes (ppr syn_tc)
+                     in addErrCtxt err_ctxt $
+                        check_type env ctxt rank 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
@@ -606,9 +730,9 @@ field to False.
 -}
 
 ----------------------------------------
-check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
+check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> ExpandMode -> KindOrType
                 -> [KindOrType] -> TcM ()
-check_ubx_tuple env ctxt ty tys
+check_ubx_tuple env ctxt expand ty tys
   = do  { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
         ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
 
@@ -617,10 +741,11 @@ check_ubx_tuple env ctxt ty tys
                 -- c.f. check_arg_type
                 -- However, args are allowed to be unlifted, or
                 -- more unboxed tuples, so can't use check_arg_ty
-        ; mapM_ (check_type env ctxt rank') tys }
+        ; mapM_ (check_type env ctxt rank' expand) tys }
 
 ----------------------------------------
-check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
+check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> ExpandMode
+               -> 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)
@@ -639,9 +764,9 @@ check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> 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 env ctxt rank ty
+check_arg_type env ctxt rank expand ty
   = do  { impred <- xoptM LangExt.ImpredicativeTypes
         ; let rank' = case rank of          -- Predictive => must be monotype
                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
@@ -652,7 +777,7 @@ check_arg_type env ctxt rank ty
                         --    (Ord (forall a.a)) => a -> a
                         -- and so that if it Must be a monotype, we check that it is!
 
-        ; check_type env ctxt rank' ty }
+        ; check_type env ctxt rank' expand ty }
 
 ----------------------------------------
 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
@@ -766,19 +891,21 @@ checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
 checkValidTheta ctxt theta
   = addErrCtxtM (checkThetaCtxt ctxt theta) $
     do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
-       ; check_valid_theta env ctxt theta }
+       ; expand <- initialExpandMode
+       ; check_valid_theta env ctxt expand theta }
 
 -------------------------
-check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
-check_valid_theta _ _ []
+check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode
+                  -> [PredType] -> TcM ()
+check_valid_theta _ _ _ []
   = return ()
-check_valid_theta env ctxt theta
+check_valid_theta env ctxt expand theta
   = do { dflags <- getDynFlags
        ; warnTcM (Reason Opt_WarnDuplicateConstraints)
                  (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
                  (dupPredWarn env dups)
        ; traceTc "check_valid_theta" (ppr theta)
-       ; mapM_ (check_pred_ty env dflags ctxt) theta }
+       ; mapM_ (check_pred_ty env dflags ctxt expand) theta }
   where
     (_,dups) = removeDups nonDetCmpType theta
     -- It's OK to use nonDetCmpType because dups only appears in the
@@ -809,11 +936,12 @@ to avoid requiring language extensions at the use site.  Main example
 We don't want to require ConstraintKinds in module B.
 -}
 
-check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
+check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode
+              -> PredType -> TcM ()
 -- Check the validity of a predicate in a signature
 -- See Note [Validity checking for constraints]
-check_pred_ty env dflags ctxt pred
-  = do { check_type env SigmaCtxt rank pred
+check_pred_ty env dflags ctxt expand pred
+  = do { check_type env SigmaCtxt rank expand pred
        ; check_pred_help False env dflags ctxt pred }
   where
     rank | xopt LangExt.QuantifiedConstraints dflags
@@ -1563,7 +1691,8 @@ checkValidInstance ctxt hs_type ty
         ; traceTc "checkValidInstance {" (ppr ty)
 
         ; env0 <- tcInitTidyEnv
-        ; check_valid_theta env0 ctxt theta
+        ; expand <- initialExpandMode
+        ; check_valid_theta env0 ctxt expand theta
 
         -- The Termination and Coverate Conditions
         -- Check that instance inference will terminate (if we care)
diff --git a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
index a5c13bb5aa..1d64daa5ae 100644
--- a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
+++ b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE UnboxedTuples #-}
 module Dep05 where
 
 import GHC.Arr
diff --git a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
index a35d679f8d..4c93c907e8 100644
--- a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
+++ b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
@@ -1,3 +1,3 @@
 
-Dep05.hs:5:1:
+Dep05.hs:6:1: error:
     GHC.Arr: Can't be safely imported! The module itself isn't safe.
diff --git a/testsuite/tests/typecheck/should_fail/T16059a.hs b/testsuite/tests/typecheck/should_fail/T16059a.hs
new file mode 100644
index 0000000000..1eb9e67bcc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16059a where
+
+type Foo b = Eq b => b
+
+f :: forall b (a :: Eq b => b). Int
+f = 27
+
+g :: forall b (a :: Foo b). Int
+g = 42
diff --git a/testsuite/tests/typecheck/should_fail/T16059a.stderr b/testsuite/tests/typecheck/should_fail/T16059a.stderr
new file mode 100644
index 0000000000..2768220653
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059a.stderr
@@ -0,0 +1,9 @@
+
+T16059a.hs:8:6: error:
+    • Illegal constraint in a kind: Eq b => b
+    • In the type signature: f :: forall b (a :: Eq b => b). Int
+
+T16059a.hs:11:6: error:
+    • Illegal constraint in a kind: Eq b => b
+    • In the expansion of type synonym ‘Foo’
+      In the type signature: g :: forall b (a :: Foo b). Int
diff --git a/testsuite/tests/typecheck/should_fail/T16059b.hs b/testsuite/tests/typecheck/should_fail/T16059b.hs
new file mode 100644
index 0000000000..a8097b9951
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnboxedTuples #-}
+module T16059b where
+
+type Foo = forall a. a
+type Bar = (# #)
diff --git a/testsuite/tests/typecheck/should_fail/T16059c.hs b/testsuite/tests/typecheck/should_fail/T16059c.hs
new file mode 100644
index 0000000000..d26c7db6d4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059c.hs
@@ -0,0 +1,6 @@
+module T16059c where
+
+import T16059b
+
+f :: Foo -> a -> f
+f g x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T16059c.stderr b/testsuite/tests/typecheck/should_fail/T16059c.stderr
new file mode 100644
index 0000000000..6c6113fb5f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059c.stderr
@@ -0,0 +1,6 @@
+
+T16059c.hs:5:6: error:
+    • Illegal polymorphic type: forall a1. a1
+      Perhaps you intended to use RankNTypes
+    • In the expansion of type synonym ‘Foo’
+      In the type signature: f :: Foo -> a -> f
diff --git a/testsuite/tests/typecheck/should_fail/T16059d.hs b/testsuite/tests/typecheck/should_fail/T16059d.hs
new file mode 100644
index 0000000000..0c61136323
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059d.hs
@@ -0,0 +1,5 @@
+module T16059d where
+
+import T16059b
+
+type Bar' = Bar
diff --git a/testsuite/tests/typecheck/should_fail/T16059d.stderr b/testsuite/tests/typecheck/should_fail/T16059d.stderr
new file mode 100644
index 0000000000..7932d72858
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059d.stderr
@@ -0,0 +1,6 @@
+
+T16059d.hs:5:1: error:
+    • Illegal unboxed tuple type as function argument: (# #)
+      Perhaps you intended to use UnboxedTuples
+    • In the expansion of type synonym ‘Bar’
+      In the type synonym declaration for ‘Bar'’
diff --git a/testsuite/tests/typecheck/should_fail/T16059e.hs b/testsuite/tests/typecheck/should_fail/T16059e.hs
new file mode 100644
index 0000000000..4747edc302
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059e.hs
@@ -0,0 +1,15 @@
+module T16059e where
+
+import T16059b
+
+type Const a b = a
+
+-- This is accepted, since the rank-n type `Foo` never makes it into the type
+-- of `f` post-expansion...
+f :: Const Int Foo -> Int
+f _ = 42
+
+-- ...but this *is* rejected, since `Foo` does make it into the type of `g`
+-- post-expansion.
+g :: Const Foo Foo -> Int
+g _ = f 27
diff --git a/testsuite/tests/typecheck/should_fail/T16059e.stderr b/testsuite/tests/typecheck/should_fail/T16059e.stderr
new file mode 100644
index 0000000000..f5a6bb00ba
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059e.stderr
@@ -0,0 +1,7 @@
+
+T16059e.hs:14:6: error:
+    • Illegal polymorphic type: forall a. a
+      Perhaps you intended to use RankNTypes
+    • In the expansion of type synonym ‘Foo’
+      In the expansion of type synonym ‘Const’
+      In the type signature: g :: Const Foo Foo -> Int
diff --git a/testsuite/tests/typecheck/should_fail/T9858a.stderr b/testsuite/tests/typecheck/should_fail/T9858a.stderr
index a42339ed78..fcf76ef247 100644
--- a/testsuite/tests/typecheck/should_fail/T9858a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9858a.stderr
@@ -1,14 +1,6 @@
 
-T9858a.hs:28:18: error:
-    No instance for (Typeable
-                       ((() :: Constraint, () :: Constraint) => ()))
-      arising from a use of ‘cast’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: cast e
-    In the expression: case cast e of { Just e' -> ecast e' }
-    In an equation for ‘supercast’:
-        supercast
-          = case cast e of { Just e' -> ecast e' }
-          where
-              e = Refl
-              e :: E PX PX
+T9858a.hs:20:18: error:
+    • Illegal qualified type:
+        (() :: Constraint, () :: Constraint) => ()
+    • In the expansion of type synonym ‘PX’
+      In the newtype instance declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index bac4d6b14e..9bd518f10c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -501,3 +501,10 @@ test('T15797', normal, compile_fail, [''])
 test('T15799', normal, compile_fail, [''])
 test('T15801', normal, compile_fail, [''])
 test('T15816', normal, compile_fail, [''])
+test('T16059a', normal, compile_fail, [''])
+test('T16059c', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059c', '-v0'])
+test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059d', '-v0'])
+test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059e', '-v0'])