LiberalTypeSynonyms unsaturation check doesn't kick in

GHC accepts this program:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

import GHC.Exts (Any)

type KindOf (a :: k) = k
type A a = (Any :: a)
type KA = KindOf A

But it really oughtn't to. After all, we have an unsaturated use of A in KindOf A, and we don't have LiberalTypeSynonyms enabled!

What's even stranger is that there seems to be something about this exact setup that sneaks by LiberalTypeSynonyms' validity checks. If I add another argument to A:

type A x a = (Any :: a)

Then it //does// error:

$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:10:1: error:
    • Illegal polymorphic type: forall a -> a
      Perhaps you intended to use LiberalTypeSynonyms
    • In the type synonym declaration for ‘KA’
   |
10 | type KA = KindOf A
   | ^^^^^^^^^^^^^^^^^^

Similarly, if I use something besides KindOf:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

import GHC.Exts (Any)

type A a = (Any :: a)
type B a = Int
type C = B A

Then I also get the same Illegal polymorphic type: forall a -> a error.

Trac metadata

Trac field	Value
Version	8.6.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture