Impredicativity checking is fooled by a type synonym

Consider the following functions, which all instantiate undefined impredicatively:

{-# LANGUAGE RankNTypes #-}
module Bug where

a :: (forall a. a) -> ()
a = undefined

b :: (Show a => a) -> ()
b = undefined

type C = forall a. a
c :: C -> ()
c = undefined

type D a = Show a => a
d :: D a -> ()
d = undefined

a, b, and c will each fail to typecheck:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:5:5: error:
    • Cannot instantiate unification variable ‘a1’
      with a type involving polytypes: (forall a. a) -> ()
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In an equation for ‘a’: a = undefined
  |
5 | a = undefined
  |     ^^^^^^^^^

Bug.hs:8:5: error:
    • Cannot instantiate unification variable ‘a2’
      with a type involving polytypes: (Show a => a) -> ()
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In an equation for ‘b’: b = undefined
    • Relevant bindings include
        b :: (Show a => a) -> () (bound at Bug.hs:8:1)
  |
8 | b = undefined
  |     ^^^^^^^^^

Bug.hs:12:5: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving polytypes: C -> ()
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In an equation for ‘c’: c = undefined
   |
12 | c = undefined
   |     ^^^^^^^^^

Curiously, there is no error message for d. In fact, if you comment out a, b, and c, then d will typecheck! This is concerning, as d is just a variant of b with an extra type synonym thrown into the mix.

Why is it that c, which also uses a type synonym, is rejected, but d is accepted? It's ultimately because of GHC.Tc.Utils.Unify.preCheck, which powers GHC's impredicative instantiation checks. This part of preCheck is suspicious:

preCheck dflags ty_fam_ok tv ty
  = fast_check ty
  where
    ...

    fast_check :: TcType -> MetaTyVarUpdateResult ()
    ...
    fast_check (TyConApp tc tys)
      | bad_tc tc              = MTVU_Bad
      | otherwise              = mapM fast_check tys >> ok
    ...

    bad_tc :: TyCon -> Bool
    bad_tc tc
      | not (impredicative_ok || isTauTyCon tc)     = True
      | not (ty_fam_ok        || isFamFreeTyCon tc) = True
      | otherwise                                   = False

If bad_tc returns True, then that results in a TyConApp being flagged as impredicative. bad_tc first checks if impredicative_ok is True (i.e., if ImpredicativeTypes is enabled), and since that isn't the case in the program above, it checks isTauTyCon tc. For type synonyms like C and D, this checks if the RHS of the type synonym is a tau type, as defined by the isTauTy function:

-- @isTauTy@ tests if a type has no foralls
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
isTauTy (TyVarTy _)           = True
isTauTy (LitTy {})            = True
isTauTy (TyConApp tc tys)     = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b)           = isTauTy a && isTauTy b
isTauTy (FunTy _ a b)         = isTauTy a && isTauTy b
isTauTy (ForAllTy {})         = False
isTauTy (CastTy ty _)         = isTauTy ty
isTauTy (CoercionTy _)        = False  -- Not sure about this

However, isTauTy only checks if a type contains foralls, not contexts! As a result, C is flagged as impredicative, but D a is not.

I wonder if the definition of isTauTy should be expanded to detect higher-rank contexts in addition to higher-rank foralls? In other words, should the following change be applied?

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1e7af2d8cf..3cf4231480 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1864,6 +1864,7 @@ isTauTy (TyVarTy _)           = True
 isTauTy (LitTy {})            = True
 isTauTy (TyConApp tc tys)     = all isTauTy tys && isTauTyCon tc
 isTauTy (AppTy a b)           = isTauTy a && isTauTy b
+isTauTy (FunTy InvisArg _ _)  = False
 isTauTy (FunTy _ a b)         = isTauTy a && isTauTy b
 isTauTy (ForAllTy {})         = False
 isTauTy (CastTy ty _)         = isTauTy ty

This change suffices to make d be flagged as impredicative, and it passes GHC's test suite to boot. But then again, I'm unclear on the origins of the term "tau type"—perhaps it's permissible for tau types to have higher-rank contexts? If so, this suggests that we'd need to implement a variant of isTauTy that checked for both contexts and foralls.